diff options
Diffstat (limited to 'src/common')
| -rw-r--r-- | src/common/Coquplib.v | 60 | ||||
| -rw-r--r-- | src/common/IntegerExtra.v | 134 | ||||
| -rw-r--r-- | src/common/Monad.v | 4 | ||||
| -rw-r--r-- | src/common/ZExtra.v | 15 |
4 files changed, 183 insertions, 30 deletions
diff --git a/src/common/Coquplib.v b/src/common/Coquplib.v index c9361c2..469eddc 100644 --- a/src/common/Coquplib.v +++ b/src/common/Coquplib.v @@ -32,6 +32,29 @@ From coqup Require Import Show. From compcert.lib Require Export Coqlib. From compcert Require Import Integers. +Local Open Scope Z_scope. + +(* This tactic due to Clement Pit-Claudel with some minor additions by JDP to + allow the result to be named: https://pit-claudel.fr/clement/MSc/#org96a1b5f *) +Inductive Learnt {A: Type} (a: A) := + | AlreadyKnown : Learnt a. + +Ltac learn_tac fact name := + lazymatch goal with + | [ H: Learnt fact |- _ ] => + fail 0 "fact" fact "has already been learnt" + | _ => let type := type of fact in + lazymatch goal with + | [ H: @Learnt type _ |- _ ] => + fail 0 "fact" fact "of type" type "was already learnt through" H + | _ => let learnt := fresh "Learn" in + pose proof (AlreadyKnown fact) as learnt; pose proof fact as name + end + end. + +Tactic Notation "learn" constr(fact) := let name := fresh "H" in learn_tac fact name. +Tactic Notation "learn" constr(fact) "as" simple_intropattern(name) := learn_tac fact name. + Ltac unfold_rec c := unfold c; fold c. Ltac solve_by_inverts n := @@ -49,10 +72,11 @@ Ltac invert x := inversion x; subst; clear x. Ltac destruct_match := match goal with | [ |- context[match ?x with | _ => _ end ] ] => destruct x end. -Ltac clear_obvious := +Ltac nicify_hypotheses := repeat match goal with | [ H : ex _ |- _ ] => invert H | [ H : Some _ = Some _ |- _ ] => invert H + | [ H : ?x = ?x |- _ ] => clear H | [ H : _ /\ _ |- _ ] => invert H end. @@ -129,16 +153,38 @@ 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. +Ltac substpp := + repeat match goal with + | [ H1 : ?x = Some _, H2 : ?x = Some _ |- _ ] => + let EQ := fresh "EQ" in + learn H1 as EQ; rewrite H2 in EQ; invert EQ + | _ => idtac + end. -Global Opaque Nat.div. -Global Opaque Z.mul. +Ltac simplify := intros; unfold_constants; simpl in *; + repeat (nicify_hypotheses; nicify_goals; kill_bools; substpp); + simpl in *. Infix "==nat" := eq_nat_dec (no associativity, at level 50). Infix "==Z" := Z.eq_dec (no associativity, at level 50). +Ltac liapp := + repeat 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). *) @@ -189,3 +235,5 @@ Definition debug_show {A B : Type} `{Show A} (a : A) (b : B) : B := Definition debug_show_msg {A B : Type} `{Show A} (s : string) (a : A) (b : B) : B := let unused := debug_print (s ++ show a) in b. + +Notation "f $ x" := (f x) (at level 60, right associativity, only parsing). diff --git a/src/common/IntegerExtra.v b/src/common/IntegerExtra.v index 6bac18d..8e32c2c 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. @@ -202,7 +199,7 @@ Ltac ptrofs := end. Module IntExtra. - + Import Int. Ltac int_mod_match m := match goal with | [ H : ?x = 0 |- context[?x] ] => rewrite H @@ -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,92 @@ 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. + + Definition ofbytes (a b c d : byte) : int := + or (shl (repr (Byte.unsigned a)) (repr (3 * Byte.zwordsize))) + (or (shl (repr (Byte.unsigned b)) (repr (2 * Byte.zwordsize))) + (or (shl (repr (Byte.unsigned c)) (repr Byte.zwordsize)) + (repr (Byte.unsigned d)))). + + Definition byte0 (n: int) : byte := Byte.repr $ unsigned n. + Definition ibyte0 (n: int) : int := Int.repr $ Byte.unsigned $ byte0 n. + + Definition byte1 (n: int) : byte := Byte.repr $ unsigned $ shru n $ repr Byte.zwordsize. + Definition ibyte1 (n: int) : int := Int.repr $ Byte.unsigned $ byte1 n. + + Definition byte2 (n: int) : byte := Byte.repr $ unsigned $ shru n $ repr (2 * Byte.zwordsize). + Definition ibyte2 (n: int) : int := Int.repr $ Byte.unsigned $ byte2 n. + + Definition byte3 (n: int) : byte := Byte.repr $ unsigned $ shru n $ repr (3 * Byte.zwordsize). + Definition ibyte3 (n: int) : int := Int.repr $ Byte.unsigned $ byte3 n. + + Lemma bits_byte0: + forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte0 n) i = testbit n i. + Proof. + intros. unfold byte0. rewrite Byte.testbit_repr; auto. + Qed. + + Lemma bits_byte1: + forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte1 n) i = testbit n (i + Byte.zwordsize). + Proof. + intros. unfold byte1. rewrite Byte.testbit_repr; auto. + assert (zwordsize = 4 * Byte.zwordsize) by reflexivity. + fold (testbit (shru n (repr Byte.zwordsize)) i). rewrite bits_shru. + change (unsigned (repr Byte.zwordsize)) with Byte.zwordsize. + apply zlt_true. omega. omega. + Qed. + + Lemma bits_byte2: + forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte2 n) i = testbit n (i + (2 * Byte.zwordsize)). + Proof. + intros. unfold byte2. rewrite Byte.testbit_repr; auto. + assert (zwordsize = 4 * Byte.zwordsize) by reflexivity. + fold (testbit (shru n (repr (2 * Byte.zwordsize))) i). rewrite bits_shru. + change (unsigned (repr (2 * Byte.zwordsize))) with (2 * Byte.zwordsize). + apply zlt_true. omega. omega. + Qed. + + Lemma bits_byte3: + forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte3 n) i = testbit n (i + (3 * Byte.zwordsize)). + Proof. + intros. unfold byte3. rewrite Byte.testbit_repr; auto. + assert (zwordsize = 4 * Byte.zwordsize) by reflexivity. + fold (testbit (shru n (repr (3 * Byte.zwordsize))) i). rewrite bits_shru. + change (unsigned (repr (3 * Byte.zwordsize))) with (3 * Byte.zwordsize). + apply zlt_true. omega. omega. + Qed. + + Lemma bits_ofwords: + forall b4 b3 b2 b1 i, 0 <= i < zwordsize -> + testbit (ofbytes b4 b3 b2 b1) i = + if zlt i Byte.zwordsize + then Byte.testbit b1 i + else (if zlt i (2 * Byte.zwordsize) + then Byte.testbit b2 (i - Byte.zwordsize) + else (if zlt i (3 * Byte.zwordsize) + then Byte.testbit b2 (i - 2 * Byte.zwordsize) + else Byte.testbit b2 (i - 3 * Byte.zwordsize))). + Proof. + intros. unfold ofbytes. repeat (rewrite bits_or; auto). repeat (rewrite bits_shl; auto). + change (unsigned (repr Byte.zwordsize)) with Byte.zwordsize. + change (unsigned (repr (2 * Byte.zwordsize))) with (2 * Byte.zwordsize). + change (unsigned (repr (3 * Byte.zwordsize))) with (3 * Byte.zwordsize). + assert (zwordsize = 4 * Byte.zwordsize) by reflexivity. + destruct (zlt i Byte.zwordsize). + rewrite testbit_repr; auto. + Abort. + End IntExtra. diff --git a/src/common/Monad.v b/src/common/Monad.v index 8517186..628963e 100644 --- a/src/common/Monad.v +++ b/src/common/Monad.v @@ -20,6 +20,10 @@ Module MonadExtra(M : Monad). Module MonadNotation. + Notation "A ; B" := + (bind A (fun _ => B)) + (at level 200, B at level 200). + Notation "'do' X <- A ; B" := (bind A (fun X => B)) (at level 200, X ident, A at level 100, B at level 200). diff --git a/src/common/ZExtra.v b/src/common/ZExtra.v index a0dd717..519ee7c 100644 --- a/src/common/ZExtra.v +++ b/src/common/ZExtra.v @@ -31,4 +31,19 @@ Module ZExtra. apply Zmult_gt_reg_r in g; lia. Qed. + Lemma Ple_not_eq : + forall x y, + (x < y)%positive -> x <> y. + Proof. lia. Qed. + + Lemma Pge_not_eq : + forall x y, + (y < x)%positive -> x <> y. + Proof. lia. Qed. + + Lemma Ple_Plt_Succ : + forall x y n, + (x <= y)%positive -> (x < y + n)%positive. + Proof. lia. Qed. + End ZExtra. |