Changeset 261
 Timestamp:
 Nov 23, 2010, 3:50:28 PM (9 years ago)
 Location:
 Deliverables/D4.1/Matita
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Nat.ma
r260 r261 207 207 nqed. 208 208 209 naxiom less_than_or_equal_injective: 210 ∀m, n: Nat. 211 S m ≤ S n → m ≤ n. 212 209 213 (* 210 nlemma less_than_or_equal_injective:211 ∀m, n: Nat.212 S m ≤ S n → m ≤ n.213 #m n.214 nelim m.215 #H.216 napplyS less_than_or_equal_zero.217 #N H H2.218 ndestruct.219 220 214 nlemma less_than_or_equal_zero_equal_zero: 221 215 ∀m: Nat. … … 249 243 napplyS less_than_or_equal_zero. 250 244 #N H H2. 251 //. 252 napplyS H. 253 245 nrewrite > H. 246 nnormalize. 254 247 255 248 nlemma less_than_or_equal_transitive: … … 262 255 #N H H2. 263 256 nnormalize. 264 #;265 257 *) 266 258 
Deliverables/D4.1/Matita/Vector.ma
r260 r261 37 37 (* ===================================== *) 38 38 39 naxiom succ_less_than_injective: 40 ∀m, n: Nat. 41 S m < S n → m < n. 42 43 naxiom nothing_less_than_Z: 44 ∀m: Nat. 45 ¬(m < Z). 46 39 47 nlet rec get_index (A: Type[0]) (n: Nat) 48 (v: Vector A n) (m: Nat) (lt: m < n) on m: A ≝ 49 (match m with 50 [ Z ⇒ 51 match v return λx.λ_. Z < x → A with 52 [ Empty ⇒ λabsd1: Z < Z. ? 53  Cons p hd tl ⇒ λprf1: Z < S p. hd 54 ] 55  S o ⇒ 56 (match v return λx.λ_. S o < x → A with 57 [ Empty ⇒ λprf: S o < Z. ? 58  Cons p hd tl ⇒ λprf: S o < S p. get_index A p tl o ? 59 ]) 60 ]) lt. 61 ##[ ncases (nothing_less_than_Z Z); #K; ncases (K absd1) 62 ## ncases (nothing_less_than_Z (S o)); #K; ncases (K prf) 63 ## napply succ_less_than_injective; nassumption 64 ##] 65 nqed. 66 67 nlet rec get_index_weak (A: Type[0]) (n: Nat) 40 68 (v: Vector A n) (m: Nat) on m ≝ 41 69 match m with … … 48 76 match v with 49 77 [ Empty ⇒ Nothing A 50  Cons p hd tl ⇒ get_index A p tl o78  Cons p hd tl ⇒ get_index_weak A p tl o 51 79 ] 52 80 ]. … … 54 82 interpretation "Vector get_index" 'get_index v n = (get_index ? ? v n). 55 83 56 nlet rec set_index (A: Type[0]) (n: Nat) (v: Vector A n) (m: Nat) (a: A) on m≝57 match m return (λx. x < n → A)with84 nlet rec set_index (A: Type[0]) (n: Nat) (v: Vector A n) (m: Nat) (a: A) (lt: m < n) on m: Vector A n ≝ 85 (match m with 58 86 [ Z ⇒ 59 match v with 60 [ Empty ⇒ λ_.? 61  Cons p hd tl ⇒ λ_.hd 62 ] 63  S o ⇒ 64 match v with 65 [ Empty ⇒ λ_.? 66  Cons p hd tl ⇒ λprf: m < p. set_index A p tl o a 67 ] 68 ]. 87 match v return λx.λ_. Z < x → Vector A x with 88 [ Empty ⇒ λabsd1: Z < Z. Empty A 89  Cons p hd tl ⇒ λprf1: Z < S p. (a :: tl) 90 ] 91  S o ⇒ 92 (match v return λx.λ_. S o < x → Vector A x with 93 [ Empty ⇒ λprf: S o < Z. Empty A 94  Cons p hd tl ⇒ λprf: S o < S p. hd :: (set_index A p tl o a ?) 95 ]) 96 ]) lt. 97 napply succ_less_than_injective. 98 nassumption. 99 nqed. 69 100 70 101 nlet rec set_index_weak (A: Type[0]) (n: Nat) 
Deliverables/D4.1/Matita/depends
r260 r261 1 Exponential.ma Connectives.ma Equality.ma Nat.ma 1 2 Arithmetic.ma BitVector.ma Bool.ma Connectives.ma Exponential.ma List.ma Nat.ma Plogic/equality.ma Universes.ma 2 Exponential.ma Connectives.ma Equality.ma Nat.ma3 3 BitVectorTrie.ma BitVector.ma Bool.ma Maybe.ma 4 4 Cartesian.ma Universes.ma 5 Universes.ma 5 6 Maybe.ma Bool.ma Plogic/equality.ma Universes.ma 6 7 Either.ma Bool.ma Maybe.ma Universes.ma 7 Universes.ma8 8 ASM.ma BitVector.ma BitVectorTrie.ma Either.ma Plogic/equality.ma Universes.ma 9 Char.ma Universes.ma 9 10 Vector.ma Cartesian.ma List.ma Maybe.ma Nat.ma Plogic/equality.ma Universes.ma Util.ma 10 Char.ma Universes.ma11 11 Connectives.ma Plogic/equality.ma 12 12 Bool.ma Universes.ma … … 14 14 Util.ma Nat.ma 15 15 Interpret.ma Arithmetic.ma BitVectorTrie.ma 16 String.ma Char.ma List.ma 16 17 BitVector.ma Bool.ma List.ma Nat.ma Universes.ma Vector.ma 17 18 Compare.ma Universes.ma 18 String.ma Char.ma List.ma19 19 Plogic/equality.ma Universes.ma 20 20 Nat.ma Bool.ma Cartesian.ma Connectives.ma
Note: See TracChangeset
for help on using the changeset viewer.