Changeset 230


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

Lots of work from today.

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

Legend:

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

    r228 r230  
    44
    55ndefinition BitVector ≝ λn: Nat. Vector Bool n.
     6ndefinition Bit ≝ BitVector (S Z).
     7ndefinition Nibble ≝ BitVector (S (S (S (S Z)))).
     8ndefinition Byte7 ≝ BitVector (S (S (S (S (S (S (S Z))))))).
     9ndefinition Byte ≝ BitVector (S (S (S (S (S (S (S (S Z)))))))).
     10ndefinition Word ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))).
    611
    712ndefinition zero ≝
     
    2631  λc: BitVector n.
    2732    zip Bool Bool Bool n exclusive_disjunction b c.
    28    
    29    
  • Deliverables/D4.1/Matita/List.ma

    r229 r230  
    22include "Nat.ma".
    33include "Util.ma".
     4
     5include "Plogic/equality.ma".
    46
    57ninductive List (A: Type[0]): Type[0] ≝
     
    1113  for @{ 'Cons $hd $tl }.
    1214
    13 interpretation "Empty" 'Empty = (Empty ?).
    14 interpretation "Cons" 'Cons = (Cons ?).
     15interpretation "List empty" 'Empty = (Empty ?).
     16interpretation "List cons" 'Cons = (Cons ?).
    1517 
    1618notation "[ list0 x sep ; ]"
     
    2729  match l with
    2830    [ Empty ⇒ m
    29     | Cons hd tl ⇒ hd :: (append A tl l)
     31    | Cons hd tl ⇒ hd :: (append A tl m)
    3032    ].
    3133   
     
    3436  for @{ 'append $l $r }.
    3537 
    36 interpretation "Append" 'append = (append ?).
     38interpretation "List append" 'append = (append ?).
    3739 
    3840nlet rec fold_right (A: Type[0]) (B: Type[0])
     
    9092    | S o ⇒ a :: replicate A o a
    9193    ].
     94   
     95nlemma append_empty:
     96  ∀A: Type[0].
     97  ∀l: List A.
     98    l @ (Empty A) = l.
     99  #A l.
     100  nelim l.
     101  nnormalize.
     102  @.
     103  #H L H2.
     104  nnormalize.
     105  nrewrite > H2.
     106  @.
     107nqed.
     108
     109nlemma append_associative:
     110  ∀A: Type[0].
     111  ∀l,m,n: List A.
     112    l @ (m @ n) = (l @ m) @ n.
     113  #A l m n.
     114  nelim l.
     115  nnormalize.
     116  @.
     117  #H L H2.
     118  nnormalize.
     119  nrewrite > H2.
     120  @.
     121nqed.
     122   
     123nlemma reverse_append:
     124  ∀A: Type[0].
     125  ∀l, m: List A.
     126    reverse A (l @ m) = reverse A m @ reverse A l.
     127  #A l m.
     128  nelim l.
     129  nnormalize.
     130  napplyS append_empty.
     131  #H L A.
     132  nnormalize.
     133  nrewrite > A.
     134  napplyS append_associative.
     135nqed.
     136
     137nlemma length_append:
     138  ∀A: Type[0].
     139  ∀l, m: List A.
     140    length A (l @ m) = length A l + length A m.
     141  #A l m.
     142  nelim l.
     143  nnormalize.
     144  @.
     145  #H L H2.
     146  nnormalize.
     147  nrewrite > H2.
     148  @.
     149nqed.
     150
     151(* 
     152nlemma length_reverse:
     153  ∀A: Type[0].
     154  ∀l: List A.
     155    length A (reverse A l) = length A l.
     156  #A l.
     157  nelim l.
     158  nnormalize.
     159  @.
     160  #H L H2.
     161  nnormalize.
     162  napplyS length_append.
     163   
     164nlemma reverse_reverse:
     165  ∀A: Type[0].
     166  ∀l: List A.
     167    reverse A (reverse A l) = l.
     168  #A l.
     169  nelim l.
     170  nnormalize.
     171  @.
     172  #H L H2.
     173  nnormalize.
     174*)
  • Deliverables/D4.1/Matita/Nat.ma

    r228 r230  
    108108nqed.
    109109
    110 nlemma multiplication_zero:
     110nlemma multiplication_zero_right_neutral:
    111111  ∀m: Nat.
    112112    m * Z = Z.
     
    151151  napplyS multiplication_succ.
    152152nqed.
    153  
     153
     154nlemma multiplication_succ_zero_left_neutral:
     155  ∀m: Nat.
     156    (S Z) * m = m.
     157  #m.
     158  nelim m.
     159  nnormalize.
     160  @.
     161  #N H.
     162  nnormalize.
     163  napplyS succ_plus.
     164nqed.
     165
     166nlemma multiplication_succ_zero_right_neutral:
     167  ∀m: Nat.
     168    m * (S Z) = m.
     169  #m.
     170  nelim m.
     171  nnormalize.
     172  @.
     173  #N H.
     174  nnormalize.
     175  nrewrite > H.
     176  @.
     177nqed.
     178
     179nlemma multiplication_distributes_right_plus:
     180  ∀m, n, o: Nat.
     181    (m + n) * o = m * o + n * o.
     182  #m n o.
     183  nelim m.
     184  nnormalize.
     185  @.
     186  #N H.
     187  nnormalize.
     188  nrewrite > H.
     189  napplyS plus_associative.
     190nqed.
     191
     192nlemma multiplication_distributes_left_plus:
     193  ∀m, n, o: Nat.
     194    o * (m + n) = o * m + o * n.
     195  #m n o.
     196  napplyS multiplication_symmetrical.
     197nqed.
     198
     199nlemma mutliplication_associative:
     200  ∀m, n, o: Nat.
     201    m * (n * o) = (m * n) * o.
     202  #m n o.
     203  nelim m.
     204  nnormalize.
     205  @.
     206  #N H.
     207  nnormalize.
     208  nrewrite > H.
     209  napplyS multiplication_distributes_right_plus.
     210nqed.
     211
     212nlemma minus_minus:
     213  ∀n: Nat.
     214    n - n = Z.
     215  #n.
     216  nelim n.
     217  nnormalize.
     218  @.
     219  #N H.
     220  nnormalize.
     221  nrewrite > H.
     222  @.
     223nqed.
     224
     225(*
     226nlemma succ_injective:
     227  ∀m, n: Nat.
     228    S m = S n → m = n.
     229  #m n.
     230  nelim m.
     231  #H.
     232  ninversion H.
     233  #H.
     234  ndestruct
     235
     236nlemma plus_minus_associate:
     237  ∀m, n, o: Nat.
     238    (m + n) - o = m + (n - o).
     239  #m n o.
     240  nelim m.
     241  nnormalize.
     242  @.
     243  #N H.
     244 
     245
     246nlemma plus_minus_inverses:
     247  ∀m, n: Nat.
     248    (m + n) - n = m.
     249  #m n.
     250  nelim m.
     251  nnormalize.
     252  napply minus_minus.
     253  #N H.
     254*)
  • 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.