Merge branch 'robbert/eunify' into 'master'

Add `eunify` tactic that lifts Coq's `unify` tactic to `open_constr`

See merge request iris/stdpp!224

CHANGELOG.md

@@ -53,6 +53,7 @@ Coq 8.8 and 8.9 are no longer supported.
   are used for `A → B1` and `A → B2` variants of `A ↔ B1 ∧ B2` lemmas.
 - Rename `Forall_Forall2` → `Forall_Forall2_diag` to be consistent with the
   names for big operators in Iris.
+- Add `eunify` tactic that lifts Coq's `unify` tactic to `open_constr`.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):

tests/eunify.ref

+"eunify_test"
+     : string
+The command has indeed failed with message:
+No matching clauses for match.
+((fix add (n m : nat) {struct n} : nat :=
+    match n with
+    | 0 => m
+    | S p => S (add p m)
+    end) x y)
+"eunify_test_evars"
+     : string
+The command has indeed failed with message:
+No matching clauses for match.

tests/eunify.v

+From stdpp Require Import tactics strings.
+
+Check "eunify_test".
+Lemma eunify_test : ∀ x y, 0 < S x + y.
+Proof.
+  intros x y.
+  (* Test that Ltac matching fails, otherwise this test is pointless *)
+  Fail
+    match goal with
+    | |- 0 < S _ => idtac
+    end.
+  (* [eunify] succeeds *)
+  match goal with
+  | |- 0 < ?x => eunify x (S _)
+  end.
+  match goal with
+  | |- 0 < ?x => let y := open_constr:(_) in eunify x (S y); idtac y
+  end.
+  lia.
+Qed.
+
+Check "eunify_test_evars".
+Lemma eunify_test_evars : ∃ x y, 0 < S x + y.
+Proof.
+  eexists _, _.
+  (* Test that Ltac matching fails, otherwise this test is pointless *)
+  Fail
+    match goal with
+    | |- 0 < S _ => idtac
+    end.
+  (* [eunify] succeeds even if the goal contains evars *)
+  match goal with
+  | |- 0 < ?x => eunify x (S _)
+  end.
+  (* Let's try to use [eunify] to instantiate the first evar *)
+  match goal with
+  | |- 0 < ?x => eunify x (1 + _)
+  end.
+  (* And the other evar *)
+  match goal with
+  | |- 0 < ?x => eunify x 2
+  end.
+  lia.
+Qed.
\ No newline at end of file

theories/tactics.v

@@ -214,6 +214,16 @@ does the converse. *)
 Ltac var_eq x1 x2 := match x1 with x2 => idtac | _ => fail 1 end.
 Ltac var_neq x1 x2 := match x1 with x2 => fail 1 | _ => idtac end.
 
+(** The tactic [eunify x y] succeeds if [x] and [y] can be unified, and fails
+otherwise. If it succeeds, it will instantiate necessary evars in [x] and [y].
+
+Contrary to Coq's standard [unify] tactic, which uses [constr] for the arguments
+[x] and [y], [eunify] uses [open_constr] so that one can use holes (i.e., [_]s).
+For example, it allows one to write [eunify x (S _)], which will test if [x]
+unifies a successor. *)
+Tactic Notation "eunify" open_constr(x) open_constr(y) :=
+  unify x y.
+
 (** Operational type class projections in recursive calls are not folded back
 appropriately by [simpl]. The tactic [csimpl] uses the [fold_classes] tactics
 to refold recursive calls of [fmap], [mbind], [omap] and [alter]. A