Commit b3c3d734 authored by Robbert Krebbers's avatar Robbert Krebbers

Let set_solver handle mkSet.

parent a1407723
......@@ -40,7 +40,7 @@ Record closed (S : states sts) (T : tokens sts) : Prop := Closed {
closed_step s1 s2 : s1 S frame_step T s1 s2 s2 S
}.
Definition up (s : state sts) (T : tokens sts) : states sts :=
mkSet (rtc (frame_step T) s).
{[ s' | rtc (frame_step T) s s' ]}.
Definition up_set (S : states sts) (T : tokens sts) : states sts :=
S = λ s, up s T.
......@@ -70,7 +70,7 @@ Global Instance up_preserving : Proper ((=) ==> flip (⊆) ==> (⊆)) up.
Proof.
intros s ? <- T T' HT ; apply elem_of_subseteq.
induction 1 as [|s1 s2 s3 [T1 T2]]; [constructor|].
eapply rtc_l; [eapply Frame_step with T1 T2|]; eauto with sts.
eapply elem_of_mkSet, rtc_l; [eapply Frame_step with T1 T2|]; eauto with sts.
Qed.
Global Instance up_proper : Proper ((=) ==> () ==> ()) up.
Proof. by intros ??? ?? [??]; split; apply up_preserving. Qed.
......@@ -128,7 +128,7 @@ Proof.
specialize (HS s' Hs'); clear Hs' S.
induction Hstep as [s|s1 s2 s3 [T1 T2 ? Hstep] ? IH]; first done.
inversion_clear Hstep; apply IH; clear IH; auto with sts.
- intros s1 s2; rewrite !elem_of_bind; intros (s&?&?) ?; exists s.
- intros s1 s2; rewrite /up; set_unfold; intros (s&?&?) ?; exists s.
split; [eapply rtc_r|]; eauto.
Qed.
Lemma closed_up s T : tok s T closed (up s T) T.
......@@ -359,9 +359,7 @@ Lemma sts_op_auth_frag_up s T :
sts_auth s sts_frag_up s T sts_auth s T.
Proof.
intros; split; [split|constructor; set_solver]; simpl.
- intros (?&?&?). destruct_conjs.
apply closed_disjoint with (up s T); first done.
apply elem_of_up.
- intros (?&[??]&?). by apply closed_disjoint with (up s T), elem_of_up.
- intros; split_and?.
+ set_solver+.
+ by apply closed_up.
......@@ -411,12 +409,9 @@ Lemma up_set_intersection S1 Sf Tf :
S1 Sf S1 up_set (S1 Sf) Tf.
Proof.
intros Hclf. apply (anti_symm ()).
+ move=>s [HS1 HSf]. split; first by apply HS1.
by apply subseteq_up_set.
+ move=>s [HS1 Hscl]. split; first done.
destruct Hscl as [s' [Hsup Hs']].
eapply closed_steps; last (hnf in Hsup; eexact Hsup); first done.
set_solver +Hs'.
+ move=>s [HS1 HSf]. split. by apply HS1. by apply subseteq_up_set.
+ move=>s [HS1 [s' [/elem_of_mkSet Hsup Hs']]]. split; first done.
eapply closed_steps, Hsup; first done. set_solver +Hs'.
Qed.
(** Inclusion *)
......
......@@ -164,7 +164,7 @@ Proof.
rewrite -sts_ownS_op; eauto using i_states_closed, low_states_closed.
set_solver.
+ move=> /= t. rewrite !elem_of_mkSet; intros [<-|<-]; set_solver.
+ rewrite !elem_of_mkSet; set_solver.
+ rewrite /= /i_states. set_solver.
+ auto using sts.closed_op, i_states_closed, low_states_closed.
Qed.
......@@ -293,7 +293,7 @@ Proof.
apply sep_mono.
* rewrite -sts_ownS_op; eauto using i_states_closed.
+ apply sts_own_weaken; eauto using sts.closed_op, i_states_closed.
rewrite !elem_of_mkSet; set_solver.
rewrite /i_states. set_solver.
+ set_solver.
* rewrite const_equiv // !left_id.
rewrite {1}[heap_ctx _]always_sep_dup {1}[sts_ctx _ _ _]always_sep_dup.
......@@ -319,7 +319,7 @@ Proof.
apply sep_mono.
* rewrite -sts_ownS_op; eauto using i_states_closed.
+ apply sts_own_weaken; eauto using sts.closed_op, i_states_closed.
rewrite !elem_of_mkSet; set_solver.
rewrite /i_states. set_solver.
+ set_solver.
* rewrite const_equiv // !left_id.
rewrite {1}[heap_ctx _]always_sep_dup {1}[sts_ctx _ _ _]always_sep_dup.
......
......@@ -36,14 +36,12 @@ Definition low_states : set state := {[ s | state_phase s = Low ]}.
Lemma i_states_closed i : sts.closed (i_states i) {[ Change i ]}.
Proof.
split.
- move=>[p I]. rewrite /= !elem_of_mkSet /= =>HI.
destruct p; set_solver by eauto.
- intros [p I]. rewrite /= /i_states /change_tok. destruct p; set_solver.
- (* 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
means we can use "destruct" instead of "inversion". *)
move=>s1 s2. rewrite !elem_of_mkSet.
intros Hs1 [T1 T2 Hdisj Hstep'].
intros s1 s2 Hs1 [T1 T2 Hdisj Hstep'].
inversion_clear Hstep' as [? ? ? ? Htrans _ _ Htok].
destruct Htrans; simpl in *; last done.
move: Hs1 Hdisj Htok. rewrite elem_of_equiv_empty elem_of_equiv.
......@@ -56,10 +54,8 @@ Qed.
Lemma low_states_closed : sts.closed low_states {[ Send ]}.
Proof.
split.
- move=>[p I]. rewrite /= /tok !elem_of_mkSet /= =>HI.
destruct p; set_solver.
- move=>s1 s2. rewrite !elem_of_mkSet.
intros Hs1 [T1 T2 Hdisj Hstep'].
- intros [p I]. rewrite /low_states. set_solver.
- intros s1 s2 Hs1 [T1 T2 Hdisj Hstep'].
inversion_clear Hstep' as [? ? ? ? Htrans _ _ Htok].
destruct Htrans; simpl in *; first by destruct p.
exfalso; set_solver.
......@@ -74,7 +70,7 @@ Lemma wait_step i I :
sts.steps (State High I, {[ Change i ]}) (State High (I {[ i ]}), ).
Proof.
intros. apply rtc_once.
constructor; first constructor; simpl; [set_solver by eauto..|].
constructor; first constructor; rewrite /= /change_tok; [set_solver by eauto..|].
(* TODO this proof is rather annoying. *)
apply elem_of_equiv=>t. rewrite !elem_of_union.
rewrite !elem_of_mkSet /change_tok /=.
......
......@@ -4,6 +4,7 @@
importantly, it implements some tactics to automatically solve goals involving
collections. *)
From prelude Require Export base tactics orders.
From prelude Require Import sets.
Instance collection_subseteq `{ElemOf A C} : SubsetEq C := λ X Y,
x, x X x Y.
......@@ -153,6 +154,9 @@ Tactic Notation "decompose_elem_of" hyp(H) :=
let rec go H :=
lazymatch type of H with
| _ => apply elem_of_empty in H; destruct H
| _ => clear H
| _ {[ _ | _ ]} => rewrite elem_of_mkSet in H
| ¬_ {[ _ | _ ]} => rewrite not_elem_of_mkSet in H
| ?x {[ ?y ]} =>
apply elem_of_singleton in H; try first [subst y | subst x]
| ?x {[ ?y ]} =>
......@@ -217,7 +221,9 @@ Ltac set_unfold :=
| context [ _ = ] => setoid_rewrite elem_of_equiv_empty_L in H
| context [ _ = _ ] => setoid_rewrite elem_of_equiv_alt_L in H
| context [ _ ] => setoid_rewrite elem_of_empty in H
| context [ _ ] => setoid_rewrite elem_of_all in H
| context [ _ {[ _ ]} ] => setoid_rewrite elem_of_singleton in H
| context [ _ {[_| _ ]} ] => setoid_rewrite elem_of_mkSet in H; simpl in H
| context [ _ _ _ ] => setoid_rewrite elem_of_union in H
| context [ _ _ _ ] => setoid_rewrite elem_of_intersection in H
| context [ _ _ _ ] => setoid_rewrite elem_of_difference in H
......@@ -237,7 +243,9 @@ Ltac set_unfold :=
| |- context [ _ = ] => setoid_rewrite elem_of_equiv_empty_L
| |- context [ _ = _ ] => setoid_rewrite elem_of_equiv_alt_L
| |- context [ _ ] => setoid_rewrite elem_of_empty
| |- context [ _ ] => setoid_rewrite elem_of_all
| |- context [ _ {[ _ ]} ] => setoid_rewrite elem_of_singleton
| |- context [ _ {[ _ | _ ]} ] => setoid_rewrite elem_of_mkSet; simpl
| |- context [ _ _ _ ] => setoid_rewrite elem_of_union
| |- context [ _ _ _ ] => setoid_rewrite elem_of_intersection
| |- context [ _ _ _ ] => setoid_rewrite elem_of_difference
......
......@@ -23,9 +23,11 @@ Instance set_difference {A} : Difference (set A) := λ X1 X2,
Instance set_collection : Collection A (set A).
Proof. split; [split | |]; by repeat intro. Qed.
Lemma elem_of_mkSet {A} (P : A Prop) x : (x {[ x | P x ]}) = P x.
Lemma elem_of_all {A} (x : A) : x True.
Proof. done. Qed.
Lemma not_elem_of_mkSet {A} (P : A Prop) x : (x {[ x | P x ]}) = (¬P x).
Lemma elem_of_mkSet {A} (P : A Prop) x : x {[ x | P x ]} P x.
Proof. done. Qed.
Lemma not_elem_of_mkSet {A} (P : A Prop) x : x {[ x | P x ]} ¬P x.
Proof. done. Qed.
Instance set_ret : MRet set := λ A (x : A), {[ x ]}.
......@@ -38,4 +40,4 @@ Instance set_join : MJoin set := λ A (XX : set (set A)),
Instance set_collection_monad : CollectionMonad set.
Proof. by split; try apply _. Qed.
Global Opaque set_union set_intersection set_difference.
Global Opaque set_elem_of set_union set_intersection set_difference.
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