diff options
author | Jason Gross <jgross@mit.edu> | 2017-05-13 11:55:41 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-05-13 11:55:41 -0400 |
commit | 6e5dfa6ad6aca6aa19b7d1348817bd2c23d8fdad (patch) | |
tree | 41f0bf32aa0029c669c7fc72cb31553bbaf1170e /src/Util/ZUtil | |
parent | 4ecdd6ca43af688e5cd36ec9ab2496c4e192477d (diff) |
Split off more of ZUtil
Diffstat (limited to 'src/Util/ZUtil')
-rw-r--r-- | src/Util/ZUtil/Div.v | 36 | ||||
-rw-r--r-- | src/Util/ZUtil/Tactics.v | 11 | ||||
-rw-r--r-- | src/Util/ZUtil/Tactics/CompareToSgn.v | 8 | ||||
-rw-r--r-- | src/Util/ZUtil/Tactics/DivModToQuotRem.v | 40 | ||||
-rw-r--r-- | src/Util/ZUtil/Tactics/DivideExistsMul.v | 14 | ||||
-rw-r--r-- | src/Util/ZUtil/Tactics/LinearSubstitute.v | 66 | ||||
-rw-r--r-- | src/Util/ZUtil/Tactics/LtbToLt.v | 76 | ||||
-rw-r--r-- | src/Util/ZUtil/Tactics/PrimeBound.v | 7 | ||||
-rw-r--r-- | src/Util/ZUtil/Tactics/ReplaceNegWithPos.v | 34 | ||||
-rw-r--r-- | src/Util/ZUtil/Tactics/SimplifyFractionsLe.v | 133 | ||||
-rw-r--r-- | src/Util/ZUtil/Tactics/ZeroBounds.v | 27 | ||||
-rw-r--r-- | src/Util/ZUtil/Tactics/Ztestbit.v | 22 | ||||
-rw-r--r-- | src/Util/ZUtil/Testbit.v | 90 | ||||
-rw-r--r-- | src/Util/ZUtil/ZSimplify.v | 2 | ||||
-rw-r--r-- | src/Util/ZUtil/ZSimplify/Autogenerated.v | 590 | ||||
-rw-r--r-- | src/Util/ZUtil/ZSimplify/Simple.v | 82 |
16 files changed, 1238 insertions, 0 deletions
diff --git a/src/Util/ZUtil/Div.v b/src/Util/ZUtil/Div.v new file mode 100644 index 000000000..325818a2c --- /dev/null +++ b/src/Util/ZUtil/Div.v @@ -0,0 +1,36 @@ +Require Import Coq.ZArith.ZArith Coq.micromega.Lia. +Require Import Crypto.Util.ZUtil.Tactics.CompareToSgn. +Require Import Crypto.Util.ZUtil.Hints.Core. +Local Open Scope Z_scope. + +Module Z. + Lemma div_mul' : forall a b : Z, b <> 0 -> (b * a) / b = a. + Proof. intros. rewrite Z.mul_comm. apply Z.div_mul; auto. Qed. + Hint Rewrite div_mul' using zutil_arith : zsimplify. + + Local Ltac replace_to_const c := + repeat match goal with + | [ H : ?x = ?x |- _ ] => clear H + | [ H : ?x = c, H' : context[?x] |- _ ] => rewrite H in H' + | [ H : c = ?x, H' : context[?x] |- _ ] => rewrite <- H in H' + | [ H : ?x = c |- context[?x] ] => rewrite H + | [ H : c = ?x |- context[?x] ] => rewrite <- H + end. + + Lemma lt_div_0 n m : n / m < 0 <-> ((n < 0 < m \/ m < 0 < n) /\ 0 < -(n / m)). + Proof. + Z.compare_to_sgn; rewrite Z.sgn_opp; simpl. + pose proof (Zdiv_sgn n m) as H. + pose proof (Z.sgn_spec (n / m)) as H'. + repeat first [ progress intuition auto + | progress simpl in * + | congruence + | lia + | progress replace_to_const (-1) + | progress replace_to_const 0 + | progress replace_to_const 1 + | match goal with + | [ x : Z |- _ ] => destruct x + end ]. + Qed. +End Z. diff --git a/src/Util/ZUtil/Tactics.v b/src/Util/ZUtil/Tactics.v new file mode 100644 index 000000000..3700611df --- /dev/null +++ b/src/Util/ZUtil/Tactics.v @@ -0,0 +1,11 @@ +Require Export Crypto.Util.ZUtil.Tactics.CompareToSgn. +Require Export Crypto.Util.ZUtil.Tactics.DivideExistsMul. +Require Export Crypto.Util.ZUtil.Tactics.DivModToQuotRem. +Require Export Crypto.Util.ZUtil.Tactics.LinearSubstitute. +Require Export Crypto.Util.ZUtil.Tactics.LtbToLt. +Require Export Crypto.Util.ZUtil.Tactics.PeelLe. +Require Export Crypto.Util.ZUtil.Tactics.PrimeBound. +Require Export Crypto.Util.ZUtil.Tactics.ReplaceNegWithPos. +Require Export Crypto.Util.ZUtil.Tactics.SimplifyFractionsLe. +Require Export Crypto.Util.ZUtil.Tactics.ZeroBounds. +Require Export Crypto.Util.ZUtil.Tactics.Ztestbit. diff --git a/src/Util/ZUtil/Tactics/CompareToSgn.v b/src/Util/ZUtil/Tactics/CompareToSgn.v new file mode 100644 index 000000000..31588815b --- /dev/null +++ b/src/Util/ZUtil/Tactics/CompareToSgn.v @@ -0,0 +1,8 @@ +Require Import Coq.ZArith.ZArith. +Module Z. + Ltac compare_to_sgn := + repeat match goal with + | [ H : _ |- _ ] => progress rewrite <- ?Z.sgn_neg_iff, <- ?Z.sgn_pos_iff, <- ?Z.sgn_null_iff in H + | _ => progress rewrite <- ?Z.sgn_neg_iff, <- ?Z.sgn_pos_iff, <- ?Z.sgn_null_iff + end. +End Z. diff --git a/src/Util/ZUtil/Tactics/DivModToQuotRem.v b/src/Util/ZUtil/Tactics/DivModToQuotRem.v new file mode 100644 index 000000000..b37047397 --- /dev/null +++ b/src/Util/ZUtil/Tactics/DivModToQuotRem.v @@ -0,0 +1,40 @@ +Require Import Coq.ZArith.ZArith. +Require Import Crypto.Util.ZUtil.Hints.Core. +Local Open Scope Z_scope. + +Module Z. + (** [div_mod_to_quot_rem] replaces [x / y] and [x mod y] with new + variables [q] and [r] while simultaneously adding facts that + uniquely specify [q] and [r] to the context (roughly, that [y * + q + r = x] and that [0 <= r < y]. *) + Ltac div_mod_to_quot_rem_inequality_solver := + zutil_arith_more_inequalities. + Ltac generalize_div_eucl x y := + let H := fresh in + let H' := fresh in + assert (H' : y <> 0) by div_mod_to_quot_rem_inequality_solver; + generalize (Z.div_mod x y H'); clear H'; + first [ assert (H' : 0 < y) by div_mod_to_quot_rem_inequality_solver; + generalize (Z.mod_pos_bound x y H'); clear H' + | assert (H' : y < 0) by div_mod_to_quot_rem_inequality_solver; + generalize (Z.mod_neg_bound x y H'); clear H' + | assert (H' : y < 0 \/ 0 < y) by (apply Z.neg_pos_cases; div_mod_to_quot_rem_inequality_solver); + let H'' := fresh in + assert (H'' : y < x mod y <= 0 \/ 0 <= x mod y < y) + by (destruct H'; [ left; apply Z.mod_neg_bound; assumption + | right; apply Z.mod_pos_bound; assumption ]); + clear H'; revert H'' ]; + let q := fresh "q" in + let r := fresh "r" in + set (q := x / y); + set (r := x mod y); + clearbody q r. + + Ltac div_mod_to_quot_rem_step := + match goal with + | [ |- context[?x / ?y] ] => generalize_div_eucl x y + | [ |- context[?x mod ?y] ] => generalize_div_eucl x y + end. + + Ltac div_mod_to_quot_rem := repeat div_mod_to_quot_rem_step; intros. +End Z. diff --git a/src/Util/ZUtil/Tactics/DivideExistsMul.v b/src/Util/ZUtil/Tactics/DivideExistsMul.v new file mode 100644 index 000000000..07cebc8f8 --- /dev/null +++ b/src/Util/ZUtil/Tactics/DivideExistsMul.v @@ -0,0 +1,14 @@ +Require Import Coq.ZArith.ZArith Coq.omega.Omega. +Local Open Scope Z_scope. + +Module Z. + Ltac divide_exists_mul := let k := fresh "k" in + match goal with + | [ H : (?a | ?b) |- _ ] => apply Z.mod_divide in H; try apply Zmod_divides in H; + match type of H with + | ex _ => destruct H as [k H] + | _ => destruct H + end + | [ |- (?a | ?b) ] => apply Z.mod_divide; try apply Zmod_divides + end; (omega || auto). +End Z. diff --git a/src/Util/ZUtil/Tactics/LinearSubstitute.v b/src/Util/ZUtil/Tactics/LinearSubstitute.v new file mode 100644 index 000000000..d03c9d196 --- /dev/null +++ b/src/Util/ZUtil/Tactics/LinearSubstitute.v @@ -0,0 +1,66 @@ +Require Import Coq.omega.Omega Coq.ZArith.ZArith. +Require Import Crypto.Util.Tactics.Contains. +Require Import Crypto.Util.Tactics.Not. +Local Open Scope Z_scope. + +Module Z. + Lemma move_R_pX x y z : x + y = z -> x = z - y. + Proof. omega. Qed. + Lemma move_R_mX x y z : x - y = z -> x = z + y. + Proof. omega. Qed. + Lemma move_R_Xp x y z : y + x = z -> x = z - y. + Proof. omega. Qed. + Lemma move_R_Xm x y z : y - x = z -> x = y - z. + Proof. omega. Qed. + Lemma move_L_pX x y z : z = x + y -> z - y = x. + Proof. omega. Qed. + Lemma move_L_mX x y z : z = x - y -> z + y = x. + Proof. omega. Qed. + Lemma move_L_Xp x y z : z = y + x -> z - y = x. + Proof. omega. Qed. + Lemma move_L_Xm x y z : z = y - x -> y - z = x. + Proof. omega. Qed. + + (** [linear_substitute x] attempts to maipulate equations using only + addition and subtraction to put [x] on the left, and then + eliminates [x]. Currently, it only handles equations where [x] + appears once; it does not yet handle equations like [x - x + x = + 5]. *) + Ltac linear_solve_for_in_step for_var H := + let LHS := match type of H with ?LHS = ?RHS => LHS end in + let RHS := match type of H with ?LHS = ?RHS => RHS end in + first [ match RHS with + | ?a + ?b + => first [ contains for_var b; apply move_L_pX in H + | contains for_var a; apply move_L_Xp in H ] + | ?a - ?b + => first [ contains for_var b; apply move_L_mX in H + | contains for_var a; apply move_L_Xm in H ] + | for_var + => progress symmetry in H + end + | match LHS with + | ?a + ?b + => first [ not contains for_var b; apply move_R_pX in H + | not contains for_var a; apply move_R_Xp in H ] + | ?a - ?b + => first [ not contains for_var b; apply move_R_mX in H + | not contains for_var a; apply move_R_Xm in H ] + end ]. + Ltac linear_solve_for_in for_var H := repeat linear_solve_for_in_step for_var H. + Ltac linear_solve_for for_var := + match goal with + | [ H : for_var = _ |- _ ] => idtac + | [ H : context[for_var] |- _ ] + => linear_solve_for_in for_var H; + lazymatch type of H with + | for_var = _ => idtac + | ?T => fail 0 "Could not fully solve for" for_var "in" T "(hypothesis" H ")" + end + end. + Ltac linear_substitute for_var := linear_solve_for for_var; subst for_var. + Ltac linear_substitute_all := + repeat match goal with + | [ v : Z |- _ ] => linear_substitute v + end. +End Z. diff --git a/src/Util/ZUtil/Tactics/LtbToLt.v b/src/Util/ZUtil/Tactics/LtbToLt.v new file mode 100644 index 000000000..df6eae383 --- /dev/null +++ b/src/Util/ZUtil/Tactics/LtbToLt.v @@ -0,0 +1,76 @@ +Require Import Coq.ZArith.ZArith. +Require Import Crypto.Util.Bool. +Local Open Scope Z_scope. + +Module Z. + Lemma eqb_cases x y : if x =? y then x = y else x <> y. + Proof. + pose proof (Z.eqb_spec x y) as H. + inversion H; trivial. + Qed. + + Lemma geb_spec0 : forall x y : Z, Bool.reflect (x >= y) (x >=? y). + Proof. + intros x y; pose proof (Zge_cases x y) as H; destruct (Z.geb x y); constructor; omega. + Qed. + Lemma gtb_spec0 : forall x y : Z, Bool.reflect (x > y) (x >? y). + Proof. + intros x y; pose proof (Zgt_cases x y) as H; destruct (Z.gtb x y); constructor; omega. + Qed. + + Ltac ltb_to_lt_with_hyp H lem := + let H' := fresh in + rename H into H'; + pose proof lem as H; + rewrite H' in H; + clear H'. + + Ltac ltb_to_lt_in_goal b' lem := + refine (proj1 (@reflect_iff_gen _ _ lem b') _); + cbv beta iota. + + Ltac ltb_to_lt_hyps_step := + match goal with + | [ H : (?x <? ?y) = ?b |- _ ] + => ltb_to_lt_with_hyp H (Zlt_cases x y) + | [ H : (?x <=? ?y) = ?b |- _ ] + => ltb_to_lt_with_hyp H (Zle_cases x y) + | [ H : (?x >? ?y) = ?b |- _ ] + => ltb_to_lt_with_hyp H (Zgt_cases x y) + | [ H : (?x >=? ?y) = ?b |- _ ] + => ltb_to_lt_with_hyp H (Zge_cases x y) + | [ H : (?x =? ?y) = ?b |- _ ] + => ltb_to_lt_with_hyp H (eqb_cases x y) + end. + Ltac ltb_to_lt_goal_step := + match goal with + | [ |- (?x <? ?y) = ?b ] + => ltb_to_lt_in_goal b (Z.ltb_spec0 x y) + | [ |- (?x <=? ?y) = ?b ] + => ltb_to_lt_in_goal b (Z.leb_spec0 x y) + | [ |- (?x >? ?y) = ?b ] + => ltb_to_lt_in_goal b (Z.gtb_spec0 x y) + | [ |- (?x >=? ?y) = ?b ] + => ltb_to_lt_in_goal b (Z.geb_spec0 x y) + | [ |- (?x =? ?y) = ?b ] + => ltb_to_lt_in_goal b (Z.eqb_spec x y) + end. + Ltac ltb_to_lt_step := + first [ ltb_to_lt_hyps_step + | ltb_to_lt_goal_step ]. + Ltac ltb_to_lt := repeat ltb_to_lt_step. + + Section R_Rb. + Local Ltac t := intros ? ? []; split; intro; ltb_to_lt; omega. + Local Notation R_Rb Rb R nR := (forall x y b, Rb x y = b <-> if b then R x y else nR x y). + Lemma ltb_lt_iff : R_Rb Z.ltb Z.lt Z.ge. Proof. t. Qed. + Lemma leb_le_iff : R_Rb Z.leb Z.le Z.gt. Proof. t. Qed. + Lemma gtb_gt_iff : R_Rb Z.gtb Z.gt Z.le. Proof. t. Qed. + Lemma geb_ge_iff : R_Rb Z.geb Z.ge Z.lt. Proof. t. Qed. + Lemma eqb_eq_iff : R_Rb Z.eqb (@Logic.eq Z) (fun x y => x <> y). Proof. t. Qed. + End R_Rb. + Hint Rewrite ltb_lt_iff leb_le_iff gtb_gt_iff geb_ge_iff eqb_eq_iff : ltb_to_lt. + Ltac ltb_to_lt_in_context := + repeat autorewrite with ltb_to_lt in *; + cbv beta iota in *. +End Z. diff --git a/src/Util/ZUtil/Tactics/PrimeBound.v b/src/Util/ZUtil/Tactics/PrimeBound.v new file mode 100644 index 000000000..f914ed7c8 --- /dev/null +++ b/src/Util/ZUtil/Tactics/PrimeBound.v @@ -0,0 +1,7 @@ +Require Import Coq.omega.Omega Coq.ZArith.Znumtheory. + +Module Z. + Ltac prime_bound := match goal with + | [ H : prime ?p |- _ ] => pose proof (prime_ge_2 p H); try omega + end. +End Z. diff --git a/src/Util/ZUtil/Tactics/ReplaceNegWithPos.v b/src/Util/ZUtil/Tactics/ReplaceNegWithPos.v new file mode 100644 index 000000000..67b5397aa --- /dev/null +++ b/src/Util/ZUtil/Tactics/ReplaceNegWithPos.v @@ -0,0 +1,34 @@ +Require Import Coq.omega.Omega Coq.ZArith.ZArith. +Local Open Scope Z_scope. + +Module Z. + Ltac clean_neg := + repeat match goal with + | [ H : (-?x) < 0 |- _ ] => assert (0 < x) by omega; clear H + | [ H : 0 > (-?x) |- _ ] => assert (0 < x) by omega; clear H + | [ H : (-?x) <= 0 |- _ ] => assert (0 <= x) by omega; clear H + | [ H : 0 >= (-?x) |- _ ] => assert (0 <= x) by omega; clear H + | [ H : -?x <= -?y |- _ ] => apply Z.opp_le_mono in H + | [ |- -?x <= -?y ] => apply Z.opp_le_mono + | _ => progress rewrite <- Z.opp_le_mono in * + | [ H : 0 <= ?x, H' : 0 <= ?y, H'' : -?x <= ?y |- _ ] => clear H'' + | [ H : 0 < ?x, H' : 0 <= ?y, H'' : -?x <= ?y |- _ ] => clear H'' + | [ H : 0 <= ?x, H' : 0 < ?y, H'' : -?x <= ?y |- _ ] => clear H'' + | [ H : 0 < ?x, H' : 0 < ?y, H'' : -?x <= ?y |- _ ] => clear H'' + | [ H : 0 < ?x, H' : 0 <= ?y, H'' : -?x < ?y |- _ ] => clear H'' + | [ H : 0 <= ?x, H' : 0 < ?y, H'' : -?x < ?y |- _ ] => clear H'' + | [ H : 0 < ?x, H' : 0 < ?y, H'' : -?x < ?y |- _ ] => clear H'' + end. + Ltac replace_with_neg x := + assert (x = -(-x)) by (symmetry; apply Z.opp_involutive); generalize dependent (-x); + let x' := fresh in + rename x into x'; intro x; intros; subst x'; + clean_neg. + Ltac replace_all_neg_with_pos := + repeat match goal with + | [ H : ?x < 0 |- _ ] => replace_with_neg x + | [ H : 0 > ?x |- _ ] => replace_with_neg x + | [ H : ?x <= 0 |- _ ] => replace_with_neg x + | [ H : 0 >= ?x |- _ ] => replace_with_neg x + end. +End Z. diff --git a/src/Util/ZUtil/Tactics/SimplifyFractionsLe.v b/src/Util/ZUtil/Tactics/SimplifyFractionsLe.v new file mode 100644 index 000000000..c5b024eca --- /dev/null +++ b/src/Util/ZUtil/Tactics/SimplifyFractionsLe.v @@ -0,0 +1,133 @@ +Require Import Coq.ZArith.ZArith. +Require Import Coq.micromega.Lia. +Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. +Require Import Crypto.Util.ZUtil.Div. +Local Open Scope Z_scope. + +Module Z. + (** * [Z.simplify_fractions_le] *) + (** The culmination of this series of tactics, + [Z.simplify_fractions_le], will use the fact that [a * (b / c) <= + (a * b) / c], and do some reasoning modulo associativity and + commutativity in [Z] to perform such a reduction. It may leave + over goals if it cannot prove that some denominators are non-zero. + If the rewrite [a * (b / c)] → [(a * b) / c] is safe to do on the + LHS of the goal, this tactic should not turn a solvable goal into + an unsolvable one. + + After running, the tactic does some basic rewriting to simplify + fractions, e.g., that [a * b / b = a]. *) + Ltac split_sums_step := + match goal with + | [ |- _ + _ <= _ ] + => etransitivity; [ eapply Z.add_le_mono | ] + | [ |- _ - _ <= _ ] + => etransitivity; [ eapply Z.sub_le_mono | ] + end. + Ltac split_sums := + try (split_sums_step; [ split_sums.. | ]). + Ltac pre_reorder_fractions_step := + match goal with + | [ |- context[?x / ?y * ?z] ] + => lazymatch z with + | context[_ / _] => fail + | _ => idtac + end; + rewrite (Z.mul_comm (x / y) z) + | _ => let LHS := match goal with |- ?LHS <= ?RHS => LHS end in + match LHS with + | context G[?x * (?y / ?z)] + => let G' := context G[(x * y) / z] in + transitivity G' + end + end. + Ltac pre_reorder_fractions := + try first [ split_sums_step; [ pre_reorder_fractions.. | ] + | pre_reorder_fractions_step; [ .. | pre_reorder_fractions ] ]. + Ltac split_comparison := + match goal with + | [ |- ?x <= ?x ] => reflexivity + | [ H : _ >= _ |- _ ] + => apply Z.ge_le_iff in H + | [ |- ?x * ?y <= ?z * ?w ] + => lazymatch goal with + | [ H : 0 <= x |- _ ] => idtac + | [ H : x < 0 |- _ ] => fail + | _ => destruct (Z_lt_le_dec x 0) + end; + [ .. + | lazymatch goal with + | [ H : 0 <= y |- _ ] => idtac + | [ H : y < 0 |- _ ] => fail + | _ => destruct (Z_lt_le_dec y 0) + end; + [ .. + | apply Zmult_le_compat; [ | | assumption | assumption ] ] ] + | [ |- ?x / ?y <= ?z / ?y ] + => lazymatch goal with + | [ H : 0 < y |- _ ] => idtac + | [ H : y <= 0 |- _ ] => fail + | _ => destruct (Z_lt_le_dec 0 y) + end; + [ apply Z_div_le; [ apply Z.gt_lt_iff; assumption | ] + | .. ] + | [ |- ?x / ?y <= ?x / ?z ] + => lazymatch goal with + | [ H : 0 <= x |- _ ] => idtac + | [ H : x < 0 |- _ ] => fail + | _ => destruct (Z_lt_le_dec x 0) + end; + [ .. + | lazymatch goal with + | [ H : 0 < z |- _ ] => idtac + | [ H : z <= 0 |- _ ] => fail + | _ => destruct (Z_lt_le_dec 0 z) + end; + [ apply Z.div_le_compat_l; [ assumption | split; [ assumption | ] ] + | .. ] ] + | [ |- _ + _ <= _ + _ ] + => apply Z.add_le_mono + | [ |- _ - _ <= _ - _ ] + => apply Z.sub_le_mono + | [ |- ?x * (?y / ?z) <= (?x * ?y) / ?z ] + => apply Z.div_mul_le + end. + Ltac split_comparison_fin_step := + match goal with + | _ => assumption + | _ => lia + | _ => progress subst + | [ H : ?n * ?m < 0 |- _ ] + => apply (proj1 (Z.lt_mul_0 n m)) in H; destruct H as [ [??]|[??] ] + | [ H : ?n / ?m < 0 |- _ ] + => apply (proj1 (Z.lt_div_0 n m)) in H; destruct H as [ [ [??]|[??] ] ? ] + | [ H : (?x^?y) <= ?n < _, H' : ?n < 0 |- _ ] + => assert (0 <= x^y) by Z.zero_bounds; lia + | [ H : (?x^?y) < 0 |- _ ] + => assert (0 <= x^y) by Z.zero_bounds; lia + | [ H : (?x^?y) <= 0 |- _ ] + => let H' := fresh in + assert (H' : 0 <= x^y) by Z.zero_bounds; + assert (x^y = 0) by lia; + clear H H' + | [ H : _^_ = 0 |- _ ] + => apply Z.pow_eq_0_iff in H; destruct H as [ ?|[??] ] + | [ H : 0 <= ?x, H' : ?x - 1 < 0 |- _ ] + => assert (x = 0) by lia; clear H H' + | [ |- ?x <= ?y ] => is_evar x; reflexivity + | [ |- ?x <= ?y ] => is_evar y; reflexivity + end. + Ltac split_comparison_fin := repeat split_comparison_fin_step. + Ltac simplify_fractions_step := + match goal with + | _ => rewrite Z.div_mul by (try apply Z.pow_nonzero; Z.zero_bounds) + | [ |- context[?x * ?y / ?x] ] + => rewrite (Z.mul_comm x y) + | [ |- ?x <= ?x ] => reflexivity + end. + Ltac simplify_fractions := repeat simplify_fractions_step. + Ltac simplify_fractions_le := + pre_reorder_fractions; + [ repeat split_comparison; split_comparison_fin; Z.zero_bounds.. + | simplify_fractions ]. +End Z. diff --git a/src/Util/ZUtil/Tactics/ZeroBounds.v b/src/Util/ZUtil/Tactics/ZeroBounds.v new file mode 100644 index 000000000..d10b6714c --- /dev/null +++ b/src/Util/ZUtil/Tactics/ZeroBounds.v @@ -0,0 +1,27 @@ +Require Import Coq.ZArith.ZArith Coq.omega.Omega. +Require Import Crypto.Util.ZUtil.Tactics.PrimeBound. +Local Open Scope Z_scope. + +Module Z. + (* prove that combinations of known positive/nonnegative numbers are positive/nonnegative *) + Ltac zero_bounds' := + repeat match goal with + | [ |- 0 <= _ + _] => apply Z.add_nonneg_nonneg + | [ |- 0 <= _ - _] => apply Z.le_0_sub + | [ |- 0 <= _ * _] => apply Z.mul_nonneg_nonneg + | [ |- 0 <= _ / _] => apply Z.div_pos + | [ |- 0 <= _ ^ _ ] => apply Z.pow_nonneg + | [ |- 0 <= Z.shiftr _ _] => apply Z.shiftr_nonneg + | [ |- 0 <= _ mod _] => apply Z.mod_pos_bound + | [ |- 0 < _ + _] => try solve [apply Z.add_pos_nonneg; zero_bounds']; + try solve [apply Z.add_nonneg_pos; zero_bounds'] + | [ |- 0 < _ - _] => apply Z.lt_0_sub + | [ |- 0 < _ * _] => apply Z.lt_0_mul; left; split + | [ |- 0 < _ / _] => apply Z.div_str_pos + | [ |- 0 < _ ^ _ ] => apply Z.pow_pos_nonneg + end; try omega; try Z.prime_bound; auto. + + Ltac zero_bounds := try omega; try Z.prime_bound; zero_bounds'. + + Hint Extern 1 => progress zero_bounds : zero_bounds. +End Z. diff --git a/src/Util/ZUtil/Tactics/Ztestbit.v b/src/Util/ZUtil/Tactics/Ztestbit.v new file mode 100644 index 000000000..d12de5330 --- /dev/null +++ b/src/Util/ZUtil/Tactics/Ztestbit.v @@ -0,0 +1,22 @@ +Require Import Coq.ZArith.ZArith. +Require Import Crypto.Util.ZUtil.Testbit. +Require Import Crypto.Util.ZUtil.Hints.Core. + +Ltac Ztestbit_full_step := + match goal with + | _ => progress autorewrite with Ztestbit_full + | [ |- context[Z.testbit ?x ?y] ] + => rewrite (Z.testbit_neg_r x y) by zutil_arith + | [ |- context[Z.testbit ?x ?y] ] + => rewrite (Z.bits_above_pow2 x y) by zutil_arith + | [ |- context[Z.testbit ?x ?y] ] + => rewrite (Z.bits_above_log2 x y) by zutil_arith + end. +Ltac Ztestbit_full := repeat Ztestbit_full_step. + +Ltac Ztestbit_step := + match goal with + | _ => progress autorewrite with Ztestbit + | _ => progress Ztestbit_full_step + end. +Ltac Ztestbit := repeat Ztestbit_step. diff --git a/src/Util/ZUtil/Testbit.v b/src/Util/ZUtil/Testbit.v new file mode 100644 index 000000000..a315f7e4b --- /dev/null +++ b/src/Util/ZUtil/Testbit.v @@ -0,0 +1,90 @@ +Require Import Coq.ZArith.ZArith. +Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.ZUtil.Hints. +Require Import Crypto.Util.ZUtil.Notations. +Require Import Crypto.Util.Tactics.BreakMatch. +Local Open Scope Z_scope. + +Module Z. + Lemma ones_spec : forall n m, 0 <= n -> 0 <= m -> Z.testbit (Z.ones n) m = if Z_lt_dec m n then true else false. + Proof. + intros. + break_match. + + apply Z.ones_spec_low. omega. + + apply Z.ones_spec_high. omega. + Qed. + Hint Rewrite ones_spec using zutil_arith : Ztestbit. + + Lemma ones_spec_full : forall n m, Z.testbit (Z.ones n) m + = if Z_lt_dec m 0 + then false + else if Z_lt_dec n 0 + then true + else if Z_lt_dec m n then true else false. + Proof. + intros. + repeat (break_match || autorewrite with Ztestbit); try reflexivity; try omega. + unfold Z.ones. + rewrite <- Z.shiftr_opp_r, Z.shiftr_eq_0 by (simpl; omega); simpl. + destruct m; simpl in *; try reflexivity. + exfalso; auto using Zlt_neg_0. + Qed. + Hint Rewrite ones_spec_full : Ztestbit_full. + + Lemma testbit_pow2_mod : forall a n i, 0 <= n -> + Z.testbit (Z.pow2_mod a n) i = if Z_lt_dec i n then Z.testbit a i else false. + Proof. + cbv [Z.pow2_mod]; intros; destruct (Z_le_dec 0 i); + repeat match goal with + | |- _ => rewrite Z.testbit_neg_r by omega + | |- _ => break_innermost_match_step + | |- _ => omega + | |- _ => reflexivity + | |- _ => progress autorewrite with Ztestbit + end. + Qed. + Hint Rewrite testbit_pow2_mod using zutil_arith : Ztestbit. + + Lemma testbit_pow2_mod_full : forall a n i, + Z.testbit (Z.pow2_mod a n) i = if Z_lt_dec n 0 + then if Z_lt_dec i 0 then false else Z.testbit a i + else if Z_lt_dec i n then Z.testbit a i else false. + Proof. + intros; destruct (Z_lt_dec n 0); [ | apply testbit_pow2_mod; omega ]. + unfold Z.pow2_mod. + autorewrite with Ztestbit_full; + repeat break_match; + autorewrite with Ztestbit; + reflexivity. + Qed. + Hint Rewrite testbit_pow2_mod_full : Ztestbit_full. + + Lemma bits_above_pow2 a n : 0 <= a < 2^n -> Z.testbit a n = false. + Proof. + intros. + destruct (Z_zerop a); subst; autorewrite with Ztestbit; trivial. + apply Z.bits_above_log2; auto with zarith concl_log2. + Qed. + Hint Rewrite bits_above_pow2 using zutil_arith : Ztestbit. + + Lemma testbit_low : forall n x i, (0 <= i < n) -> + Z.testbit x i = Z.testbit (Z.land x (Z.ones n)) i. + Proof. + intros. + rewrite Z.land_ones by omega. + symmetry. + apply Z.mod_pow2_bits_low. + omega. + Qed. + + Lemma testbit_add_shiftl_low : forall i, (0 <= i) -> forall a b n, (i < n) -> + Z.testbit (a + Z.shiftl b n) i = Z.testbit a i. + Proof. + intros. + erewrite Z.testbit_low; eauto. + rewrite Z.land_ones, Z.shiftl_mul_pow2 by omega. + rewrite Z.mod_add by (pose proof (Z.pow_pos_nonneg 2 n); omega). + auto using Z.mod_pow2_bits_low. + Qed. + Hint Rewrite testbit_add_shiftl_low using zutil_arith : Ztestbit. +End Z. diff --git a/src/Util/ZUtil/ZSimplify.v b/src/Util/ZUtil/ZSimplify.v new file mode 100644 index 000000000..b27a92a0c --- /dev/null +++ b/src/Util/ZUtil/ZSimplify.v @@ -0,0 +1,2 @@ +Require Export Crypto.Util.ZUtil.ZSimplify.Autogenerated. +Require Export Crypto.Util.ZUtil.ZSimplify.Simple. diff --git a/src/Util/ZUtil/ZSimplify/Autogenerated.v b/src/Util/ZUtil/ZSimplify/Autogenerated.v new file mode 100644 index 000000000..b3b6d36b6 --- /dev/null +++ b/src/Util/ZUtil/ZSimplify/Autogenerated.v @@ -0,0 +1,590 @@ +Require Import Coq.ZArith.ZArith Coq.micromega.Lia. +Require Import Crypto.Util.ZUtil.Hints.Core. +Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. +Local Open Scope Z_scope. + +Module Z. + Local Ltac simplify_div_tac := + intros; Z.div_mod_to_quot_rem; nia. + (* Naming Convention: [X] for thing being divided by, [p] for plus, + [m] for minus, [d] for div, and [_] to separate parentheses and + multiplication. *) + (* Mathematica code to generate these hints: +<< +ClearAll[minus, plus, div, mul, combine, parens, ExprToString, + ExprToExpr, ExprToName, SymbolsIn, Chars, RestFrom, a, b, c, d, e, + f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, X]; +Chars = StringSplit["abcdefghijklmnopqrstuvwxyz", ""]; +RestFrom[i_, len_] := + Join[{mul[Chars[[i]], "X"]}, Take[Drop[Chars, i], len]] +Exprs = Flatten[ + Map[{#1, #1 /. mul[a_, "X", b___] :> mul["X", a, b]} &, Flatten[{ + Table[ + Table[div[ + combine @@ + Join[Take[Chars, start - 1], RestFrom[start, len]], + "X"], {len, 0, 10 - start}], {start, 1, 2}], + Table[ + Table[div[ + combine["a", + parens @@ + Join[Take[Drop[Chars, 1], start - 1], + RestFrom[1 + start, len]]], "X"], {len, 0, + 10 - start}], {start, 1, 2}], + div[combine["a", parens["b", parens["c", mul["d", "X"]], "e"]], + "X"], + div[combine["a", "b", parens["c", mul["d", "X"]], "e"], "X"], + div[combine["a", "b", mul["c", "X", "d"], "e", "f"], "X"], + div[combine["a", mul["b", "X", "c"], "d", "e"], "X"], + div[ + combine["a", + parens["b", parens["c", mul["d", "X", "e"]], "f"]], "X"], + div[combine["a", parens["b", mul["c", "X", "d"]], "e"], "X"]}]]]; +ExprToString[div[x_, y_], withparen_: False] := + With[{v := ExprToString[x, True] <> " / " <> ExprToString[y, True]}, + If[withparen, "(" <> v <> ")", v]] +ExprToString[combine[x_], withparen_: False] := + ExprToString[x, withparen] +ExprToString[combine[x_, minus, y__], withparen_: False] := + With[{v := + ExprToString[x, False] <> " - " <> + ExprToString[combine[y], False]}, + If[withparen, "(" <> v <> ")", v]] +ExprToString[combine[minus, y__], withparen_: False] := + With[{v := "-" <> ExprToString[combine[y], False]}, + If[withparen, "(" <> v <> ")", v]] +ExprToString[combine[x_, y__], withparen_: False] := + With[{v := + ExprToString[x, False] <> " + " <> + ExprToString[combine[y], False]}, + If[withparen, "(" <> v <> ")", v]] +ExprToString[mul[x_], withparen_: False] := ExprToString[x] +ExprToString[mul[x_, y__], withparen_: False] := + With[{v := + ExprToString[x, False] <> " * " <> ExprToString[mul[y], False]}, + If[withparen, "(" <> v <> ")", v]] +ExprToString[parens[x__], withparen_: False] := + "(" <> ExprToString[combine[x]] <> ")" +ExprToString[x_String, withparen_: False] := x +ExprToExpr[div[x__]] := Divide @@ Map[ExprToExpr, {x}] +ExprToExpr[mul[x__]] := Times @@ Map[ExprToExpr, {x}] +ExprToExpr[combine[]] := 0 +ExprToExpr[combine[minus, y_, z___]] := -ExprToExpr[y] + + ExprToExpr[combine[z]] +ExprToExpr[combine[x_, y___]] := ExprToExpr[x] + ExprToExpr[combine[y]] +ExprToExpr[parens[x__]] := ExprToExpr[combine[x]] +ExprToExpr[x_String] := Symbol[x] +ExprToName["X", ispos_: True] := If[ispos, "X", "mX"] +ExprToName[x_String, ispos_: True] := If[ispos, "p", "m"] +ExprToName[div[x_, y_], ispos_: True] := + If[ispos, "p", "m"] <> ExprToName[x] <> "d" <> ExprToName[y] +ExprToName[mul[x_], ispos_: True] := + If[ispos, "", "m_"] <> ExprToName[x] <> "_" +ExprToName[mul[x_, y__], ispos_: True] := + If[ispos, "", "m_"] <> ExprToName[x] <> ExprToName[mul[y]] +ExprToName[combine[], ispos_: True] := "" +ExprToName[combine[x_], ispos_: True] := ExprToName[x, ispos] +ExprToName[combine[x_, minus, mul[y__], z___], ispos_: True] := + ExprToName[x, ispos] <> "m_" <> ExprToName[mul[y], True] <> + ExprToName[combine[z], True] +ExprToName[combine[x_, mul[y__], z___], ispos_: True] := + ExprToName[x, ispos] <> "p_" <> ExprToName[mul[y], True] <> + ExprToName[combine[z], True] +ExprToName[combine[x_, y__], ispos_: True] := + ExprToName[x, ispos] <> ExprToName[combine[y], True] +ExprToName[combine[x_, minus, y__], ispos_: True] := + ExprToName[x, ispos] <> ExprToName[combine[y], True] +ExprToName[combine[x_, y__], ispos_: True] := + ExprToName[x, ispos] <> ExprToName[combine[y], True] +ExprToName[parens[x__], ispos_: True] := + "_o_" <> ExprToName[combine[x], ispos] <> "_c_" +SymbolsIn[x_String] := {x <> " "} +SymbolsIn[f_[y___]] := Join @@ Map[SymbolsIn, {y}] +StringJoin @@ + Map[{" Lemma simplify_div_" <> ExprToName[#1] <> " " <> + StringJoin @@ Sort[DeleteDuplicates[SymbolsIn[#1]]] <> + ": X <> 0 -> " <> ExprToString[#1] <> " = " <> + StringReplace[(FullSimplify[ExprToExpr[#1]] // InputForm // + ToString), "/" -> " / "] <> "." <> + "\n Proof. simplify_div_tac. Qed.\n Hint Rewrite \ +simplify_div_" <> ExprToName[#1] <> + " using zutil_arith : zsimplify.\n"} &, Exprs] +>> *) + Lemma simplify_div_ppX_dX a X : X <> 0 -> (a * X) / X = a. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_ppX_dX using zutil_arith : zsimplify. + Lemma simplify_div_pXp_dX a X : X <> 0 -> (X * a) / X = a. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pXp_dX using zutil_arith : zsimplify. + Lemma simplify_div_ppX_pdX a b X : X <> 0 -> (a * X + b) / X = a + b / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_ppX_pdX using zutil_arith : zsimplify. + Lemma simplify_div_pXp_pdX a b X : X <> 0 -> (X * a + b) / X = a + b / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pXp_pdX using zutil_arith : zsimplify. + Lemma simplify_div_ppX_ppdX a b c X : X <> 0 -> (a * X + b + c) / X = a + (b + c) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_ppX_ppdX using zutil_arith : zsimplify. + Lemma simplify_div_pXp_ppdX a b c X : X <> 0 -> (X * a + b + c) / X = a + (b + c) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pXp_ppdX using zutil_arith : zsimplify. + Lemma simplify_div_ppX_pppdX a b c d X : X <> 0 -> (a * X + b + c + d) / X = a + (b + c + d) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_ppX_pppdX using zutil_arith : zsimplify. + Lemma simplify_div_pXp_pppdX a b c d X : X <> 0 -> (X * a + b + c + d) / X = a + (b + c + d) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pXp_pppdX using zutil_arith : zsimplify. + Lemma simplify_div_ppX_ppppdX a b c d e X : X <> 0 -> (a * X + b + c + d + e) / X = a + (b + c + d + e) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_ppX_ppppdX using zutil_arith : zsimplify. + Lemma simplify_div_pXp_ppppdX a b c d e X : X <> 0 -> (X * a + b + c + d + e) / X = a + (b + c + d + e) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pXp_ppppdX using zutil_arith : zsimplify. + Lemma simplify_div_ppX_pppppdX a b c d e f X : X <> 0 -> (a * X + b + c + d + e + f) / X = a + (b + c + d + e + f) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_ppX_pppppdX using zutil_arith : zsimplify. + Lemma simplify_div_pXp_pppppdX a b c d e f X : X <> 0 -> (X * a + b + c + d + e + f) / X = a + (b + c + d + e + f) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pXp_pppppdX using zutil_arith : zsimplify. + Lemma simplify_div_ppX_ppppppdX a b c d e f g X : X <> 0 -> (a * X + b + c + d + e + f + g) / X = a + (b + c + d + e + f + g) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_ppX_ppppppdX using zutil_arith : zsimplify. + Lemma simplify_div_pXp_ppppppdX a b c d e f g X : X <> 0 -> (X * a + b + c + d + e + f + g) / X = a + (b + c + d + e + f + g) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pXp_ppppppdX using zutil_arith : zsimplify. + Lemma simplify_div_ppX_pppppppdX a b c d e f g h X : X <> 0 -> (a * X + b + c + d + e + f + g + h) / X = a + (b + c + d + e + f + g + h) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_ppX_pppppppdX using zutil_arith : zsimplify. + Lemma simplify_div_pXp_pppppppdX a b c d e f g h X : X <> 0 -> (X * a + b + c + d + e + f + g + h) / X = a + (b + c + d + e + f + g + h) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pXp_pppppppdX using zutil_arith : zsimplify. + Lemma simplify_div_ppX_ppppppppdX a b c d e f g h i X : X <> 0 -> (a * X + b + c + d + e + f + g + h + i) / X = a + (b + c + d + e + f + g + h + i) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_ppX_ppppppppdX using zutil_arith : zsimplify. + Lemma simplify_div_pXp_ppppppppdX a b c d e f g h i X : X <> 0 -> (X * a + b + c + d + e + f + g + h + i) / X = a + (b + c + d + e + f + g + h + i) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pXp_ppppppppdX using zutil_arith : zsimplify. + Lemma simplify_div_ppX_pppppppppdX a b c d e f g h i j X : X <> 0 -> (a * X + b + c + d + e + f + g + h + i + j) / X = a + (b + c + d + e + f + g + h + i + j) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_ppX_pppppppppdX using zutil_arith : zsimplify. + Lemma simplify_div_pXp_pppppppppdX a b c d e f g h i j X : X <> 0 -> (X * a + b + c + d + e + f + g + h + i + j) / X = a + (b + c + d + e + f + g + h + i + j) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pXp_pppppppppdX using zutil_arith : zsimplify. + Lemma simplify_div_ppp_pX_dX a b X : X <> 0 -> (a + b * X) / X = b + a / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_ppp_pX_dX using zutil_arith : zsimplify. + Lemma simplify_div_ppp_Xp_dX a b X : X <> 0 -> (a + X * b) / X = b + a / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_ppp_Xp_dX using zutil_arith : zsimplify. + Lemma simplify_div_ppp_pX_pdX a b c X : X <> 0 -> (a + b * X + c) / X = b + (a + c) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_ppp_pX_pdX using zutil_arith : zsimplify. + Lemma simplify_div_ppp_Xp_pdX a b c X : X <> 0 -> (a + X * b + c) / X = b + (a + c) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_ppp_Xp_pdX using zutil_arith : zsimplify. + Lemma simplify_div_ppp_pX_ppdX a b c d X : X <> 0 -> (a + b * X + c + d) / X = b + (a + c + d) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_ppp_pX_ppdX using zutil_arith : zsimplify. + Lemma simplify_div_ppp_Xp_ppdX a b c d X : X <> 0 -> (a + X * b + c + d) / X = b + (a + c + d) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_ppp_Xp_ppdX using zutil_arith : zsimplify. + Lemma simplify_div_ppp_pX_pppdX a b c d e X : X <> 0 -> (a + b * X + c + d + e) / X = b + (a + c + d + e) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_ppp_pX_pppdX using zutil_arith : zsimplify. + Lemma simplify_div_ppp_Xp_pppdX a b c d e X : X <> 0 -> (a + X * b + c + d + e) / X = b + (a + c + d + e) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_ppp_Xp_pppdX using zutil_arith : zsimplify. + Lemma simplify_div_ppp_pX_ppppdX a b c d e f X : X <> 0 -> (a + b * X + c + d + e + f) / X = b + (a + c + d + e + f) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_ppp_pX_ppppdX using zutil_arith : zsimplify. + Lemma simplify_div_ppp_Xp_ppppdX a b c d e f X : X <> 0 -> (a + X * b + c + d + e + f) / X = b + (a + c + d + e + f) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_ppp_Xp_ppppdX using zutil_arith : zsimplify. + Lemma simplify_div_ppp_pX_pppppdX a b c d e f g X : X <> 0 -> (a + b * X + c + d + e + f + g) / X = b + (a + c + d + e + f + g) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_ppp_pX_pppppdX using zutil_arith : zsimplify. + Lemma simplify_div_ppp_Xp_pppppdX a b c d e f g X : X <> 0 -> (a + X * b + c + d + e + f + g) / X = b + (a + c + d + e + f + g) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_ppp_Xp_pppppdX using zutil_arith : zsimplify. + Lemma simplify_div_ppp_pX_ppppppdX a b c d e f g h X : X <> 0 -> (a + b * X + c + d + e + f + g + h) / X = b + (a + c + d + e + f + g + h) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_ppp_pX_ppppppdX using zutil_arith : zsimplify. + Lemma simplify_div_ppp_Xp_ppppppdX a b c d e f g h X : X <> 0 -> (a + X * b + c + d + e + f + g + h) / X = b + (a + c + d + e + f + g + h) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_ppp_Xp_ppppppdX using zutil_arith : zsimplify. + Lemma simplify_div_ppp_pX_pppppppdX a b c d e f g h i X : X <> 0 -> (a + b * X + c + d + e + f + g + h + i) / X = b + (a + c + d + e + f + g + h + i) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_ppp_pX_pppppppdX using zutil_arith : zsimplify. + Lemma simplify_div_ppp_Xp_pppppppdX a b c d e f g h i X : X <> 0 -> (a + X * b + c + d + e + f + g + h + i) / X = b + (a + c + d + e + f + g + h + i) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_ppp_Xp_pppppppdX using zutil_arith : zsimplify. + Lemma simplify_div_ppp_pX_ppppppppdX a b c d e f g h i j X : X <> 0 -> (a + b * X + c + d + e + f + g + h + i + j) / X = b + (a + c + d + e + f + g + h + i + j) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_ppp_pX_ppppppppdX using zutil_arith : zsimplify. + Lemma simplify_div_ppp_Xp_ppppppppdX a b c d e f g h i j X : X <> 0 -> (a + X * b + c + d + e + f + g + h + i + j) / X = b + (a + c + d + e + f + g + h + i + j) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_ppp_Xp_ppppppppdX using zutil_arith : zsimplify. + Lemma simplify_div_pp_o_pX__c_dX a b X : X <> 0 -> (a + (b * X)) / X = b + a / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pp_o_pX__c_dX using zutil_arith : zsimplify. + Lemma simplify_div_pp_o_Xp__c_dX a b X : X <> 0 -> (a + (X * b)) / X = b + a / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pp_o_Xp__c_dX using zutil_arith : zsimplify. + Lemma simplify_div_pp_o_pX_p_c_dX a b c X : X <> 0 -> (a + (b * X + c)) / X = b + (a + c) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pp_o_pX_p_c_dX using zutil_arith : zsimplify. + Lemma simplify_div_pp_o_Xp_p_c_dX a b c X : X <> 0 -> (a + (X * b + c)) / X = b + (a + c) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pp_o_Xp_p_c_dX using zutil_arith : zsimplify. + Lemma simplify_div_pp_o_pX_pp_c_dX a b c d X : X <> 0 -> (a + (b * X + c + d)) / X = b + (a + c + d) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pp_o_pX_pp_c_dX using zutil_arith : zsimplify. + Lemma simplify_div_pp_o_Xp_pp_c_dX a b c d X : X <> 0 -> (a + (X * b + c + d)) / X = b + (a + c + d) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pp_o_Xp_pp_c_dX using zutil_arith : zsimplify. + Lemma simplify_div_pp_o_pX_ppp_c_dX a b c d e X : X <> 0 -> (a + (b * X + c + d + e)) / X = b + (a + c + d + e) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pp_o_pX_ppp_c_dX using zutil_arith : zsimplify. + Lemma simplify_div_pp_o_Xp_ppp_c_dX a b c d e X : X <> 0 -> (a + (X * b + c + d + e)) / X = b + (a + c + d + e) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pp_o_Xp_ppp_c_dX using zutil_arith : zsimplify. + Lemma simplify_div_pp_o_pX_pppp_c_dX a b c d e f X : X <> 0 -> (a + (b * X + c + d + e + f)) / X = b + (a + c + d + e + f) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pp_o_pX_pppp_c_dX using zutil_arith : zsimplify. + Lemma simplify_div_pp_o_Xp_pppp_c_dX a b c d e f X : X <> 0 -> (a + (X * b + c + d + e + f)) / X = b + (a + c + d + e + f) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pp_o_Xp_pppp_c_dX using zutil_arith : zsimplify. + Lemma simplify_div_pp_o_pX_ppppp_c_dX a b c d e f g X : X <> 0 -> (a + (b * X + c + d + e + f + g)) / X = b + (a + c + d + e + f + g) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pp_o_pX_ppppp_c_dX using zutil_arith : zsimplify. + Lemma simplify_div_pp_o_Xp_ppppp_c_dX a b c d e f g X : X <> 0 -> (a + (X * b + c + d + e + f + g)) / X = b + (a + c + d + e + f + g) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pp_o_Xp_ppppp_c_dX using zutil_arith : zsimplify. + Lemma simplify_div_pp_o_pX_pppppp_c_dX a b c d e f g h X : X <> 0 -> (a + (b * X + c + d + e + f + g + h)) / X = b + (a + c + d + e + f + g + h) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pp_o_pX_pppppp_c_dX using zutil_arith : zsimplify. + Lemma simplify_div_pp_o_Xp_pppppp_c_dX a b c d e f g h X : X <> 0 -> (a + (X * b + c + d + e + f + g + h)) / X = b + (a + c + d + e + f + g + h) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pp_o_Xp_pppppp_c_dX using zutil_arith : zsimplify. + Lemma simplify_div_pp_o_pX_ppppppp_c_dX a b c d e f g h i X : X <> 0 -> (a + (b * X + c + d + e + f + g + h + i)) / X = b + (a + c + d + e + f + g + h + i) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pp_o_pX_ppppppp_c_dX using zutil_arith : zsimplify. + Lemma simplify_div_pp_o_Xp_ppppppp_c_dX a b c d e f g h i X : X <> 0 -> (a + (X * b + c + d + e + f + g + h + i)) / X = b + (a + c + d + e + f + g + h + i) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pp_o_Xp_ppppppp_c_dX using zutil_arith : zsimplify. + Lemma simplify_div_pp_o_pX_pppppppp_c_dX a b c d e f g h i j X : X <> 0 -> (a + (b * X + c + d + e + f + g + h + i + j)) / X = b + (a + c + d + e + f + g + h + i + j) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pp_o_pX_pppppppp_c_dX using zutil_arith : zsimplify. + Lemma simplify_div_pp_o_Xp_pppppppp_c_dX a b c d e f g h i j X : X <> 0 -> (a + (X * b + c + d + e + f + g + h + i + j)) / X = b + (a + c + d + e + f + g + h + i + j) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pp_o_Xp_pppppppp_c_dX using zutil_arith : zsimplify. + Lemma simplify_div_pp_o_pX_ppppppppp_c_dX a b c d e f g h i j k X : X <> 0 -> (a + (b * X + c + d + e + f + g + h + i + j + k)) / X = b + (a + c + d + e + f + g + h + i + j + k) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pp_o_pX_ppppppppp_c_dX using zutil_arith : zsimplify. + Lemma simplify_div_pp_o_Xp_ppppppppp_c_dX a b c d e f g h i j k X : X <> 0 -> (a + (X * b + c + d + e + f + g + h + i + j + k)) / X = b + (a + c + d + e + f + g + h + i + j + k) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pp_o_Xp_ppppppppp_c_dX using zutil_arith : zsimplify. + Lemma simplify_div_pp_o_pp_pX__c_dX a b c X : X <> 0 -> (a + (b + c * X)) / X = c + (a + b) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pp_o_pp_pX__c_dX using zutil_arith : zsimplify. + Lemma simplify_div_pp_o_pp_Xp__c_dX a b c X : X <> 0 -> (a + (b + X * c)) / X = c + (a + b) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pp_o_pp_Xp__c_dX using zutil_arith : zsimplify. + Lemma simplify_div_pp_o_pp_pX_p_c_dX a b c d X : X <> 0 -> (a + (b + c * X + d)) / X = c + (a + b + d) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pp_o_pp_pX_p_c_dX using zutil_arith : zsimplify. + Lemma simplify_div_pp_o_pp_Xp_p_c_dX a b c d X : X <> 0 -> (a + (b + X * c + d)) / X = c + (a + b + d) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pp_o_pp_Xp_p_c_dX using zutil_arith : zsimplify. + Lemma simplify_div_pp_o_pp_pX_pp_c_dX a b c d e X : X <> 0 -> (a + (b + c * X + d + e)) / X = c + (a + b + d + e) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pp_o_pp_pX_pp_c_dX using zutil_arith : zsimplify. + Lemma simplify_div_pp_o_pp_Xp_pp_c_dX a b c d e X : X <> 0 -> (a + (b + X * c + d + e)) / X = c + (a + b + d + e) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pp_o_pp_Xp_pp_c_dX using zutil_arith : zsimplify. + Lemma simplify_div_pp_o_pp_pX_ppp_c_dX a b c d e f X : X <> 0 -> (a + (b + c * X + d + e + f)) / X = c + (a + b + d + e + f) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pp_o_pp_pX_ppp_c_dX using zutil_arith : zsimplify. + Lemma simplify_div_pp_o_pp_Xp_ppp_c_dX a b c d e f X : X <> 0 -> (a + (b + X * c + d + e + f)) / X = c + (a + b + d + e + f) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pp_o_pp_Xp_ppp_c_dX using zutil_arith : zsimplify. + Lemma simplify_div_pp_o_pp_pX_pppp_c_dX a b c d e f g X : X <> 0 -> (a + (b + c * X + d + e + f + g)) / X = c + (a + b + d + e + f + g) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pp_o_pp_pX_pppp_c_dX using zutil_arith : zsimplify. + Lemma simplify_div_pp_o_pp_Xp_pppp_c_dX a b c d e f g X : X <> 0 -> (a + (b + X * c + d + e + f + g)) / X = c + (a + b + d + e + f + g) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pp_o_pp_Xp_pppp_c_dX using zutil_arith : zsimplify. + Lemma simplify_div_pp_o_pp_pX_ppppp_c_dX a b c d e f g h X : X <> 0 -> (a + (b + c * X + d + e + f + g + h)) / X = c + (a + b + d + e + f + g + h) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pp_o_pp_pX_ppppp_c_dX using zutil_arith : zsimplify. + Lemma simplify_div_pp_o_pp_Xp_ppppp_c_dX a b c d e f g h X : X <> 0 -> (a + (b + X * c + d + e + f + g + h)) / X = c + (a + b + d + e + f + g + h) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pp_o_pp_Xp_ppppp_c_dX using zutil_arith : zsimplify. + Lemma simplify_div_pp_o_pp_pX_pppppp_c_dX a b c d e f g h i X : X <> 0 -> (a + (b + c * X + d + e + f + g + h + i)) / X = c + (a + b + d + e + f + g + h + i) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pp_o_pp_pX_pppppp_c_dX using zutil_arith : zsimplify. + Lemma simplify_div_pp_o_pp_Xp_pppppp_c_dX a b c d e f g h i X : X <> 0 -> (a + (b + X * c + d + e + f + g + h + i)) / X = c + (a + b + d + e + f + g + h + i) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pp_o_pp_Xp_pppppp_c_dX using zutil_arith : zsimplify. + Lemma simplify_div_pp_o_pp_pX_ppppppp_c_dX a b c d e f g h i j X : X <> 0 -> (a + (b + c * X + d + e + f + g + h + i + j)) / X = c + (a + b + d + e + f + g + h + i + j) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pp_o_pp_pX_ppppppp_c_dX using zutil_arith : zsimplify. + Lemma simplify_div_pp_o_pp_Xp_ppppppp_c_dX a b c d e f g h i j X : X <> 0 -> (a + (b + X * c + d + e + f + g + h + i + j)) / X = c + (a + b + d + e + f + g + h + i + j) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pp_o_pp_Xp_ppppppp_c_dX using zutil_arith : zsimplify. + Lemma simplify_div_pp_o_pp_pX_pppppppp_c_dX a b c d e f g h i j k X : X <> 0 -> (a + (b + c * X + d + e + f + g + h + i + j + k)) / X = c + (a + b + d + e + f + g + h + i + j + k) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pp_o_pp_pX_pppppppp_c_dX using zutil_arith : zsimplify. + Lemma simplify_div_pp_o_pp_Xp_pppppppp_c_dX a b c d e f g h i j k X : X <> 0 -> (a + (b + X * c + d + e + f + g + h + i + j + k)) / X = c + (a + b + d + e + f + g + h + i + j + k) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pp_o_pp_Xp_pppppppp_c_dX using zutil_arith : zsimplify. + Lemma simplify_div_pp_o_p_o_pp_pX__c_p_c_dX a b c d e X : X <> 0 -> (a + (b + (c + d * X) + e)) / X = d + (a + b + c + e) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pp_o_p_o_pp_pX__c_p_c_dX using zutil_arith : zsimplify. + Lemma simplify_div_pp_o_p_o_pp_Xp__c_p_c_dX a b c d e X : X <> 0 -> (a + (b + (c + X * d) + e)) / X = d + (a + b + c + e) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pp_o_p_o_pp_Xp__c_p_c_dX using zutil_arith : zsimplify. + Lemma simplify_div_ppp_o_pp_pX__c_pdX a b c d e X : X <> 0 -> (a + b + (c + d * X) + e) / X = d + (a + b + c + e) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_ppp_o_pp_pX__c_pdX using zutil_arith : zsimplify. + Lemma simplify_div_ppp_o_pp_Xp__c_pdX a b c d e X : X <> 0 -> (a + b + (c + X * d) + e) / X = d + (a + b + c + e) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_ppp_o_pp_Xp__c_pdX using zutil_arith : zsimplify. + Lemma simplify_div_pppp_pXp_ppdX a b c d e f X : X <> 0 -> (a + b + c * X * d + e + f) / X = (a + b + e + f + c*d*X) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pppp_pXp_ppdX using zutil_arith : zsimplify. + Lemma simplify_div_pppp_Xpp_ppdX a b c d e f X : X <> 0 -> (a + b + X * c * d + e + f) / X = (a + b + e + f + c*d*X) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pppp_Xpp_ppdX using zutil_arith : zsimplify. + Lemma simplify_div_ppp_pXp_ppdX a b c d e X : X <> 0 -> (a + b * X * c + d + e) / X = (a + d + e + b*c*X) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_ppp_pXp_ppdX using zutil_arith : zsimplify. + Lemma simplify_div_ppp_Xpp_ppdX a b c d e X : X <> 0 -> (a + X * b * c + d + e) / X = (a + d + e + b*c*X) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_ppp_Xpp_ppdX using zutil_arith : zsimplify. + Lemma simplify_div_pp_o_p_o_pp_pXp__c_p_c_dX a b c d e f X : X <> 0 -> (a + (b + (c + d * X * e) + f)) / X = (a + b + c + f + d*e*X) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pp_o_p_o_pp_pXp__c_p_c_dX using zutil_arith : zsimplify. + Lemma simplify_div_pp_o_p_o_pp_Xpp__c_p_c_dX a b c d e f X : X <> 0 -> (a + (b + (c + X * d * e) + f)) / X = (a + b + c + f + d*e*X) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pp_o_p_o_pp_Xpp__c_p_c_dX using zutil_arith : zsimplify. + Lemma simplify_div_pp_o_pp_pXp__c_pdX a b c d e X : X <> 0 -> (a + (b + c * X * d) + e) / X = (a + b + e + c*d*X) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pp_o_pp_pXp__c_pdX using zutil_arith : zsimplify. + Lemma simplify_div_pp_o_pp_Xpp__c_pdX a b c d e X : X <> 0 -> (a + (b + X * c * d) + e) / X = (a + b + e + c*d*X) / X. + Proof. simplify_div_tac. Qed. + Hint Rewrite simplify_div_pp_o_pp_Xpp__c_pdX using zutil_arith : zsimplify. + + + (* Naming convention: [X] for thing being aggregated, [p] for plus, + [m] for minus, [_] for parentheses *) + (* Python code to generate these hints: +<< +#!/usr/bin/env python + +def sgn(v): + if v < 0: + return -1 + elif v == 0: + return 0 + elif v > 0: + return 1 + +def to_eqn(name): + vars_left = list('abcdefghijklmnopqrstuvwxyz') + ret = '' + close = '' + while name: + if name[0] == 'X': + ret += ' X' + name = name[1:] + elif not name[0].isdigit(): + ret += ' ' + vars_left[0] + vars_left = vars_left[1:] + if name: + if name[0] == 'm': ret += ' -' + elif name[0] == 'p': ret += ' +' + elif name[0].isdigit(): ret += ' %s *' % name[0] + name = name[1:] + if name and name[0] == '_': + ret += ' (' + close += ')' + name = name[1:] + if ret[-1] != 'X': + ret += ' ' + vars_left[0] + return (ret + close).strip().replace('( ', '(') + +def simplify(eqn): + counts = {} + sign_stack = [1, 1] + for i in eqn: + if i == ' ': continue + elif i == '(': sign_stack.append(sign_stack[-1]) + elif i == ')': sign_stack.pop() + elif i == '+': sign_stack.append(sgn(sign_stack[-1])) + elif i == '-': sign_stack.append(-sgn(sign_stack[-1])) + elif i == '*': continue + elif i.isdigit(): sign_stack[-1] *= int(i) + else: + counts[i] = counts.get(i,0) + sign_stack.pop() + ret = '' + for k in sorted(counts.keys()): + if counts[k] == 1: ret += ' + %s' % k + elif counts[k] == -1: ret += ' - %s' % k + elif counts[k] < 0: ret += ' - %d * %s' % (abs(counts[k]), k) + elif counts[k] > 0: ret += ' + %d * %s' % (abs(counts[k]), k) + if ret == '': ret = '0' + return ret.strip(' +') + + +def to_def(name): + eqn = to_eqn(name) + return r''' Lemma simplify_%s %s X : %s = %s. + Proof. lia. Qed. + Hint Rewrite simplify_%s : zsimplify.''' % (name, ' '.join(sorted(set(eqn) - set('*+-() 0123456789X'))), eqn, simplify(eqn), name) + +names = [] +names += ['%sX%s%sX' % (a, b, c) for a in 'mp' for b in 'mp' for c in 'mp'] +names += ['%sX%s_X%s' % (a, b, c) for a in 'mp' for b in 'mp' for c in 'mp'] +names += ['X%s%s_X%s' % (a, b, c) for a in 'mp' for b in 'mp' for c in 'mp'] +names += ['%sX%s_%sX' % (a, b, c) for a in 'mp' for b in 'mp' for c in 'mp'] +names += ['X%s%s_%sX' % (a, b, c) for a in 'mp' for b in 'mp' for c in 'mp'] +names += ['m2XpX', 'm2XpXpX'] + +print(r''' (* Python code to generate these hints: +<<''') +print(open(__file__).read()) +print(r''' +>> *)''') +for name in names: + print(to_def(name)) + + +>> *) + Lemma simplify_mXmmX a b X : a - X - b - X = - 2 * X + a - b. + Proof. lia. Qed. + Hint Rewrite simplify_mXmmX : zsimplify. + Lemma simplify_mXmpX a b X : a - X - b + X = a - b. + Proof. lia. Qed. + Hint Rewrite simplify_mXmpX : zsimplify. + Lemma simplify_mXpmX a b X : a - X + b - X = - 2 * X + a + b. + Proof. lia. Qed. + Hint Rewrite simplify_mXpmX : zsimplify. + Lemma simplify_mXppX a b X : a - X + b + X = a + b. + Proof. lia. Qed. + Hint Rewrite simplify_mXppX : zsimplify. + Lemma simplify_pXmmX a b X : a + X - b - X = a - b. + Proof. lia. Qed. + Hint Rewrite simplify_pXmmX : zsimplify. + Lemma simplify_pXmpX a b X : a + X - b + X = 2 * X + a - b. + Proof. lia. Qed. + Hint Rewrite simplify_pXmpX : zsimplify. + Lemma simplify_pXpmX a b X : a + X + b - X = a + b. + Proof. lia. Qed. + Hint Rewrite simplify_pXpmX : zsimplify. + Lemma simplify_pXppX a b X : a + X + b + X = 2 * X + a + b. + Proof. lia. Qed. + Hint Rewrite simplify_pXppX : zsimplify. + Lemma simplify_mXm_Xm a b X : a - X - (X - b) = - 2 * X + a + b. + Proof. lia. Qed. + Hint Rewrite simplify_mXm_Xm : zsimplify. + Lemma simplify_mXm_Xp a b X : a - X - (X + b) = - 2 * X + a - b. + Proof. lia. Qed. + Hint Rewrite simplify_mXm_Xp : zsimplify. + Lemma simplify_mXp_Xm a b X : a - X + (X - b) = a - b. + Proof. lia. Qed. + Hint Rewrite simplify_mXp_Xm : zsimplify. + Lemma simplify_mXp_Xp a b X : a - X + (X + b) = a + b. + Proof. lia. Qed. + Hint Rewrite simplify_mXp_Xp : zsimplify. + Lemma simplify_pXm_Xm a b X : a + X - (X - b) = a + b. + Proof. lia. Qed. + Hint Rewrite simplify_pXm_Xm : zsimplify. + Lemma simplify_pXm_Xp a b X : a + X - (X + b) = a - b. + Proof. lia. Qed. + Hint Rewrite simplify_pXm_Xp : zsimplify. + Lemma simplify_pXp_Xm a b X : a + X + (X - b) = 2 * X + a - b. + Proof. lia. Qed. + Hint Rewrite simplify_pXp_Xm : zsimplify. + Lemma simplify_pXp_Xp a b X : a + X + (X + b) = 2 * X + a + b. + Proof. lia. Qed. + Hint Rewrite simplify_pXp_Xp : zsimplify. + Lemma simplify_Xmm_Xm a b X : X - a - (X - b) = - a + b. + Proof. lia. Qed. + Hint Rewrite simplify_Xmm_Xm : zsimplify. + Lemma simplify_Xmm_Xp a b X : X - a - (X + b) = - a - b. + Proof. lia. Qed. + Hint Rewrite simplify_Xmm_Xp : zsimplify. + Lemma simplify_Xmp_Xm a b X : X - a + (X - b) = 2 * X - a - b. + Proof. lia. Qed. + Hint Rewrite simplify_Xmp_Xm : zsimplify. + Lemma simplify_Xmp_Xp a b X : X - a + (X + b) = 2 * X - a + b. + Proof. lia. Qed. + Hint Rewrite simplify_Xmp_Xp : zsimplify. + Lemma simplify_Xpm_Xm a b X : X + a - (X - b) = a + b. + Proof. lia. Qed. + Hint Rewrite simplify_Xpm_Xm : zsimplify. + Lemma simplify_Xpm_Xp a b X : X + a - (X + b) = a - b. + Proof. lia. Qed. + Hint Rewrite simplify_Xpm_Xp : zsimplify. + Lemma simplify_Xpp_Xm a b X : X + a + (X - b) = 2 * X + a - b. + Proof. lia. Qed. + Hint Rewrite simplify_Xpp_Xm : zsimplify. + Lemma simplify_Xpp_Xp a b X : X + a + (X + b) = 2 * X + a + b. + Proof. lia. Qed. + Hint Rewrite simplify_Xpp_Xp : zsimplify. + Lemma simplify_mXm_mX a b X : a - X - (b - X) = a - b. + Proof. lia. Qed. + Hint Rewrite simplify_mXm_mX : zsimplify. + Lemma simplify_mXm_pX a b X : a - X - (b + X) = - 2 * X + a - b. + Proof. lia. Qed. + Hint Rewrite simplify_mXm_pX : zsimplify. + Lemma simplify_mXp_mX a b X : a - X + (b - X) = - 2 * X + a + b. + Proof. lia. Qed. + Hint Rewrite simplify_mXp_mX : zsimplify. + Lemma simplify_mXp_pX a b X : a - X + (b + X) = a + b. + Proof. lia. Qed. + Hint Rewrite simplify_mXp_pX : zsimplify. + Lemma simplify_pXm_mX a b X : a + X - (b - X) = 2 * X + a - b. + Proof. lia. Qed. + Hint Rewrite simplify_pXm_mX : zsimplify. + Lemma simplify_pXm_pX a b X : a + X - (b + X) = a - b. + Proof. lia. Qed. + Hint Rewrite simplify_pXm_pX : zsimplify. + Lemma simplify_pXp_mX a b X : a + X + (b - X) = a + b. + Proof. lia. Qed. + Hint Rewrite simplify_pXp_mX : zsimplify. + Lemma simplify_pXp_pX a b X : a + X + (b + X) = 2 * X + a + b. + Proof. lia. Qed. + Hint Rewrite simplify_pXp_pX : zsimplify. + Lemma simplify_Xmm_mX a b X : X - a - (b - X) = 2 * X - a - b. + Proof. lia. Qed. + Hint Rewrite simplify_Xmm_mX : zsimplify. + Lemma simplify_Xmm_pX a b X : X - a - (b + X) = - a - b. + Proof. lia. Qed. + Hint Rewrite simplify_Xmm_pX : zsimplify. + Lemma simplify_Xmp_mX a b X : X - a + (b - X) = - a + b. + Proof. lia. Qed. + Hint Rewrite simplify_Xmp_mX : zsimplify. + Lemma simplify_Xmp_pX a b X : X - a + (b + X) = 2 * X - a + b. + Proof. lia. Qed. + Hint Rewrite simplify_Xmp_pX : zsimplify. + Lemma simplify_Xpm_mX a b X : X + a - (b - X) = 2 * X + a - b. + Proof. lia. Qed. + Hint Rewrite simplify_Xpm_mX : zsimplify. + Lemma simplify_Xpm_pX a b X : X + a - (b + X) = a - b. + Proof. lia. Qed. + Hint Rewrite simplify_Xpm_pX : zsimplify. + Lemma simplify_Xpp_mX a b X : X + a + (b - X) = a + b. + Proof. lia. Qed. + Hint Rewrite simplify_Xpp_mX : zsimplify. + Lemma simplify_Xpp_pX a b X : X + a + (b + X) = 2 * X + a + b. + Proof. lia. Qed. + Hint Rewrite simplify_Xpp_pX : zsimplify. + Lemma simplify_m2XpX a X : a - 2 * X + X = - X + a. + Proof. lia. Qed. + Hint Rewrite simplify_m2XpX : zsimplify. + Lemma simplify_m2XpXpX a X : a - 2 * X + X + X = a. + Proof. lia. Qed. + Hint Rewrite simplify_m2XpXpX : zsimplify. +End Z. diff --git a/src/Util/ZUtil/ZSimplify/Simple.v b/src/Util/ZUtil/ZSimplify/Simple.v new file mode 100644 index 000000000..9b5e0e9c8 --- /dev/null +++ b/src/Util/ZUtil/ZSimplify/Simple.v @@ -0,0 +1,82 @@ +Require Import Coq.ZArith.ZArith Coq.micromega.Lia Coq.omega.Omega. +Require Import Crypto.Util.ZUtil.Hints.Core. +Local Open Scope Z_scope. + +Module Z. + Lemma sub_same_minus (x y : Z) : x - (x - y) = y. + Proof. lia. Qed. + Hint Rewrite sub_same_minus : zsimplify. + Lemma sub_same_plus (x y : Z) : x - (x + y) = -y. + Proof. lia. Qed. + Hint Rewrite sub_same_plus : zsimplify. + Lemma sub_same_minus_plus (x y z : Z) : x - (x - y + z) = y - z. + Proof. lia. Qed. + Hint Rewrite sub_same_minus_plus : zsimplify. + Lemma sub_same_plus_plus (x y z : Z) : x - (x + y + z) = -y - z. + Proof. lia. Qed. + Hint Rewrite sub_same_plus_plus : zsimplify. + Lemma sub_same_minus_minus (x y z : Z) : x - (x - y - z) = y + z. + Proof. lia. Qed. + Hint Rewrite sub_same_minus_minus : zsimplify. + Lemma sub_same_plus_minus (x y z : Z) : x - (x + y - z) = z - y. + Proof. lia. Qed. + Hint Rewrite sub_same_plus_minus : zsimplify. + Lemma sub_same_minus_then_plus (x y w : Z) : x - (x - y) + w = y + w. + Proof. lia. Qed. + Hint Rewrite sub_same_minus_then_plus : zsimplify. + Lemma sub_same_plus_then_plus (x y w : Z) : x - (x + y) + w = w - y. + Proof. lia. Qed. + Hint Rewrite sub_same_plus_then_plus : zsimplify. + Lemma sub_same_minus_plus_then_plus (x y z w : Z) : x - (x - y + z) + w = y - z + w. + Proof. lia. Qed. + Hint Rewrite sub_same_minus_plus_then_plus : zsimplify. + Lemma sub_same_plus_plus_then_plus (x y z w : Z) : x - (x + y + z) + w = w - y - z. + Proof. lia. Qed. + Hint Rewrite sub_same_plus_plus_then_plus : zsimplify. + Lemma sub_same_minus_minus_then_plus (x y z w : Z) : x - (x - y - z) + w = y + z + w. + Proof. lia. Qed. + Hint Rewrite sub_same_minus_minus : zsimplify. + Lemma sub_same_plus_minus_then_plus (x y z w : Z) : x - (x + y - z) + w = z - y + w. + Proof. lia. Qed. + Hint Rewrite sub_same_plus_minus_then_plus : zsimplify. + + Lemma simplify_twice_sub_sub x y : 2 * x - (x - y) = x + y. + Proof. lia. Qed. + Hint Rewrite simplify_twice_sub_sub : zsimplify. + + Lemma simplify_twice_sub_add x y : 2 * x - (x + y) = x - y. + Proof. lia. Qed. + Hint Rewrite simplify_twice_sub_add : zsimplify. + + Lemma simplify_2XmX X : 2 * X - X = X. + Proof. omega. Qed. + Hint Rewrite simplify_2XmX : zsimplify. + + Lemma simplify_add_pos x y : Z.pos x + Z.pos y = Z.pos (x + y). + Proof. reflexivity. Qed. + Hint Rewrite simplify_add_pos : zsimplify_Z_to_pos. + Lemma simplify_add_pos10 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 + : Z.pos x0 + (Z.pos x1 + (Z.pos x2 + (Z.pos x3 + (Z.pos x4 + (Z.pos x5 + (Z.pos x6 + (Z.pos x7 + (Z.pos x8 + Z.pos x9)))))))) + = Z.pos (x0 + (x1 + (x2 + (x3 + (x4 + (x5 + (x6 + (x7 + (x8 + x9))))))))). + Proof. reflexivity. Qed. + Hint Rewrite simplify_add_pos10 : zsimplify_Z_to_pos. + Lemma simplify_mul_pos x y : Z.pos x * Z.pos y = Z.pos (x * y). + Proof. reflexivity. Qed. + Hint Rewrite simplify_mul_pos : zsimplify_Z_to_pos. + Lemma simplify_mul_pos10 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 + : Z.pos x0 * (Z.pos x1 * (Z.pos x2 * (Z.pos x3 * (Z.pos x4 * (Z.pos x5 * (Z.pos x6 * (Z.pos x7 * (Z.pos x8 * Z.pos x9)))))))) + = Z.pos (x0 * (x1 * (x2 * (x3 * (x4 * (x5 * (x6 * (x7 * (x8 * x9))))))))). + Proof. reflexivity. Qed. + Hint Rewrite simplify_mul_pos10 : zsimplify_Z_to_pos. + Lemma simplify_sub_pos x y : Z.pos x - Z.pos y = Z.pos_sub x y. + Proof. reflexivity. Qed. + Hint Rewrite simplify_sub_pos : zsimplify_Z_to_pos. + + Lemma two_sub_sub_inner_sub x y z : 2 * x - y - (x - z) = x - y + z. + Proof. clear; lia. Qed. + Hint Rewrite two_sub_sub_inner_sub : zsimplify. + + Lemma minus_minus_one : - -1 = 1. + Proof. reflexivity. Qed. + Hint Rewrite minus_minus_one : zsimplify. +End Z. |