From 1d8afa5949cd192620e4649ae32df49bca4da3f8 Mon Sep 17 00:00:00 2001 From: James Pollard Date: Thu, 2 Jul 2020 21:57:03 +0100 Subject: Switch to uvalueToZ in lessdef. --- src/common/Coquplib.v | 26 ++++++++++++++++----- src/common/IntegerExtra.v | 57 ++++++++++++++++++++++++++++------------------- 2 files changed, 54 insertions(+), 29 deletions(-) (limited to 'src/common') 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. -- cgit