Changeset 234 for Deliverables/D4.1/Matita/Nat.ma

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.

File:

• Deliverables/D4.1/Matita/Nat.ma (modified) (5 diffs)

Deliverables/D4.1/Matita/Nat.ma

@@ +1 @@
+(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
+(* Nat.ma: Natural numbers and common arithmetical functions.                 *)
+(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
 include "Cartesian.ma".
 include "Maybe.ma".
@@ -7 +10 @@
 include "Plogic/connectives.ma".
 
+(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
+(* The datatype.                                                              *)
+(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
 ninductive Nat: Type[0] ≝
   Z: Nat
 | S: Nat → Nat.
 
+(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
+(* Orderings.                                                                 *)
+(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
+
+ninductive less_than_or_equal_p (n: Nat): Nat → Prop ≝
+  ltoe_refl: less_than_or_equal_p n n
+| ltoe_step: ∀m: Nat. less_than_or_equal_p n m → less_than_or_equal_p n (S m).
+
+nlet rec less_than_or_equal_b (m: Nat) (n: Nat) on m: Bool ≝
+  match m with
+    [ Z ⇒ True
+    | S o ⇒
+      match n with
+        [ Z ⇒ False
+        | S p ⇒ less_than_or_equal_b o p
+        ]
+    ].
+    
+notation "n break ≤ m"
+  non associative with precedence 47
+  for @{ 'less_than_or_equal $n $m }.
+  
+interpretation "Nat less than or equal prop" 'less_than_or_equal n m = (less_than_or_equal_p n m).
+interpretation "Nat less than or equal bool" 'less_than_or_equal n m = (less_than_or_equal_b n m).
+
+ndefinition greater_than_or_equal_p: Nat → Nat → Prop ≝
+  λm, n: Nat.
+    n ≤ m.
+
+ndefinition greater_than_or_equal_b ≝
+  λm, n: Nat.
+    n ≤ m.
+    
+notation "n break ≥ m"
+  non associative with precedence 47
+  for @{ 'greater_than_or_equal $n $m }.
+  
+
+interpretation "Nat greater than or equal prop" 'greater_than_or_equal n m = (greater_than_or_equal_p n m).
+interpretation "Nat greater than or equal bool" 'greater_than_or_equal n m = (greater_than_or_equal_b n m).
+
+(* Add Boolean versions.                                                      *)
+ndefinition less_than_p ≝
+  λm, n: Nat.
+    m ≤ n ∧ ¬(m = n).
+    
+notation "n break < m"
+  non associative with precedence 47
+  for @{ 'less_than $n $m }.
+  
+interpretation "Nat less than prop" 'less_than n m = (less_than_p n m).
+
+ndefinition greater_than_p ≝
+  λm, n: Nat.
+    n < m.
+    
+notation "n break > m"
+  non associative with precedence 47
+  for @{ 'greater_than $n $m }.
+  
+interpretation "Nat greater than prop" 'greater_than n m = (greater_than_p n m).
+
+(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
+(* Addition and subtraction.                                                  *)
+(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
 nlet rec plus (n: Nat) (o: Nat) on n ≝
   match n with
@@ -38 +109 @@
   
 interpretation "Nat minus" 'minus n m = (minus n m).
+
+(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
+(* Multiplication, modulus and division.                                      *)
+(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
 nlet rec multiplication (n: Nat) (o: Nat) on n ≝
@@ -51 +126 @@
 interpretation "Nat multiplication" 'times n m = (multiplication n m).
 
-ninductive less_than_or_equal_p (n: Nat): Nat → Prop ≝
-  ltoe_refl: less_than_or_equal_p n n
-| ltoe_step: ∀m: Nat. less_than_or_equal_p n m → less_than_or_equal_p n (S m).
-
-nlet rec less_than_or_equal_b (m: Nat) (n: Nat) on m ≝
-  match m with
-    [ Z ⇒ True
-    | S o ⇒
-      match n with
-        [ Z ⇒ False
-        | S p ⇒ less_than_or_equal_b o p
+nlet rec division_aux (m: Nat) (n : Nat) (p: Nat) ≝
+  match n ≤ p with
+    [ True ⇒ Z
+    | False ⇒
+      match m with
+        [ Z ⇒ Z
+        | (S q) ⇒ S (division_aux q (n - (S p)) p)
         ]
     ].
     
-notation "n break ≤ m"
-  non associative with precedence 47
-  for @{ 'less_than_or_equal $n $m }.
-  
-interpretation "Nat less than or equal prop" 'less_than_or_equal n m = (less_than_or_equal_p n m).
-interpretation "Nat less than or equal bool" 'less_than_or_equal n m = (less_than_or_equal_b n m).
-
-ndefinition less_than_p ≝
-  λm, n: Nat.
-    m ≤ n ∧ ¬(m = n).
-    
-notation "n break < m"
-  non associative with precedence 47
-  for @{ 'less_than $n $m }.
-  
-interpretation "Nat less than prop" 'less_than n m = (less_than_p n m).
-
-(*
-nlet rec greatest_common_divisor (m: Nat) (n: Nat) on n ≝
-  match n with
-    [ Z ⇒ m
-    | S o ⇒ greatest_common_divisor n (modulus m n)
-    ].
-*)
+ndefinition division ≝
+  λm, n: Nat.
+    match n with
+      [ Z ⇒ S m
+      | S o ⇒ division_aux m m o
+      ].
+      
+notation "n break ÷ m"
+  right associative with precedence 47
+  for @{ 'division $n $m }.
+  
+interpretation "Nat division" 'division n m = (division n m).
+      
+nlet rec modulus_aux (m: Nat) (n: Nat) (p: Nat) ≝
+  match n ≤ p with
+    [ True ⇒ n
+    | False ⇒
+      match m with
+        [ Z ⇒ n
+        | S o ⇒ modulus_aux o (n - (S p)) p
+        ]
+    ].
+    
+ndefinition modulus ≝
+  λm, n: Nat.
+    match n with
+      [ Z ⇒ m
+      | S o ⇒ modulus_aux m m o
+      ].
+    
+notation "n break % m"
+  right associative with precedence 47
+  for @{ 'modulus $n $m }.
+  
+interpretation "Nat modulus" 'modulus m n = (modulus m n).
+
+(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
+(* Greatest common divisor and least common multiple.                         *)
+(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
+
+(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
+(* Lemmas.                                                                    *)
+(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
 
 nlemma less_than_or_equal_zero:
@@ -97 +187 @@
   //.
   #N.
-  //.
+  napply ltoe_step.
 nqed.