Commit a7e91677 authored by Ralf Jung's avatar Ralf Jung

make done and fast_done more consistent in behavior

In particular, make sure we always try eassumption before reflexivity.
parent fd41dc00
...@@ -11,6 +11,7 @@ buildjob: ...@@ -11,6 +11,7 @@ buildjob:
- make validate - make validate
only: only:
- master - master
- timing
artifacts: artifacts:
paths: paths:
- build-time.txt - build-time.txt
...@@ -217,8 +217,8 @@ Lemma step_fupd_mask_mono E1 E2 F1 F2 P : ...@@ -217,8 +217,8 @@ Lemma step_fupd_mask_mono E1 E2 F1 F2 P :
F1 F2 E1 E2 (|={E1,F2}=> P) |={E2,F1}=> P. F1 F2 E1 E2 (|={E1,F2}=> P) |={E2,F1}=> P.
Proof. Proof.
iIntros (??) "HP". iIntros (??) "HP".
iMod (fupd_intro_mask') as "HM1"; first fast_done. iMod "HP". iMod (fupd_intro_mask') as "HM1"; first done. iMod "HP".
iMod (fupd_intro_mask') as "HM2"; first fast_done. iModIntro. iMod (fupd_intro_mask') as "HM2"; first done. iModIntro.
iNext. iMod "HM2". iMod "HP". iMod "HM1". done. iNext. iMod "HM2". iMod "HP". iMod "HM1". done.
Qed. Qed.
......
...@@ -40,7 +40,11 @@ Tactic Notation "intuition" := intuition auto. ...@@ -40,7 +40,11 @@ Tactic Notation "intuition" := intuition auto.
we have x = y in the context, we will typically want to use the we have x = y in the context, we will typically want to use the
assumption and not reflexivity *) assumption and not reflexivity *)
Ltac fast_done := Ltac fast_done :=
solve [ eassumption | symmetry; eassumption | reflexivity ]. solve
[ eassumption
| symmetry; eassumption
| apply not_symmetry; eassumption
| reflexivity ].
Tactic Notation "fast_by" tactic(tac) := Tactic Notation "fast_by" tactic(tac) :=
tac; fast_done. tac; fast_done.
...@@ -50,16 +54,21 @@ to Ssreflect's [done], it does not compute the goal's [hnf] so as to avoid ...@@ -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 unfolding setoid equalities. Note that this tactic performs much better than
Coq's [easy] tactic as it does not perform [inversion]. *) Coq's [easy] tactic as it does not perform [inversion]. *)
Ltac done := Ltac done :=
trivial; intros; solve solve
[ repeat first [ repeat first
[ fast_done [ fast_done
| solve [trivial] | 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 [symmetry; trivial]
| solve [apply not_symmetry; trivial]
| discriminate | discriminate
| contradiction | contradiction
| solve [apply not_symmetry; trivial] | split
| split ] | match goal with H : ¬_ |- _ => case H; clear H; done end
| match goal with H : ¬_ |- _ => solve [case H; trivial] end ]. ]
].
Tactic Notation "by" tactic(tac) := Tactic Notation "by" tactic(tac) :=
tac; done. tac; done.
...@@ -477,12 +486,7 @@ Tactic Notation "naive_solver" tactic(tac) := ...@@ -477,12 +486,7 @@ Tactic Notation "naive_solver" tactic(tac) :=
(**i simplify and solve equalities *) (**i simplify and solve equalities *)
| |- _ => progress simplify_eq/= | |- _ => progress simplify_eq/=
(**i solve the goal *) (**i solve the goal *)
| |- _ => | |- _ => fast_done
solve
[ eassumption
| symmetry; eassumption
| apply not_symmetry; eassumption
| reflexivity ]
(**i operations that generate more subgoals *) (**i operations that generate more subgoals *)
| |- _ _ => split | |- _ _ => split
| |- Is_true (bool_decide _) => apply (bool_decide_pack _) | |- Is_true (bool_decide _) => apply (bool_decide_pack _)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment