Changeset 232


Ignore:
Timestamp:
Nov 11, 2010, 4:56:59 PM (9 years ago)
Author:
mulligan
Message:

Lots of work from today. Writing bitvector library is harder than it
looks. Not quite sure what Matita has done with `pad'?

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

Legend:

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

    r231 r232  
    3232    zip Bool Bool Bool n exclusive_disjunction b c.
    3333
    34 nlet rec pad (n: Nat) (m: Nat) (b: BitVector n) (p: less_than_or_equal n m) ≝
     34nlet rec pad (n: Nat) (m: Nat) (b: BitVector n) (p: less_than_or_equal_p n m): (BitVector (n + m)) ≝
     35  match m with
     36    [ Z ⇒ ?
     37    | S o ⇒ ?
     38    ].
     39   
     40    //.
     41nqed.
     42
     43ncheck pad.
    3544       
  • Deliverables/D4.1/Matita/Bool.ma

    r228 r232  
    4848    [ True ⇒ False
    4949    | False ⇒ True
    50     ].
     50    ]. 
     51 
  • Deliverables/D4.1/Matita/Nat.ma

    r231 r232  
    55include "logic/pts.ma".
    66include "Plogic/equality.ma".
     7include "Plogic/connectives.ma".
    78
    89ninductive Nat: Type[0] ≝
     
    5051interpretation "Nat multiplication" 'times n m = (multiplication n m).
    5152
    52 nlet rec less_than_or_equal (n: Nat) (m: Nat) ≝
    53   match n with
     53ninductive less_than_or_equal_p (n: Nat): Nat → Prop ≝
     54  ltoe_refl: less_than_or_equal_p n n
     55| ltoe_step: ∀m: Nat. less_than_or_equal_p n m → less_than_or_equal_p n (S m).
     56
     57nlet rec less_than_or_equal_b (m: Nat) (n: Nat) on m ≝
     58  match m with
    5459    [ Z ⇒ True
    5560    | S o ⇒
    56       match m with
     61      match n with
    5762        [ Z ⇒ False
    58         | S p ⇒ less_than_or_equal o p
     63        | S p ⇒ less_than_or_equal_b o p
    5964        ]
    6065    ].
     
    6469  for @{ 'less_than_or_equal $n $m }.
    6570 
    66 interpretation "Nat less than or equal" 'less_than_or_equal n m = (less_than_or_equal n m).
     71interpretation "Nat less than or equal prop" 'less_than_or_equal n m = (less_than_or_equal_p n m).
     72interpretation "Nat less than or equal bool" 'less_than_or_equal n m = (less_than_or_equal_b n m).
     73
     74ndefinition less_than_p ≝
     75  λm, n: Nat.
     76    m ≤ n ∧ ¬(m = n).
     77   
     78notation "n break < m"
     79  non associative with precedence 47
     80  for @{ 'less_than $n $m }.
     81 
     82interpretation "Nat less than prop" 'less_than n m = (less_than_p n m).
     83
     84(*
     85nlet rec greatest_common_divisor (m: Nat) (n: Nat) on n ≝
     86  match n with
     87    [ Z ⇒ m
     88    | S o ⇒ greatest_common_divisor n (modulus m n)
     89    ].
     90*)
     91
     92nlemma less_than_or_equal_zero:
     93  ∀n: Nat.
     94    Z ≤ n.
     95  #n.
     96  nelim n.
     97  //.
     98  #N.
     99  //.
     100nqed.
     101
     102(*
     103nlemma less_than_or_equal_injective:
     104  ∀m, n: Nat.
     105    S m ≤ S n → m ≤ n.
     106  #m n.
     107  nelim m.
     108  #H.
     109  napplyS less_than_or_equal_zero.
     110  #N H H2.
     111  ndestruct.
     112
     113nlemma less_than_or_equal_zero_equal_zero:
     114  ∀m: Nat.
     115    m ≤ Z → m = Z.
     116  #m.
     117  nelim m.
     118  //.
     119  #N H H2.
     120  nnormalize.
     121*)
     122
     123nlemma less_than_or_equal_reflexive:
     124  ∀n: Nat.
     125    n ≤ n.
     126  #n.
     127  nelim n.
     128  nnormalize.
     129  @.
     130  #N H.
     131  nnormalize.
     132  //.
     133nqed.
     134
     135(*
     136nlemma less_than_or_equal_succ:
     137  ∀m, n: Nat.
     138    S m ≤ n → m ≤ n.
     139  #m n.
     140  nelim m.
     141  #H.
     142  napplyS less_than_or_equal_zero.
     143  #N H H2.
     144  //.
     145  napplyS H.
     146
     147
     148nlemma less_than_or_equal_transitive:
     149  ∀m, n, o: Nat.
     150    m ≤ n ∧ n ≤ o → m ≤ o.
     151  #m n o.
     152  nelim m.
     153  #H.
     154  napply less_than_or_equal_zero.
     155  #N H H2.
     156  nnormalize.
     157  #;
     158*)
    67159
    68160nlemma plus_zero:
  • Deliverables/D4.1/Matita/Vector.ma

    r231 r232  
    165165    ].
    166166
     167(*
    167168nlet rec from_list (A: Type[0]) (l: List A) on l ≝
    168169  match l return λl. Vector A (length A l) with
     
    172173    //.
    173174nqed.
     175*)
    174176
    175177(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
     
    248250  @.
    249251nqed.
    250 
    251 nlemma from_list_to_list_left_inverse:
    252   ∀A: Type[0].
    253   ∀l: List A.
    254     to_list A (length A l) (from_list A l) = l.
Note: See TracChangeset for help on using the changeset viewer.