source: Deliverables/D4.1/Matita/Vector.ma @ 228

Last change on this file since 228 was 228, checked in by mulligan, 10 years ago

Conjunction, disjunction and 'xorjunction' implemented on bitvectors.
Lots of supporting datatypes. Vectors.ma includes some diabolical
dependent type hackery due to Wilmer.

File size: 2.4 KB
Line 
1(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
2(* Vectors.ma: Fixed length bitvectors, and routine operations on them.       *)
3(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
4
5include "Cartesian.ma".
6include "Nat.ma".
7(* include "List.ma". *)
8
9include "logic/pts.ma".
10include "Plogic/equality.ma".
11
12ninductive Vector (A: Type[0]): Nat → Type[0] ≝
13  Empty: Vector A Z
14| Cons: ∀n: Nat. A → Vector A n → Vector A (S n).
15
16notation "hvbox(hd break :: tl)"
17  right associative with precedence 52
18  for @{ 'Cons $hd $tl }.
19 
20interpretation "Vector cons" 'Cons hd tl = (Cons ? ? hd tl).
21
22nlet rec map (A: Type[0]) (B: Type[0]) (n: Nat)
23             (f: A → B) (v: Vector A n) on v ≝
24  match v with
25    [ Empty ⇒ Empty B
26    | Cons n hd tl ⇒ (f hd) :: (map A B n f tl)
27    ].
28   
29nlet rec fold_right (A: Type[0]) (B: Type[0]) (n: Nat)
30                    (f: A → B → B) (x: B) (v: Vector A n) on v ≝
31  match v with
32    [ Empty ⇒ x
33    | Cons n hd tl ⇒ f hd (fold_right A B n f x tl)
34    ].
35   
36nlet rec fold_left (A: Type[0]) (B: Type[0]) (n: Nat)
37                    (f: A → B → A) (x: A) (v: Vector B n) on v ≝
38  match v with
39    [ Empty ⇒ x
40    | Cons n hd tl ⇒ f (fold_left A B n f x tl) hd
41    ].
42   
43nlet rec length (A: Type[0]) (n: Nat) (v: Vector A n) on v ≝
44  match v with
45    [ Empty ⇒ Z
46    | Cons n hd tl ⇒ S (length A n tl)
47    ].
48
49nlet 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)
53    ].
54   
55nlemma 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  //;
69nqed.
70
71
72nlet 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        ]
93nqed.
Note: See TracBrowser for help on using the repository browser.