From 52ac92522d78b59d466d4d3f6d6854a7cfdfa03d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 22 Feb 2016 21:29:51 +0100
Subject: [PATCH] Make naive_solver a bit more robust.

---
 theories/tactics.v | 19 +++++++++++--------
 1 file changed, 11 insertions(+), 8 deletions(-)

diff --git a/theories/tactics.v b/theories/tactics.v
index 0166cd22..9fd53fa0 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -320,6 +320,12 @@ Lemma forall_and_distr (A : Type) (P Q : A → Prop) :
   (∀ x, P x ∧ Q x) ↔ (∀ x, P x) ∧ (∀ x, Q x).
 Proof. firstorder. Qed.
 
+(** The tactic [no_new_unsolved_evars tac] executes [tac] and fails if it
+creates any new evars. This trick is by Jonathan Leivent, see:
+https://coq.inria.fr/bugs/show_bug.cgi?id=3872 *)
+
+Ltac no_new_unsolved_evars tac := exact ltac:(tac).
+
 Tactic Notation "naive_solver" tactic(tac) :=
   unfold iff, not in *;
   repeat match goal with
@@ -353,23 +359,20 @@ Tactic Notation "naive_solver" tactic(tac) :=
   (**i use recursion to enable backtracking on the following clauses. *)
   match goal with
   (**i instantiation of the conclusion *)
-  | |- ∃ x, _ => eexists; go n
+  | |- ∃ x, _ => no_new_unsolved_evars ltac:(eexists; go n)
   | |- _ ∨ _ => first [left; go n | right; go n]
   | _ =>
     (**i instantiations of assumptions. *)
     lazymatch n with
     | S ?n' =>
       (**i we give priority to assumptions that fit on the conclusion. *)
-      match goal with 
-      | H : _ → _ |- _ =>
-        is_non_dependent H;
-        eapply H; clear H; go n'
+      match goal with
       | H : _ → _ |- _ =>
         is_non_dependent H;
-        try (eapply H; fail 2);
-        efeed pose proof H; clear H; go n'
+        no_new_unsolved_evars
+          ltac:(first [eapply H | efeed pose proof H]; clear H; go n')
       end
     end
   end
-  in iter (fun n' => go n') (eval compute in (seq 0 6)).
+  in iter (fun n' => go n') (eval compute in (seq 1 6)).
 Tactic Notation "naive_solver" := naive_solver eauto.
-- 
GitLab