Ignore:
Timestamp:
Nov 11, 2010, 4:56:59 PM (10 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'?

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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:
Note: See TracChangeset for help on using the changeset viewer.