Switch to uvalueToZ in lessdef.

2 files changed, 54 insertions, 29 deletions

diff --git a/src/common/Coquplib.v b/src/common/Coquplib.v
index c9361c2..8ad557b 100644
--- a/src/common/Coquplib.v
+++ b/src/common/Coquplib.v
@@ -32,6 +32,8 @@ From coqup Require Import Show.
 From compcert.lib Require Export Coqlib.
 From compcert Require Import Integers.
 
+Local Open Scope Z_scope.
+
 Ltac unfold_rec c := unfold c; fold c.
 
 Ltac solve_by_inverts n :=
@@ -129,16 +131,28 @@ Ltac unfold_constants :=
            end
          end.
 
-Ltac crush := intros; unfold_constants; simpl in *;
-              repeat (clear_obvious; nicify_goals; kill_bools);
-              simpl in *; try discriminate; try congruence; try lia; try assumption.
-
-Global Opaque Nat.div.
-Global Opaque Z.mul.
+Ltac simplify := intros; unfold_constants; simpl in *;
+                 repeat (clear_obvious; nicify_goals; kill_bools);
+                 simpl in *.
 
 Infix "==nat" := eq_nat_dec (no associativity, at level 50).
 Infix "==Z" := Z.eq_dec (no associativity, at level 50).
 
+Ltac liapp :=
+  match goal with
+  | [ |- (?x | ?y) ] =>
+    match (eval compute in (Z.rem y x ==Z 0)) with
+    | left _ => let q := (eval compute in (Z.div y x)) in exists q; reflexivity
+    | _ => idtac
+    end
+  | _ => idtac
+  end.
+
+Ltac crush := simplify; try discriminate; try congruence; try lia; liapp; try assumption.
+
+Global Opaque Nat.div.
+Global Opaque Z.mul.
+
 (* Definition const (A B : Type) (a : A) (b : B) : A := a.
 
 Definition compose (A B C : Type) (f : B -> C) (g : A -> B) (x : A) : C := f (g x). *)
diff --git a/src/common/IntegerExtra.v b/src/common/IntegerExtra.v
index 6bac18d..dcaf3a1 100644
--- a/src/common/IntegerExtra.v
+++ b/src/common/IntegerExtra.v
@@ -70,22 +70,21 @@ Module PtrofsExtra.
 
   Lemma of_int_mod :
     forall x m,
-      Int.signed x mod m = 0 ->
-      Ptrofs.signed (Ptrofs.of_int x) mod m = 0.
+      Int.unsigned x mod m = 0 ->
+      Ptrofs.unsigned (Ptrofs.of_int x) mod m = 0.
   Proof.
     intros.
-    pose proof (Integers.Ptrofs.agree32_of_int eq_refl x) as A.
-    pose proof Ptrofs.agree32_signed.
-    apply H0 in A; try reflexivity.
-    rewrite A. assumption.
+    unfold Ptrofs.of_int.
+    rewrite Ptrofs.unsigned_repr; crush;
+      apply Int.unsigned_range_2.
   Qed.
 
   Lemma mul_mod :
     forall x y m,
       0 < m ->
       (m | Ptrofs.modulus) ->
-      Ptrofs.signed x mod m = 0 ->
-      Ptrofs.signed y mod m = 0 ->
+      Ptrofs.unsigned x mod m = 0 ->
+      Ptrofs.unsigned y mod m = 0 ->
       (Ptrofs.signed (Ptrofs.mul x y)) mod m = 0.
   Proof.
     intros. unfold Ptrofs.mul.
@@ -95,7 +94,6 @@ Module PtrofsExtra.
            | [ _ : _ |- context[if ?x then _ else _] ] => destruct x
            | [ _ : _ |- context[_ mod Ptrofs.modulus mod m] ] =>
              rewrite <- Zmod_div_mod; try lia; try assumption
-           | [ _ : _ |- context[Ptrofs.unsigned _] ] => rewrite Ptrofs.unsigned_signed
            end; try(crush; lia); ptrofs_mod_tac m.
   Qed.
 
@@ -103,8 +101,8 @@ Module PtrofsExtra.
     forall x y m,
       0 < m ->
       (m | Ptrofs.modulus) ->
-      Ptrofs.signed x mod m = 0 ->
-      Ptrofs.signed y mod m = 0 ->
+      Ptrofs.unsigned x mod m = 0 ->
+      Ptrofs.unsigned y mod m = 0 ->
       (Ptrofs.unsigned (Ptrofs.add x y)) mod m = 0.
   Proof.
     intros. unfold Ptrofs.add.
@@ -114,7 +112,6 @@ Module PtrofsExtra.
            | [ _ : _ |- context[if ?x then _ else _] ] => destruct x
            | [ _ : _ |- context[_ mod Ptrofs.modulus mod m] ] =>
              rewrite <- Zmod_div_mod; try lia; try assumption
-           | [ _ : _ |- context[Ptrofs.unsigned _] ] => rewrite Ptrofs.unsigned_signed
            end; try (crush; lia); ptrofs_mod_tac m.
   Qed.
 
@@ -243,22 +240,37 @@ Module IntExtra.
   Ltac int_mod_tac m :=
     repeat (int_mod_match m); lia.
 
-  Lemma mul_mod :
+  Lemma mul_mod1 :
+    forall x y m,
+      0 < m ->
+      (m | Int.modulus) ->
+      Int.unsigned x mod m = 0 ->
+      (Int.unsigned (Int.mul x y)) mod m = 0.
+  Proof.
+    intros. unfold Int.mul.
+    rewrite Int.unsigned_repr_eq.
+
+    repeat match goal with
+           | [ _ : _ |- context[if ?x then _ else _] ] => destruct x
+           | [ _ : _ |- context[_ mod Int.modulus mod m] ] =>
+             rewrite <- Zmod_div_mod; try lia; try assumption
+           end; try (crush; lia); int_mod_tac m.
+  Qed.
+
+  Lemma mul_mod2 :
     forall x y m,
       0 < m ->
       (m | Int.modulus) ->
-      Int.signed x mod m = 0 ->
-      Int.signed y mod m = 0 ->
-      (Int.signed (Int.mul x y)) mod m = 0.
+      Int.unsigned y mod m = 0 ->
+      (Int.unsigned (Int.mul x y)) mod m = 0.
   Proof.
     intros. unfold Int.mul.
-    rewrite Int.signed_repr_eq.
+    rewrite Int.unsigned_repr_eq.
 
     repeat match goal with
            | [ _ : _ |- context[if ?x then _ else _] ] => destruct x
            | [ _ : _ |- context[_ mod Int.modulus mod m] ] =>
              rewrite <- Zmod_div_mod; try lia; try assumption
-           | [ _ : _ |- context[Int.unsigned _] ] => rewrite Int.unsigned_signed
            end; try (crush; lia); int_mod_tac m.
   Qed.
 
@@ -266,18 +278,17 @@ Module IntExtra.
     forall x y m,
       0 < m ->
       (m | Int.modulus) ->
-      Int.signed x mod m = 0 ->
-      Int.signed y mod m = 0 ->
-      (Int.signed (Int.add x y)) mod m = 0.
+      Int.unsigned x mod m = 0 ->
+      Int.unsigned y mod m = 0 ->
+      (Int.unsigned (Int.add x y)) mod m = 0.
   Proof.
     intros. unfold Int.add.
-    rewrite Int.signed_repr_eq.
+    rewrite Int.unsigned_repr_eq.
 
     repeat match goal with
            | [ _ : _ |- context[if ?x then _ else _] ] => destruct x
            | [ _ : _ |- context[_ mod Int.modulus mod m] ] =>
              rewrite <- Zmod_div_mod; try lia; try assumption
-           | [ _ : _ |- context[Int.unsigned _] ] => rewrite Int.unsigned_signed
            end; try (crush; lia); int_mod_tac m.
   Qed.
 End IntExtra.