Changeset 465 for Deliverables/D4.1/Matita/Util.ma
 Timestamp:
 Jan 20, 2011, 6:10:07 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Util.ma
r246 r465 1 include "Nat.ma". 1 include "arithmetics/nat.ma". 2 include "datatypes/pairs.ma". 3 include "datatypes/sums.ma". 4 include "datatypes/list.ma". 5 6 nlet rec fold_left_i_aux (A: Type[0]) (B: Type[0]) 7 (f: nat → A → B → A) (x: A) (i: nat) (l: list B) on l ≝ 8 match l with 9 [ nil ⇒ x 10  cons hd tl ⇒ fold_left_i_aux A B f (f i x hd) (S i) tl 11 ]. 12 13 ndefinition fold_left_i ≝ λA,B,f,x. fold_left_i_aux A B f x O. 14 2 15 3 16 ndefinition function_apply ≝ … … 13 26 interpretation "Function application" 'function_apply f x = (function_apply ? ? f x). 14 27 15 nlet rec iterate (A: Type[0]) (f: A → A) (a: A) (n: Nat) on n ≝28 nlet rec iterate (A: Type[0]) (f: A → A) (a: A) (n: nat) on n ≝ 16 29 match n with 17 [ Z⇒ a30 [ O ⇒ a 18 31  S o ⇒ f (iterate A f a o) 19 32 ]. 33 34 notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)" 35 with precedence 10 36 for @{ match $t with [ mk_pair ${ident x} ${ident y} ⇒ $s ] }. 37 38 39 notation "⊥" with precedence 90 40 for @{ match ? in False with [ ] }. 41 42 nlet rec if_then_else (A: Type[0]) (b: bool) (t: A) (f: A) on b ≝ 43 match b with 44 [ true ⇒ t 45  false ⇒ f 46 ]. 47 48 notation "hvbox('if' b 'then' t 'else' f)" 49 non associative with precedence 83 50 for @{ 'if_then_else $b $t $f }. 51 52 interpretation "Bool if_then_else" 'if_then_else b t f = (if_then_else ? b t f). 53 54 nlet rec exclusive_disjunction (b: bool) (c: bool) on b ≝ 55 match b with 56 [ true ⇒ 57 match c with 58 [ false ⇒ true 59  true ⇒ false 60 ] 61  false ⇒ 62 match c with 63 [ false ⇒ false 64  true ⇒ true 65 ] 66 ]. 67 68 ndefinition ltb ≝ 69 λm, n: nat. 70 leb (S m) n. 71 72 ndefinition geb ≝ 73 λm, n: nat. 74 ltb n m. 75 76 ndefinition gtb ≝ 77 λm, n: nat. 78 leb n m. 79 80 interpretation "Nat less than" 'lt m n = (ltb m n). 81 interpretation "Nat greater than" 'gt m n = (gtb m n). 82 interpretation "Nat greater than eq" 'geq m n = (geb m n). 83 84 nlet rec division_aux (m: nat) (n : nat) (p: nat) ≝ 85 match ltb n p with 86 [ true ⇒ O 87  false ⇒ 88 match m with 89 [ O ⇒ O 90  (S q) ⇒ S (division_aux q (n  (S p)) p) 91 ] 92 ]. 93 94 ndefinition division ≝ 95 λm, n: nat. 96 match n with 97 [ O ⇒ S m 98  S o ⇒ division_aux m m o 99 ]. 100 101 notation "hvbox(n break ÷ m)" 102 right associative with precedence 47 103 for @{ 'division $n $m }. 104 105 interpretation "Nat division" 'division n m = (division n m). 106 107 nlet rec modulus_aux (m: nat) (n: nat) (p: nat) ≝ 108 match leb n p with 109 [ true ⇒ n 110  false ⇒ 111 match m with 112 [ O ⇒ n 113  S o ⇒ modulus_aux o (n  (S p)) p 114 ] 115 ]. 116 117 ndefinition modulus ≝ 118 λm, n: nat. 119 match n with 120 [ O ⇒ m 121  S o ⇒ modulus_aux m m o 122 ]. 123 124 notation "hvbox(n break 'mod' m)" 125 right associative with precedence 47 126 for @{ 'modulus $n $m }. 127 128 interpretation "Nat modulus" 'modulus m n = (modulus m n). 129 130 ndefinition divide_with_remainder ≝ 131 λm, n: nat. 132 mk_pair ? ? (m ÷ n) (modulus m n). 133 134 nlet rec exponential (m: nat) (n: nat) on n ≝ 135 match n with 136 [ O ⇒ S O 137  S o ⇒ m * exponential m o 138 ]. 139 140 interpretation "Nat exponential" 'exp n m = (exponential n m). 141 142 notation "hvbox(a break ⊎ b)" 143 left associative with precedence 50 144 for @{ 'disjoint_union $a $b }. 145 interpretation "sum" 'disjoint_union A B = (Sum A B). 146 147 ntheorem less_than_or_equal_monotone: 148 ∀m, n: nat. 149 m ≤ n → (S m) ≤ (S n). 150 #m n H; nelim H; /2/. 151 nqed. 152 153 ntheorem less_than_or_equal_b_complete: ∀m,n. leb m n = false → ¬(m ≤ n). 154 #m; nelim m; nnormalize 155 [ #n H; ndestruct  #y H1 z; ncases z; nnormalize 156 [ #H; /2/  /3/ ] 157 nqed. 158 159 ntheorem less_than_or_equal_b_correct: ∀m,n. leb m n = true → m ≤ n. 160 #m; nelim m; //; #y H1 z; ncases z; nnormalize 161 [ #H; ndestruct  /3/ ] 162 nqed. 163 164 ndefinition less_than_or_equal_b_elim: 165 ∀m,n. ∀P: bool → Type[0]. (m ≤ n → P true) → (¬(m ≤ n) → P false) → 166 P (leb m n). 167 #m n P H1 H2; nlapply (less_than_or_equal_b_correct m n); 168 nlapply (less_than_or_equal_b_complete m n); 169 ncases (leb m n); /3/. 170 nqed.
Note: See TracChangeset
for help on using the changeset viewer.