Changeset 228 for Deliverables/D4.1/Matita
 Timestamp:
 Nov 9, 2010, 3:27:30 PM (10 years ago)
 Location:
 Deliverables/D4.1/Matita
 Files:

 6 added
 2 moved
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/BitVector.ma
r224 r228 1 include "Vectors.ma". 1 include "Vector.ma". 2 include "Nat.ma". 3 include "Bool.ma". 2 4 3 include "arithmetics/nat.ma". 4 include "basics/bool.ma". 5 ndefinition BitVector ≝ λn: Nat. Vector Bool n. 5 6 6 ndefinition BitVector ≝ λn: nat. Vector bool n. 7 7 ndefinition zero ≝ 8 λn: Nat. 9 replicate Bool n False. 10 8 11 ndefinition conjunction ≝ 9 λn: nat. 10 λv, q: BitVector n. 11 fold_right ∧ true v q. 12 λn: Nat. 13 λb: BitVector n. 14 λc: BitVector n. 15 zip Bool Bool Bool n conjunction b c. 16 17 ndefinition inclusive_disjunction ≝ 18 λn: Nat. 19 λb: BitVector n. 20 λc: BitVector n. 21 zip Bool Bool Bool n inclusive_disjunction b c. 22 23 ndefinition exclusive_disjunction ≝ 24 λn: Nat. 25 λb: BitVector n. 26 λc: BitVector n. 27 zip Bool Bool Bool n exclusive_disjunction b c. 28 29 
Deliverables/D4.1/Matita/Vector.ma
r224 r228 4 4 5 5 include "Cartesian.ma". 6 include "List.ma". 6 include "Nat.ma". 7 (* include "List.ma". *) 7 8 8 9 include "logic/pts.ma". 9 include "basics/eq.ma". 10 include "basics/bool.ma". 11 include "arithmetics/nat.ma". 12 include "nat/plus.ma". 13 include "nat/minus.ma". 10 include "Plogic/equality.ma". 14 11 15 ninductive Vector (A: Type[0]): nat → Type[0] ≝16 Empty: Vector A 017  Cons: ∀n: nat. A → Vector A n → Vector A (S n).12 ninductive Vector (A: Type[0]): Nat → Type[0] ≝ 13 Empty: Vector A Z 14  Cons: ∀n: Nat. A → Vector A n → Vector A (S n). 18 15 19 nlet rec map (A: Type[0]) (B: Type[0]) (n: nat) (f: A → B) (v: Vector A n) on v ≝ 16 notation "hvbox(hd break :: tl)" 17 right associative with precedence 52 18 for @{ 'Cons $hd $tl }. 19 20 interpretation "Vector cons" 'Cons hd tl = (Cons ? ? hd tl). 21 22 nlet rec map (A: Type[0]) (B: Type[0]) (n: Nat) 23 (f: A → B) (v: Vector A n) on v ≝ 20 24 match v with 21 25 [ Empty ⇒ Empty B 22  Cons n hd tl ⇒ Cons B n (f hd)(map A B n f tl)26  Cons n hd tl ⇒ (f hd) :: (map A B n f tl) 23 27 ]. 24 28 25 nlet rec fold_right (A: Type[0]) (B: Type[0]) (n: nat)29 nlet rec fold_right (A: Type[0]) (B: Type[0]) (n: Nat) 26 30 (f: A → B → B) (x: B) (v: Vector A n) on v ≝ 27 31 match v with … … 30 34 ]. 31 35 32 nlet rec fold_left (A: Type[0]) (B: Type[0]) (n: nat)36 nlet rec fold_left (A: Type[0]) (B: Type[0]) (n: Nat) 33 37 (f: A → B → A) (x: A) (v: Vector B n) on v ≝ 34 38 match v with … … 37 41 ]. 38 42 39 nlet rec length (A: Type[0]) (n: nat) (v: Vector A n) on v ≝43 nlet rec length (A: Type[0]) (n: Nat) (v: Vector A n) on v ≝ 40 44 match v with 41 [ Empty ⇒ 045 [ Empty ⇒ Z 42 46  Cons n hd tl ⇒ S (length A n tl) 43 47 ]. 44 48 45 nlet rec from_list (A: Type[0]) (l: List A) on l≝46 match lwith47 [ Empty⇒ Empty A48  Cons hd tl ⇒ Cons (length A tl) hd (from_list A tl)49 nlet rec replicate (A: Type[0]) (n: Nat) (h: A) on n ≝ 50 match n return λn. Vector A n with 51 [ Z ⇒ Empty A 52  S m ⇒ h :: (replicate A m h) 49 53 ]. 54 55 nlemma eq_rect_Type0_r : 56 ∀A: Type[0]. 57 ∀a:A. 58 ∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p. 59 #A; 60 #a; 61 #P; 62 #H; 63 #x; 64 #p; 65 ngeneralize in match H; 66 ngeneralize in match P; 67 ncases p; 68 //; 69 nqed. 70 71 72 nlet rec zip (A: Type[0]) (B: Type[0]) (C: Type[0]) (n: Nat) 73 (f: A → B → C) (v: Vector A n) (q: Vector B n) on v ≝ 74 (match v return (λx.λr. x = n → Vector C x) with 75 [ Empty ⇒ λ_. Empty C 76  Cons n hd tl ⇒ 77 match q return (λy.λr. S n = y → Vector C (S n)) with 78 [ Empty ⇒ ? 79  Cons m hd2 tl2 ⇒ 80 λe: S n = S m. 81 Cons C n (f hd hd2) (zip A B C n f tl ?) 82 ] 83 ]) 84 (refl ? n). 85 ## 86 [ #e; 87 ndestruct (e); 88 ## 89  ndestruct (e); 90 napply tl2 91 ## 92 ] 93 nqed.
Note: See TracChangeset
for help on using the changeset viewer.