Commit 5d6277d9 authored by Robbert Krebbers's avatar Robbert Krebbers

Use "clear -H" for set_solver.

Also, use "set_solver by tac" to specify a tactic.
parent 500002eb
Pipeline #137 passed with stage
......@@ -42,7 +42,7 @@ Module barrier_proto.
Proof.
split.
- move=>[p I]. rewrite /= /tok !mkSet_elem_of /= =>HI.
destruct p; set_solver eauto.
destruct p; set_solver by eauto.
- (* If we do the destruct of the states early, and then inversion
on the proof of a transition, it doesn't work - we do not obtain
the equalities we need. So we destruct the states late, because this
......@@ -90,7 +90,7 @@ Module barrier_proto.
i I sts.steps (State High I, {[ Change i ]}) (State High (I {[ i ]}), ).
Proof.
intros. apply rtc_once.
constructor; first constructor; rewrite /= /tok /=; [set_solver eauto..|].
constructor; first constructor; rewrite /= /tok /=; [set_solver by eauto..|].
(* TODO this proof is rather annoying. *)
apply elem_of_equiv=>t. rewrite !elem_of_union.
rewrite !mkSet_elem_of /change_tokens /=.
......
......@@ -253,19 +253,18 @@ Ltac set_unfold :=
(** Since [firstorder] fails or loops on very small goals generated by
[set_solver] already. We use the [naive_solver] tactic as a substitute.
This tactic either fails or proves the goal. *)
Tactic Notation "set_solver" tactic3(tac) :=
Tactic Notation "set_solver" "by" tactic3(tac) :=
setoid_subst;
decompose_empty;
set_unfold;
naive_solver tac.
Tactic Notation "set_solver" "-" hyp_list(Hs) "/" tactic3(tac) :=
clear Hs; set_solver tac.
Tactic Notation "set_solver" "+" hyp_list(Hs) "/" tactic3(tac) :=
revert Hs; clear; set_solver tac.
Tactic Notation "set_solver" := set_solver idtac.
Tactic Notation "set_solver" "-" hyp_list(Hs) "by" tactic3(tac) :=
clear Hs; set_solver by tac.
Tactic Notation "set_solver" "+" hyp_list(Hs) "by" tactic3(tac) :=
clear -Hs; set_solver by tac.
Tactic Notation "set_solver" := set_solver by idtac.
Tactic Notation "set_solver" "-" hyp_list(Hs) := clear Hs; set_solver.
Tactic Notation "set_solver" "+" hyp_list(Hs) :=
revert Hs; clear; set_solver.
Tactic Notation "set_solver" "+" hyp_list(Hs) := clear -Hs; set_solver.
(** * More theorems *)
Section collection.
......@@ -537,10 +536,10 @@ Section collection_monad.
Global Instance collection_fmap_mono {A B} :
Proper (pointwise_relation _ (=) ==> () ==> ()) (@fmap M _ A B).
Proof. intros f g ? X Y ?; set_solver eauto. Qed.
Proof. intros f g ? X Y ?; set_solver by eauto. Qed.
Global Instance collection_fmap_proper {A B} :
Proper (pointwise_relation _ (=) ==> () ==> ()) (@fmap M _ A B).
Proof. intros f g ? X Y [??]; split; set_solver eauto. Qed.
Proof. intros f g ? X Y [??]; split; set_solver by eauto. Qed.
Global Instance collection_bind_mono {A B} :
Proper (((=) ==> ()) ==> () ==> ()) (@mbind M _ A B).
Proof. unfold respectful; intros f g Hfg X Y ?; set_solver. Qed.
......@@ -575,12 +574,12 @@ Section collection_monad.
l mapM f k Forall2 (λ x y, x f y) l k.
Proof.
split.
- revert l. induction k; set_solver eauto.
- revert l. induction k; set_solver by eauto.
- induction 1; set_solver.
Qed.
Lemma collection_mapM_length {A B} (f : A M B) l k :
l mapM f k length l = length k.
Proof. revert l; induction k; set_solver eauto. Qed.
Proof. revert l; induction k; set_solver by eauto. Qed.
Lemma elem_of_mapM_fmap {A B} (f : A B) (g : B M A) l k :
Forall (λ x, y, y g x f y = x) l k mapM g l fmap f k = l.
Proof.
......
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