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

Last change on this file since 229 was 229, checked in by mulligan, 9 years ago

More changes.

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".
7include "Util.ma".
8(* include "List.ma". *)
9
10include "logic/pts.ma".
11include "Plogic/equality.ma".
12
13ninductive Vector (A: Type[0]): Nat → Type[0] ≝
14  Empty: Vector A Z
15| Cons: ∀n: Nat. A → Vector A n → Vector A (S n).
16
17notation "hvbox(hd break :: tl)"
18  right associative with precedence 52
19  for @{ 'Cons $hd $tl }.
20 
21interpretation "Vector cons" 'Cons hd tl = (Cons ? ? hd tl).
22
23nlet rec map (A: Type[0]) (B: Type[0]) (n: Nat)
24             (f: A → B) (v: Vector A n) on v ≝
25  match v with
26    [ Empty ⇒ Empty B
27    | Cons n hd tl ⇒ (f hd) :: (map A B n f tl)
28    ].
29   
30nlet rec fold_right (A: Type[0]) (B: Type[0]) (n: Nat)
31                    (f: A → B → B) (x: B) (v: Vector A n) on v ≝
32  match v with
33    [ Empty ⇒ x
34    | Cons n hd tl ⇒ f hd (fold_right A B n f x tl)
35    ].
36   
37nlet rec fold_left (A: Type[0]) (B: Type[0]) (n: Nat)
38                    (f: A → B → A) (x: A) (v: Vector B n) on v ≝
39  match v with
40    [ Empty ⇒ x
41    | Cons n hd tl ⇒ f (fold_left A B n f x tl) hd
42    ].
43   
44nlet rec length (A: Type[0]) (n: Nat) (v: Vector A n) on v ≝
45  match v with
46    [ Empty ⇒ Z
47    | Cons n hd tl ⇒ S $ length A n tl
48    ].
49
50nlet rec replicate (A: Type[0]) (n: Nat) (h: A) on n ≝
51  match n return λn. Vector A n with
52    [ Z ⇒ Empty A
53    | S m ⇒ h :: (replicate A m h)
54    ].
55   
56nlemma eq_rect_Type0_r :
57  ∀A: Type[0].
58  ∀a:A.
59  ∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
60  #A;
61  #a;
62  #P;
63  #H;
64  #x;
65  #p;
66  ngeneralize in match H;
67  ngeneralize in match P;
68  ncases p;
69  //;
70nqed.
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 hd' tl' ⇒
80            λe: S n = S m.
81              (f hd hd') :: (zip A B C n f tl ?)
82        ]
83    ])
84    (refl ? n).
85      ##
86        [ #e;
87          ndestruct(e);
88          ##
89        | ndestruct(e);
90          napply tl'
91          ##
92        ]
93nqed.
Note: See TracBrowser for help on using the repository browser.