Changeset 228


Ignore:
Timestamp:
Nov 9, 2010, 3:27:30 PM (9 years ago)
Author:
mulligan
Message:

Conjunction, disjunction and 'xorjunction' implemented on bitvectors.
Lots of supporting datatypes. Vectors.ma includes some diabolical
dependent type hackery due to Wilmer.

Location:
Deliverables/D4.1/Matita
Files:
6 added
2 moved

Legend:

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

    r224 r228  
    1 include "Vectors.ma".
     1include "Vector.ma".
     2include "Nat.ma".
     3include "Bool.ma".
    24
    3 include "arithmetics/nat.ma".
    4 include "basics/bool.ma".
     5ndefinition BitVector ≝ λn: Nat. Vector Bool n.
    56
    6 ndefinition BitVector ≝ λn: nat. Vector bool n.
    7 
     7ndefinition zero ≝
     8  λn: Nat.
     9    replicate Bool n False.
     10   
    811ndefinition conjunction ≝
    9   λn: nat.
    10   λv, q: BitVector n.
    11     fold_right ∧ true v q.
     12  λn: Nat.
     13  λb: BitVector n.
     14  λc: BitVector n.
     15    zip Bool Bool Bool n conjunction b c.
     16   
     17ndefinition inclusive_disjunction ≝
     18  λn: Nat.
     19  λb: BitVector n.
     20  λc: BitVector n.
     21    zip Bool Bool Bool n inclusive_disjunction b c.
     22   
     23ndefinition exclusive_disjunction ≝
     24  λn: Nat.
     25  λb: BitVector n.
     26  λc: BitVector n.
     27    zip Bool Bool Bool n exclusive_disjunction b c.
     28   
     29   
  • Deliverables/D4.1/Matita/Vector.ma

    r224 r228  
    44
    55include "Cartesian.ma".
    6 include "List.ma".
     6include "Nat.ma".
     7(* include "List.ma". *)
    78
    89include "logic/pts.ma".
    9 include "basics/eq.ma".
    10 include "basics/bool.ma".
    11 include "arithmetics/nat.ma".
    12 include "nat/plus.ma".
    13 include "nat/minus.ma".
     10include "Plogic/equality.ma".
    1411
    15 ninductive Vector (A: Type[0]): nat → Type[0] ≝
    16   Empty: Vector A 0
    17 | Cons: ∀n: nat. A → Vector A n → Vector A (S n).
     12ninductive Vector (A: Type[0]): Nat → Type[0] ≝
     13  Empty: Vector A Z
     14| Cons: ∀n: Nat. A → Vector A n → Vector A (S n).
    1815
    19 nlet rec map (A: Type[0]) (B: Type[0]) (n: nat) (f: A → B) (v: Vector A n) on v ≝
     16notation "hvbox(hd break :: tl)"
     17  right associative with precedence 52
     18  for @{ 'Cons $hd $tl }.
     19 
     20interpretation "Vector cons" 'Cons hd tl = (Cons ? ? hd tl).
     21
     22nlet rec map (A: Type[0]) (B: Type[0]) (n: Nat)
     23             (f: A → B) (v: Vector A n) on v ≝
    2024  match v with
    2125    [ Empty ⇒ Empty B
    22     | Cons n hd tl ⇒ Cons B n (f hd) (map A B n f tl)
     26    | Cons n hd tl ⇒ (f hd) :: (map A B n f tl)
    2327    ].
    2428   
    25 nlet rec fold_right (A: Type[0]) (B: Type[0]) (n: nat)
     29nlet rec fold_right (A: Type[0]) (B: Type[0]) (n: Nat)
    2630                    (f: A → B → B) (x: B) (v: Vector A n) on v ≝
    2731  match v with
     
    3034    ].
    3135   
    32 nlet rec fold_left (A: Type[0]) (B: Type[0]) (n: nat)
     36nlet rec fold_left (A: Type[0]) (B: Type[0]) (n: Nat)
    3337                    (f: A → B → A) (x: A) (v: Vector B n) on v ≝
    3438  match v with
     
    3741    ].
    3842   
    39 nlet rec length (A: Type[0]) (n: nat) (v: Vector A n) on v ≝
     43nlet rec length (A: Type[0]) (n: Nat) (v: Vector A n) on v ≝
    4044  match v with
    41     [ Empty ⇒ 0
     45    [ Empty ⇒ Z
    4246    | Cons n hd tl ⇒ S (length A n tl)
    4347    ].
    4448
    45 nlet 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)
     49nlet rec replicate (A: Type[0]) (n: Nat) (h: A) on n
     50  match n return λn. Vector A n with
     51    [ Z ⇒ Empty A
     52    | S m ⇒ h :: (replicate A m h)
    4953    ].
     54   
     55nlemma eq_rect_Type0_r :
     56  ∀A: Type[0].
     57  ∀a:A.
     58  ∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
     59  #A;
     60  #a;
     61  #P;
     62  #H;
     63  #x;
     64  #p;
     65  ngeneralize in match H;
     66  ngeneralize in match P;
     67  ncases p;
     68  //;
     69nqed.
     70
     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 hd2 tl2 ⇒
     80            λe: S n = S m.
     81              Cons C n (f hd hd2) (zip A B C n f tl ?)
     82        ]
     83    ])
     84    (refl ? n).
     85      ##
     86        [ #e;
     87          ndestruct (e);
     88          ##
     89        | ndestruct (e);
     90          napply tl2
     91          ##
     92        ]
     93nqed.
Note: See TracChangeset for help on using the changeset viewer.