diff options
author | Jason Gross <jagro@google.com> | 2016-08-17 10:45:07 -0700 |
---|---|---|
committer | Jason Gross <jagro@google.com> | 2016-08-17 10:49:43 -0700 |
commit | 8eb99e7fa606e4336f28b1c61d90fa2010df5b76 (patch) | |
tree | 26e85e9e532d4892ecab49738fdce61698b22fac /src/Util | |
parent | da1322d09b798dc51358308e46b85cb24cf472fa (diff) |
Add [Z.linear_solve_for], [Z.linear_substitute]
The first solves for a variable; the second does this, and then runs
[subst]. By design, they only handle addition and subtraction. They
should be easily generalizable to handle arbitrary rings (and should
probably be generalized to do so at some point).
(Also requested, if I recall correctly, by @andres-erbsen.)
Diffstat (limited to 'src/Util')
-rw-r--r-- | src/Util/Tactics.v | 7 | ||||
-rw-r--r-- | src/Util/ZUtil.v | 61 |
2 files changed, 68 insertions, 0 deletions
diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v index 880f5824a..a318f469b 100644 --- a/src/Util/Tactics.v +++ b/src/Util/Tactics.v @@ -20,6 +20,13 @@ Ltac head expr := Ltac head_hnf expr := let expr' := eval hnf in expr in head expr'. +(** [contains x expr] succeeds iff [x] appears in [expr] *) +Ltac contains search_for in_term := + idtac; + lazymatch in_term with + | appcontext[search_for] => idtac + end. + (* [pose proof defn], but only if no hypothesis of the same type exists. most useful for proofs of a proposition *) Tactic Notation "unique" "pose" "proof" constr(defn) := diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 3a96aa51e..77581d324 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -3,6 +3,7 @@ Require Import Coq.Classes.RelationClasses Coq.Classes.Morphisms. Require Import Coq.Structures.Equalities. Require Import Coq.omega.Omega Coq.micromega.Psatz Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith. Require Import Crypto.Util.NatUtil. +Require Import Crypto.Util.Tactics. Require Import Crypto.Util.Notations. Require Import Coq.Lists.List. Require Export Crypto.Util.FixCoqMistakes. @@ -1661,6 +1662,66 @@ Module Z. Proof. lia. Qed. Hint Rewrite simplify_twice_sub_add : zsimplify. + 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. + Local Ltac simplify_div_tac := intros; autorewrite with zsimplify; rewrite <- ?Z_div_plus_full_l, <- ?Z_div_plus_full by assumption; try (apply f_equal2; [ | reflexivity ]); |