Changeset 14 for C-semantics/extralib.ma

Timestamp:

Jul 21, 2010, 3:08:58 PM (11 years ago)

Author:

campbell

Message:

Make Integers.ma respect bounds again, and reenable the rest of Mem.ma.

File:

• C-semantics/extralib.ma (modified) (3 diffs)

C-semantics/extralib.ma

@@ -649 +649 @@
     | pos m ⇒ natp_to_Z (snd ?? (divide n m))
     | neg m ⇒ match divide n m with [ mk_pair q r ⇒
-                match r with [ pzero ⇒ OZ | _ ⇒ y-(natp_to_Z r) ] ]
+                match r with [ pzero ⇒ OZ | _ ⇒ y+(natp_to_Z r) ] ]
     ]
   | neg n ⇒
@@ -655 +655 @@
     [ OZ ⇒ OZ
     | pos m ⇒ match divide n m with [ mk_pair q r ⇒
-                match r with [ pzero ⇒ OZ | _ ⇒ y+(natp_to_Z r) ] ]
+                match r with [ pzero ⇒ OZ | _ ⇒ y-(natp_to_Z r) ] ]
     | neg m ⇒ natp_to_Z (snd ?? (divide n m))
     ]
@@ -664 +664 @@
 interpretation "integer division" 'divide m n = (divZ m n).
 interpretation "integer modulus" 'module m n = (modZ m n).
+
+nlemma Zminus_Zlt: ∀x,y:Z. y>0 → x-y < x.
+#x y; ncases y;
+##[ #H; napply (False_ind … H);
+##| #m; #_; ncases x; //; #n;
+    nwhd in ⊢ (?%?);
+    nlapply (pos_compare_to_Prop n m);
+    ncases (pos_compare n m); /2/;
+    #lt; nwhd; nrewrite < (minus_Sn_m … lt); /2/;
+##| #m H; napply (False_ind … H);
+##] nqed.
+
+nlemma pos_compare_lt: ∀n,m:Pos. n<m → pos_compare n m = LT.
+#n m lt; nlapply (pos_compare_to_Prop n m); ncases (pos_compare n m);
+##[ //;
+##| ##2,3: #H; napply False_ind; napply (absurd ? lt ?); /3/;
+##] nqed.
+
+ntheorem modZ_lt_mod: ∀x,y:Z. y>0 → 0 ≤ x \mod y ∧ x \mod y < y.
+#x y; ncases y;
+##[ #H; napply (False_ind … H);
+##| #m; #_; ncases x;
+  ##[ @;//;
+  ##| #n; nwhd in ⊢ (?(??%)(?%?)); nlapply (refl ? (divide n m));
+      ncases (divide n m) in ⊢ (???% → %); #dv md H;
+      nelim (divide_ok … H); #e l; nelim l; /2/;
+  ##| #n; nwhd in ⊢ (?(??%)(?%?)); nlapply (refl ? (divide n m));
+      ncases (divide n m) in ⊢ (???% → %); #dv md H;
+      nelim (divide_ok … H); #e l; nelim l;
+      ##[ /2/;
+      ##| #md' m' l'; @;
+        ##[ nwhd in ⊢ (??%); nrewrite > (pos_compare_n_m_m_n …);
+            nrewrite > (pos_compare_lt … l'); //;
+        ##| /2/;
+        ##]
+      ##]
+  ##]
+##| #m H; napply (False_ind … H);
+##] nqed.