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

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

Lots of work from today.

File size: 4.1 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".
8include "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 a P H x p.
61  ngeneralize in match H.
62  ngeneralize in match P.
63  ncases p.
64  //.
65nqed.
66
67nlet rec zip (A: Type[0]) (B: Type[0]) (C: Type[0]) (n: Nat)
68             (f: A → B → C) (v: Vector A n) (q: Vector B n) on v ≝
69  (match v return (λx.λr. x = n → Vector C x) with
70    [ Empty ⇒ λ_. Empty C
71    | Cons n hd tl ⇒
72      match q return (λy.λr. S n = y → Vector C (S n)) with
73        [ Empty ⇒ ?
74        | Cons m hd' tl' ⇒
75            λe: S n = S m.
76              (f hd hd') :: (zip A B C n f tl ?)
77        ]
78    ])
79    (refl ? n).
80      ##
81        [ #e;
82          ndestruct(e);
83          ##
84        | ndestruct(e);
85          napply tl'
86          ##
87        ]
88nqed.
89
90nlet rec append (A: Type[0]) (n: Nat) (m: Nat)
91                (v: Vector A n) (q: Vector A m) on v ≝
92  match v return (λn.λv. Vector A (n + m)) with
93    [ Empty ⇒ q
94    | Cons o hd tl ⇒ hd :: (append A o m tl q)
95    ].
96
97nlet rec reverse (A: Type[0]) (n: Nat)
98                 (v: Vector A n) on v ≝
99  match v return (λm.λv. Vector A m) with
100    [ Empty ⇒ Empty A
101    | Cons o hd tl ⇒ ? (append A o ? (reverse A o tl) (Cons A Z hd (Empty A)))
102    ].
103    //.
104nqed.
105
106nlet rec to_list (A: Type[0]) (n: Nat)
107                 (v: Vector A n) on v ≝
108  match v with
109    [ Empty ⇒ cic:/matita/Cerco/List/List.con(0,1,1) A
110    | Cons o hd tl ⇒ hd :: (to_list A o tl)
111    ].
112   
113nlet rec rotate_left (A: Type[0]) (n: Nat) (v: Vector A n)
114                     (m: Nat) on m: Vector A n ≝
115  match m with
116    [ Z ⇒ v
117    | S o ⇒
118        match v with
119          [ Empty ⇒ Empty A
120          | Cons p hd tl ⇒
121             rotate_left A (S p) (? (append A p ? tl (Cons A ? hd (Empty A)))) o
122          ]
123    ].
124    //.
125nqed.
126   
127nlemma map_fusion:
128  ∀A, B, C: Type[0].
129  ∀n: Nat.
130  ∀v: Vector A n.
131  ∀f: A → B.
132  ∀g: B → C.
133    map B C n g (map A B n f v) = map A C n (λx. g (f x)) v.
134  #A B C n v f g.
135  nelim v.
136  nnormalize.
137  @.
138  #N H V H2.
139  nnormalize.
140  nrewrite > H2.
141  @.
142nqed.
143
144nlemma length_correct:
145  ∀A: Type[0].
146  ∀n: Nat.
147  ∀v: Vector A n.
148    length A n v = n.
149  #A n v.
150  nelim v.
151  nnormalize.
152  @.
153  #N H V H2.
154  nnormalize.
155  nrewrite > H2.
156  @.
157nqed.
158
159nlemma map_length:
160  ∀A, B: Type[0].
161  ∀n: Nat.
162  ∀v: Vector A n.
163  ∀f: A → B.
164    length A n v = length B n (map A B n f v).
165  #A B n v f.
166  nelim v.
167  nnormalize.
168  @.
169  #N H V H2.
170  nnormalize.
171  nrewrite > H2.
172  @.
173nqed.
Note: See TracBrowser for help on using the repository browser.