From a7e91677b2853f55c825191b98c82cf837d1550c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 21 Nov 2016 16:21:39 +0100
Subject: [PATCH] make done and fast_done more consistent in behavior

In particular, make sure we always try eassumption before reflexivity.
---
 .gitlab-ci.yml                 |  1 +
 base_logic/lib/fancy_updates.v |  4 ++--
 prelude/tactics.v              | 26 +++++++++++++++-----------
 3 files changed, 18 insertions(+), 13 deletions(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 78e1f98a2..5c3e7df8a 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -11,6 +11,7 @@ buildjob:
   - make validate
   only:
   - master
+  - timing
   artifacts:
     paths:
     - build-time.txt
diff --git a/base_logic/lib/fancy_updates.v b/base_logic/lib/fancy_updates.v
index 5f1836dc3..e36059cc4 100644
--- a/base_logic/lib/fancy_updates.v
+++ b/base_logic/lib/fancy_updates.v
@@ -217,8 +217,8 @@ Lemma step_fupd_mask_mono E1 E2 F1 F2 P :
   F1 ⊆ F2 → E1 ⊆ E2 → (|={E1,F2}▷=> P) ⊢ |={E2,F1}▷=> P.
 Proof.
   iIntros (??) "HP".
-  iMod (fupd_intro_mask') as "HM1"; first fast_done. iMod "HP".
-  iMod (fupd_intro_mask') as "HM2"; first fast_done. iModIntro.
+  iMod (fupd_intro_mask') as "HM1"; first done. iMod "HP".
+  iMod (fupd_intro_mask') as "HM2"; first done. iModIntro.
   iNext. iMod "HM2". iMod "HP". iMod "HM1". done.
 Qed.
 
diff --git a/prelude/tactics.v b/prelude/tactics.v
index 6c9bb2693..de4e05609 100644
--- a/prelude/tactics.v
+++ b/prelude/tactics.v
@@ -40,7 +40,11 @@ Tactic Notation "intuition" := intuition auto.
    we have x = y in the context, we will typically want to use the
    assumption and not reflexivity *)
 Ltac fast_done :=
-  solve [ eassumption | symmetry; eassumption | reflexivity ].
+  solve
+    [ eassumption
+    | symmetry; eassumption
+    | apply not_symmetry; eassumption
+    | reflexivity ].
 Tactic Notation "fast_by" tactic(tac) :=
   tac; fast_done.
 
@@ -50,16 +54,21 @@ to Ssreflect's [done], it does not compute the goal's [hnf] so as to avoid
 unfolding setoid equalities. Note that this tactic performs much better than
 Coq's [easy] tactic as it does not perform [inversion]. *)
 Ltac done :=
-  trivial; intros; solve
+  solve
   [ repeat first
     [ fast_done
     | solve [trivial]
+    (* All the tactics below will introduce themselves anyway, or make no sense
+       for goals of product type. So this is a good place for us to do it. *)
+    | progress intros
     | solve [symmetry; trivial]
+    | solve [apply not_symmetry; trivial]
     | discriminate
     | contradiction
-    | solve [apply not_symmetry; trivial]
-    | split ]
-  | match goal with H : ¬_ |- _ => solve [case H; trivial] end ].
+    | split
+    | match goal with H : ¬_ |- _ => case H; clear H; done end
+    ]
+  ].
 Tactic Notation "by" tactic(tac) :=
   tac; done.
 
@@ -477,12 +486,7 @@ Tactic Notation "naive_solver" tactic(tac) :=
   (**i simplify and solve equalities *)
   | |- _ => progress simplify_eq/=
   (**i solve the goal *)
-  | |- _ =>
-    solve
-    [ eassumption
-    | symmetry; eassumption
-    | apply not_symmetry; eassumption
-    | reflexivity ]
+  | |- _ => fast_done
   (**i operations that generate more subgoals *)
   | |- _ ∧ _ => split
   | |- Is_true (bool_decide _) => apply (bool_decide_pack _)
-- 
GitLab