Ignore:
Timestamp:
Nov 10, 2010, 5:26:08 PM (9 years ago)
Author:
mulligan
Message:

Lots of work from today.

File:
1 edited

Legend:

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

    r229 r230  
    66include "Nat.ma".
    77include "Util.ma".
    8 (* include "List.ma". *)
     8include "List.ma".
    99
    1010include "logic/pts.ma".
     
    5858  ∀a:A.
    5959  ∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
    60   #A;
    61   #a;
    62   #P;
    63   #H;
    64   #x;
    65   #p;
    66   ngeneralize in match H;
    67   ngeneralize in match P;
    68   ncases p;
    69   //;
     60  #A a P H x p.
     61  ngeneralize in match H.
     62  ngeneralize in match P.
     63  ncases p.
     64  //.
    7065nqed.
    7166
     
    9287        ]
    9388nqed.
     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 TracChangeset for help on using the changeset viewer.