Changeset 222


Ignore:
Timestamp:
Nov 8, 2010, 1:53:17 PM (9 years ago)
Author:
mulligan
Message:

Datatype for fixed length lists (vectors) as well as some recursive functions over them (folds, etc.)

File:
1 moved

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/Vectors.ma

    r221 r222  
     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   
     42nlet rec append (A: Type[0]) (n: nat) (m: nat)
     43                (v: Vector A n) (q: Vector A m) on v ≝
     44  match v with
     45    [ Empty ⇒ q
     46    | Cons n hd tl ⇒ Cons n hd (append A n m tl q)
     47    ].
     48
     49(*   
     50nlet rec reverse (A: Type[0]) (n: nat) (v: Vector A n) on v ≝
     51  match v with
     52    [ Empty ⇒ Empty A
     53    | Cons n hd tl ⇒ append
     54   
     55nlemma length_correct:
     56  ∀A: Type[0].
     57  ∀n: nat.
     58  ∀v: Vector A n.
     59    length A n v = n.
     60  #A n v;
     61  nelim v.
     62  nnormalize.
     63  @.
     64  #n0 H V H.
     65  nnormalize.
     66  nrewrite > H.
     67*)
Note: See TracChangeset for help on using the changeset viewer.