source: Deliverables/D4.1/Matita/Vectors.ma @ 223

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

File for bitvector specific stuff added.

File size: 1.8 KB
Line 
1(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
2(* Vectors.ma: Fixed length bitvectors, and routine operations on them.       *)
3(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
4
5include "logic/pts.ma".
6include "basics/eq.ma".
7include "basics/bool.ma".
8include "arithmetics/nat.ma".
9include "nat/plus.ma".
10include "nat/minus.ma".
11
12ninductive Vector (A: Type[0]): nat → Type[0] ≝
13  Empty: Vector A 0
14| Cons: ∀n: nat. A → Vector A n → Vector A (n + 1).
15
16nlet rec map (A: Type[0]) (B: Type[0]) (n: nat) (f: A → B) (v: Vector A n) on v ≝
17  match v with
18    [ Empty ⇒ Empty B
19    | Cons n hd tl ⇒ Cons B n (f hd) (map A B n f tl)
20    ].
21   
22nlet rec fold_right (A: Type[0]) (B: Type[0]) (n: nat)
23                    (f: A → B → B) (x: B) (v: Vector A n) on v ≝
24  match v with
25    [ Empty ⇒ x
26    | Cons n hd tl ⇒ f hd (fold_right A B n f x tl)
27    ].
28   
29nlet rec fold_left (A: Type[0]) (B: Type[0]) (n: nat)
30                    (f: A → B → A) (x: A) (v: Vector B n) on v ≝
31  match v with
32    [ Empty ⇒ x
33    | Cons n hd tl ⇒ f (fold_left A B n f x tl) hd
34    ].
35   
36nlet rec length (A: Type[0]) (n: nat) (v: Vector A n) on v ≝
37  match v with
38    [ Empty ⇒ 0
39    | Cons n hd tl ⇒ 1 + length A n tl
40    ].
41   
42(*   
43nlet rec append (A: Type[0]) (n: nat) (m: nat)
44                (v: Vector A n) (q: Vector A m) on v ≝
45  match v with
46    [ Empty ⇒ q
47    | Cons n hd tl ⇒ Cons ? n hd (append A n m tl q)
48    ].
49*)
50
51(*   
52nlet rec reverse (A: Type[0]) (n: nat) (v: Vector A n) on v ≝
53  match v with
54    [ Empty ⇒ Empty A
55    | Cons n hd tl ⇒ append
56   
57nlemma length_correct:
58  ∀A: Type[0].
59  ∀n: nat.
60  ∀v: Vector A n.
61    length A n v = n.
62  #A n v;
63  nelim v.
64  nnormalize.
65  @.
66  #n0 H V H.
67  nnormalize.
68  nrewrite > H.
69*)
Note: See TracBrowser for help on using the repository browser.