Changeset 224


Ignore:
Timestamp:
Nov 8, 2010, 5:04:27 PM (9 years ago)
Author:
mulligan
Message:

Changes to bit vectors and vectors.

Location:
Deliverables/D4.1/Matita
Files:
2 edited

Legend:

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

    r223 r224  
     1include "Vectors.ma".
     2
     3include "arithmetics/nat.ma".
     4include "basics/bool.ma".
     5
     6ndefinition BitVector ≝ λn: nat. Vector bool n.
     7
     8ndefinition conjunction ≝
     9  λn: nat.
     10  λv, q: BitVector n.
     11    fold_right ∧ true v q.
  • Deliverables/D4.1/Matita/Vectors.ma

    r223 r224  
    22(* Vectors.ma: Fixed length bitvectors, and routine operations on them.       *)
    33(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     4
     5include "Cartesian.ma".
     6include "List.ma".
    47
    58include "logic/pts.ma".
     
    1215ninductive Vector (A: Type[0]): nat → Type[0] ≝
    1316  Empty: Vector A 0
    14 | Cons: ∀n: nat. A → Vector A n → Vector A (n + 1).
     17| Cons: ∀n: nat. A → Vector A n → Vector A (S n).
    1518
    1619nlet rec map (A: Type[0]) (B: Type[0]) (n: nat) (f: A → B) (v: Vector A n) on v ≝
     
    3740  match v with
    3841    [ Empty ⇒ 0
    39     | Cons n hd tl ⇒ 1 + length A n tl
     42    | Cons n hd tl ⇒ S (length A n tl)
    4043    ].
    41    
    42 (*   
    43 nlet 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)
     44
     45nlet rec from_list (A: Type[0]) (l: List A) on l ≝
     46  match l with
     47    [ Empty ⇒ Empty A
     48    | Cons hd tl ⇒ Cons (length A tl) hd (from_list A tl)
    4849    ].
    49 *)
    50 
    51 (*   
    52 nlet 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    
    57 nlemma 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 TracChangeset for help on using the changeset viewer.