Changeset 234


Ignore:
Timestamp:
Nov 12, 2010, 2:27:56 PM (9 years ago)
Author:
mulligan
Message:

Division and modulus implemented. All necessary orders on naturals
completed. More operations on bitvectors (and general operations that
apply to all vectors) implemented.

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

Legend:

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

    r232 r234  
     1include "List.ma".
    12include "Vector.ma".
    23include "Nat.ma".
     
    3132  λc: BitVector n.
    3233    zip Bool Bool Bool n exclusive_disjunction b c.
     34   
     35ndefinition complement ≝
     36  λn: Nat.
     37  λb: BitVector n.
     38    map Bool Bool n (negation) b.
    3339
    34 nlet 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     //.
    41 nqed.
     40ndefinition divide_with_remainder ≝
     41  λm, n: Nat.
     42    mk_Cartesian Nat Nat (m ÷ n) (modulus m n).
    4243
    43 ncheck pad.
    44        
     44nlet rec bitvector_of_nat_aux (n: Nat): List Nat ≝
     45  let div_rem ≝ divide_with_remainder n (S (S Z)) in
     46  let div ≝ first Nat Nat div_rem in
     47  let rem ≝ second Nat Nat div_rem in
     48    Empty Nat.
  • Deliverables/D4.1/Matita/Nat.ma

    r233 r234  
     1(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     2(* Nat.ma: Natural numbers and common arithmetical functions.                 *)
     3(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    14include "Cartesian.ma".
    25include "Maybe.ma".
     
    710include "Plogic/connectives.ma".
    811
     12(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     13(* The datatype.                                                              *)
     14(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    915ninductive Nat: Type[0] ≝
    1016  Z: Nat
    1117| S: Nat → Nat.
    1218
     19(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     20(* Orderings.                                                                 *)
     21(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     22
     23ninductive less_than_or_equal_p (n: Nat): Nat → Prop ≝
     24  ltoe_refl: less_than_or_equal_p n n
     25| ltoe_step: ∀m: Nat. less_than_or_equal_p n m → less_than_or_equal_p n (S m).
     26
     27nlet rec less_than_or_equal_b (m: Nat) (n: Nat) on m: Bool ≝
     28  match m with
     29    [ Z ⇒ True
     30    | S o ⇒
     31      match n with
     32        [ Z ⇒ False
     33        | S p ⇒ less_than_or_equal_b o p
     34        ]
     35    ].
     36   
     37notation "n break ≤ m"
     38  non associative with precedence 47
     39  for @{ 'less_than_or_equal $n $m }.
     40 
     41interpretation "Nat less than or equal prop" 'less_than_or_equal n m = (less_than_or_equal_p n m).
     42interpretation "Nat less than or equal bool" 'less_than_or_equal n m = (less_than_or_equal_b n m).
     43
     44ndefinition greater_than_or_equal_p: Nat → Nat → Prop ≝
     45  λm, n: Nat.
     46    n ≤ m.
     47
     48ndefinition greater_than_or_equal_b ≝
     49  λm, n: Nat.
     50    n ≤ m.
     51   
     52notation "n break ≥ m"
     53  non associative with precedence 47
     54  for @{ 'greater_than_or_equal $n $m }.
     55 
     56
     57interpretation "Nat greater than or equal prop" 'greater_than_or_equal n m = (greater_than_or_equal_p n m).
     58interpretation "Nat greater than or equal bool" 'greater_than_or_equal n m = (greater_than_or_equal_b n m).
     59
     60(* Add Boolean versions.                                                      *)
     61ndefinition less_than_p ≝
     62  λm, n: Nat.
     63    m ≤ n ∧ ¬(m = n).
     64   
     65notation "n break < m"
     66  non associative with precedence 47
     67  for @{ 'less_than $n $m }.
     68 
     69interpretation "Nat less than prop" 'less_than n m = (less_than_p n m).
     70
     71ndefinition greater_than_p ≝
     72  λm, n: Nat.
     73    n < m.
     74   
     75notation "n break > m"
     76  non associative with precedence 47
     77  for @{ 'greater_than $n $m }.
     78 
     79interpretation "Nat greater than prop" 'greater_than n m = (greater_than_p n m).
     80
     81(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     82(* Addition and subtraction.                                                  *)
     83(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    1384nlet rec plus (n: Nat) (o: Nat) on n ≝
    1485  match n with
     
    38109 
    39110interpretation "Nat minus" 'minus n m = (minus n m).
     111
     112(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     113(* Multiplication, modulus and division.                                      *)
     114(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    40115   
    41116nlet rec multiplication (n: Nat) (o: Nat) on n ≝
     
    51126interpretation "Nat multiplication" 'times n m = (multiplication n m).
    52127
    53 ninductive 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 
    57 nlet rec less_than_or_equal_b (m: Nat) (n: Nat) on m ≝
    58   match m with
    59     [ Z ⇒ True
    60     | S o ⇒
    61       match n with
    62         [ Z ⇒ False
    63         | S p ⇒ less_than_or_equal_b o p
     128nlet rec division_aux (m: Nat) (n : Nat) (p: Nat) ≝
     129  match n ≤ p with
     130    [ True ⇒ Z
     131    | False ⇒
     132      match m with
     133        [ Z ⇒ Z
     134        | (S q) ⇒ S (division_aux q (n - (S p)) p)
    64135        ]
    65136    ].
    66137   
    67 notation "n break ≤ m"
    68   non associative with precedence 47
    69   for @{ 'less_than_or_equal $n $m }.
    70  
    71 interpretation "Nat less than or equal prop" 'less_than_or_equal n m = (less_than_or_equal_p n m).
    72 interpretation "Nat less than or equal bool" 'less_than_or_equal n m = (less_than_or_equal_b n m).
    73 
    74 ndefinition less_than_p ≝
    75   λm, n: Nat.
    76     m ≤ n ∧ ¬(m = n).
    77    
    78 notation "n break < m"
    79   non associative with precedence 47
    80   for @{ 'less_than $n $m }.
    81  
    82 interpretation "Nat less than prop" 'less_than n m = (less_than_p n m).
    83 
    84 (*
    85 nlet 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 *)
     138ndefinition division ≝
     139  λm, n: Nat.
     140    match n with
     141      [ Z ⇒ S m
     142      | S o ⇒ division_aux m m o
     143      ].
     144     
     145notation "n break ÷ m"
     146  right associative with precedence 47
     147  for @{ 'division $n $m }.
     148 
     149interpretation "Nat division" 'division n m = (division n m).
     150     
     151nlet rec modulus_aux (m: Nat) (n: Nat) (p: Nat) ≝
     152  match n ≤ p with
     153    [ True ⇒ n
     154    | False ⇒
     155      match m with
     156        [ Z ⇒ n
     157        | S o ⇒ modulus_aux o (n - (S p)) p
     158        ]
     159    ].
     160   
     161ndefinition modulus ≝
     162  λm, n: Nat.
     163    match n with
     164      [ Z ⇒ m
     165      | S o ⇒ modulus_aux m m o
     166      ].
     167   
     168notation "n break % m"
     169  right associative with precedence 47
     170  for @{ 'modulus $n $m }.
     171 
     172interpretation "Nat modulus" 'modulus m n = (modulus m n).
     173
     174(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     175(* Greatest common divisor and least common multiple.                         *)
     176(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     177
     178(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     179(* Lemmas.                                                                    *)
     180(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    91181
    92182nlemma less_than_or_equal_zero:
     
    97187  //.
    98188  #N.
    99   //.
     189  napply ltoe_step.
    100190nqed.
    101191
  • Deliverables/D4.1/Matita/Vector.ma

    r233 r234  
    11(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    2 (* Vectors.ma: Fixed length polymorphic vectors, and routine operations on    *)
    3 (*             them.                                                          *)
     2(* Vector.ma: Fixed length polymorphic vectors, and routine operations on     *)
     3(*            them.                                                           *)
    44(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    55
Note: See TracChangeset for help on using the changeset viewer.