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

1 files changed, 7 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) :=