Changeset 261 for Deliverables/D4.1/Matita/Vector.ma
 Timestamp:
 Nov 23, 2010, 3:50:28 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

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)
Note: See TracChangeset
for help on using the changeset viewer.