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.)

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 ]);