From 30758aded113a62ba2222f4c032abff73c6e2c9c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 5 Mar 2016 11:19:28 +0100
Subject: [PATCH] introduce "fast_done", a tactic that *quickly* tries to solve
 the goal

---
 heap_lang/wp_tactics.v | 14 +++++++-------
 prelude/collections.v  |  2 +-
 prelude/tactics.v      | 14 ++++++++++----
 3 files changed, 18 insertions(+), 12 deletions(-)

diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index cd3a74aa3..723c911fe 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -6,14 +6,14 @@ Import uPred.
 Ltac wp_bind K :=
   lazymatch eval hnf in K with
   | [] => idtac
-  | _ => etrans; [|solve [ apply (wp_bind K) ]]; simpl
+  | _ => etrans; [|fast_by apply (wp_bind K)]; simpl
   end.
 Ltac wp_finish :=
   let rec go :=
   match goal with
-  | |- _ ⊑ ▷ _ => etrans; [|apply later_mono; go; reflexivity]
+  | |- _ ⊑ ▷ _ => etrans; [|fast_by apply later_mono; go]
   | |- _ ⊑ wp _ _ _ =>
-    etrans; [|eapply wp_value_pvs; reflexivity];
+    etrans; [|eapply wp_value_pvs; fast_done];
     (* sometimes, we will have to do a final view shift, so only apply
     pvs_intro if we obtain a consecutive wp *)
     try (eapply pvs_intro;
@@ -31,7 +31,7 @@ Tactic Notation "wp_rec" ">" :=
 (* hnf does not reduce through an of_val *)
 (*      match eval hnf in e1 with Rec _ _ _ => *)
       wp_bind K; etrans;
-         [|eapply wp_rec'; repeat rewrite /= to_of_val; reflexivity];
+         [|eapply wp_rec'; repeat rewrite /= to_of_val; fast_done];
          simpl_subst; wp_finish
 (*      end *) end)
      end).
@@ -43,7 +43,7 @@ Tactic Notation "wp_lam" ">" :=
     match eval hnf in e' with App ?e1 _ =>
 (*    match eval hnf in e1 with Rec BAnon _ _ => *)
     wp_bind K; etrans;
-       [|eapply wp_lam; repeat (reflexivity || rewrite /= to_of_val)];
+       [|eapply wp_lam; repeat (fast_done || rewrite /= to_of_val)];
        simpl_subst; wp_finish
 (*    end *) end)
   end.
@@ -62,9 +62,9 @@ Tactic Notation "wp_op" ">" :=
     | BinOp LeOp _ _ => wp_bind K; apply wp_le; wp_finish
     | BinOp EqOp _ _ => wp_bind K; apply wp_eq; wp_finish
     | BinOp _ _ _ =>
-       wp_bind K; etrans; [|eapply wp_bin_op; reflexivity]; wp_finish
+       wp_bind K; etrans; [|fast_by eapply wp_bin_op]; wp_finish
     | UnOp _ _ =>
-       wp_bind K; etrans; [|eapply wp_un_op; reflexivity]; wp_finish
+       wp_bind K; etrans; [|fast_by eapply wp_un_op]; wp_finish
     end)
   end.
 Tactic Notation "wp_op" := wp_op>; try strip_later.
diff --git a/prelude/collections.v b/prelude/collections.v
index 41610062c..13bba4fea 100644
--- a/prelude/collections.v
+++ b/prelude/collections.v
@@ -265,7 +265,7 @@ Ltac set_unfold :=
 [set_solver] already. We use the [naive_solver] tactic as a substitute.
 This tactic either fails or proves the goal. *)
 Tactic Notation "set_solver" "by" tactic3(tac) :=
-  try (reflexivity || eassumption);
+  try fast_done;
   intros; setoid_subst;
   set_unfold;
   intros; setoid_subst;
diff --git a/prelude/tactics.v b/prelude/tactics.v
index d2f4bd6da..7f6f1f1b2 100644
--- a/prelude/tactics.v
+++ b/prelude/tactics.v
@@ -34,6 +34,13 @@ is rather efficient when having big hint databases, or expensive [Hint Extern]
 declarations as the ones above. *)
 Tactic Notation "intuition" := intuition auto.
 
+(* [done] can get slow as it calls "trivial". [fast_done] can solve way less
+   goals, but it will also always finish quickly. *)
+Ltac fast_done :=
+  solve [ reflexivity | eassumption | symmetry; eassumption ].
+Tactic Notation "fast_by" tactic(tac) :=
+  tac; fast_done.
+
 (** A slightly modified version of Ssreflect's finishing tactic [done]. It
 also performs [reflexivity] and uses symmetry of negated equalities. Compared
 to Ssreflect's [done], it does not compute the goal's [hnf] so as to avoid
@@ -42,10 +49,9 @@ Coq's [easy] tactic as it does not perform [inversion]. *)
 Ltac done :=
   trivial; intros; solve
   [ repeat first
-    [ solve [trivial]
+    [ fast_done
+    | solve [trivial]
     | solve [symmetry; trivial]
-    | eassumption
-    | reflexivity
     | discriminate
     | contradiction
     | solve [apply not_symmetry; trivial]
@@ -288,7 +294,7 @@ Ltac auto_proper :=
   (* Normalize away equalities. *)
   simplify_eq;
   (* repeatedly apply congruence lemmas and use the equalities in the hypotheses. *)
-  try (f_equiv; assumption || (symmetry; assumption) || auto_proper).
+  try (f_equiv; fast_done || auto_proper).
 
 (** solve_proper solves goals of the form "Proper (R1 ==> R2)", for any
     number of relations. All the actual work is done by f_equiv;
-- 
GitLab