Changeset 232 for Deliverables
 Timestamp:
 Nov 11, 2010, 4:56:59 PM (10 years ago)
 Location:
 Deliverables/D4.1/Matita
 Files:

 4 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/BitVector.ma
r231 r232 32 32 zip Bool Bool Bool n exclusive_disjunction b c. 33 33 34 nlet rec pad (n: Nat) (m: Nat) (b: BitVector n) (p: less_than_or_equal n m) ≝ 34 nlet rec pad (n: Nat) (m: Nat) (b: BitVector n) (p: less_than_or_equal_p n m): (BitVector (n + m)) ≝ 35 match m with 36 [ Z ⇒ ? 37  S o ⇒ ? 38 ]. 39 40 //. 41 nqed. 42 43 ncheck pad. 35 44 
Deliverables/D4.1/Matita/Bool.ma
r228 r232 48 48 [ True ⇒ False 49 49  False ⇒ True 50 ]. 50 ]. 51 
Deliverables/D4.1/Matita/Nat.ma
r231 r232 5 5 include "logic/pts.ma". 6 6 include "Plogic/equality.ma". 7 include "Plogic/connectives.ma". 7 8 8 9 ninductive Nat: Type[0] ≝ … … 50 51 interpretation "Nat multiplication" 'times n m = (multiplication n m). 51 52 52 nlet rec less_than_or_equal (n: Nat) (m: Nat) ≝ 53 match n with 53 ninductive less_than_or_equal_p (n: Nat): Nat → Prop ≝ 54 ltoe_refl: less_than_or_equal_p n n 55  ltoe_step: ∀m: Nat. less_than_or_equal_p n m → less_than_or_equal_p n (S m). 56 57 nlet rec less_than_or_equal_b (m: Nat) (n: Nat) on m ≝ 58 match m with 54 59 [ Z ⇒ True 55 60  S o ⇒ 56 match mwith61 match n with 57 62 [ Z ⇒ False 58  S p ⇒ less_than_or_equal o p63  S p ⇒ less_than_or_equal_b o p 59 64 ] 60 65 ]. … … 64 69 for @{ 'less_than_or_equal $n $m }. 65 70 66 interpretation "Nat less than or equal" 'less_than_or_equal n m = (less_than_or_equal n m). 71 interpretation "Nat less than or equal prop" 'less_than_or_equal n m = (less_than_or_equal_p n m). 72 interpretation "Nat less than or equal bool" 'less_than_or_equal n m = (less_than_or_equal_b n m). 73 74 ndefinition less_than_p ≝ 75 λm, n: Nat. 76 m ≤ n ∧ ¬(m = n). 77 78 notation "n break < m" 79 non associative with precedence 47 80 for @{ 'less_than $n $m }. 81 82 interpretation "Nat less than prop" 'less_than n m = (less_than_p n m). 83 84 (* 85 nlet rec greatest_common_divisor (m: Nat) (n: Nat) on n ≝ 86 match n with 87 [ Z ⇒ m 88  S o ⇒ greatest_common_divisor n (modulus m n) 89 ]. 90 *) 91 92 nlemma less_than_or_equal_zero: 93 ∀n: Nat. 94 Z ≤ n. 95 #n. 96 nelim n. 97 //. 98 #N. 99 //. 100 nqed. 101 102 (* 103 nlemma less_than_or_equal_injective: 104 ∀m, n: Nat. 105 S m ≤ S n → m ≤ n. 106 #m n. 107 nelim m. 108 #H. 109 napplyS less_than_or_equal_zero. 110 #N H H2. 111 ndestruct. 112 113 nlemma less_than_or_equal_zero_equal_zero: 114 ∀m: Nat. 115 m ≤ Z → m = Z. 116 #m. 117 nelim m. 118 //. 119 #N H H2. 120 nnormalize. 121 *) 122 123 nlemma less_than_or_equal_reflexive: 124 ∀n: Nat. 125 n ≤ n. 126 #n. 127 nelim n. 128 nnormalize. 129 @. 130 #N H. 131 nnormalize. 132 //. 133 nqed. 134 135 (* 136 nlemma less_than_or_equal_succ: 137 ∀m, n: Nat. 138 S m ≤ n → m ≤ n. 139 #m n. 140 nelim m. 141 #H. 142 napplyS less_than_or_equal_zero. 143 #N H H2. 144 //. 145 napplyS H. 146 147 148 nlemma less_than_or_equal_transitive: 149 ∀m, n, o: Nat. 150 m ≤ n ∧ n ≤ o → m ≤ o. 151 #m n o. 152 nelim m. 153 #H. 154 napply less_than_or_equal_zero. 155 #N H H2. 156 nnormalize. 157 #; 158 *) 67 159 68 160 nlemma plus_zero: 
Deliverables/D4.1/Matita/Vector.ma
r231 r232 165 165 ]. 166 166 167 (* 167 168 nlet rec from_list (A: Type[0]) (l: List A) on l ≝ 168 169 match l return λl. Vector A (length A l) with … … 172 173 //. 173 174 nqed. 175 *) 174 176 175 177 (* ===================================== *) … … 248 250 @. 249 251 nqed. 250 251 nlemma from_list_to_list_left_inverse:252 ∀A: Type[0].253 ∀l: List A.254 to_list A (length A l) (from_list A l) = l.
Note: See TracChangeset
for help on using the changeset viewer.