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

Last change on this file since 228 was 228, checked in by mulligan, 9 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.