Commit 3207ffe1 authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

parents 1b172b22 a1407723
...@@ -163,8 +163,8 @@ Proof. ...@@ -163,8 +163,8 @@ Proof.
+ apply pvs_mono. + apply pvs_mono.
rewrite -sts_ownS_op; eauto using i_states_closed, low_states_closed. rewrite -sts_ownS_op; eauto using i_states_closed, low_states_closed.
set_solver. set_solver.
+ move=> /= t. rewrite !mkSet_elem_of; intros [<-|<-]; set_solver. + move=> /= t. rewrite !elem_of_mkSet; intros [<-|<-]; set_solver.
+ rewrite !mkSet_elem_of; set_solver. + rewrite !elem_of_mkSet; set_solver.
+ auto using sts.closed_op, i_states_closed, low_states_closed. + auto using sts.closed_op, i_states_closed, low_states_closed.
Qed. Qed.
...@@ -293,7 +293,7 @@ Proof. ...@@ -293,7 +293,7 @@ Proof.
apply sep_mono. apply sep_mono.
* rewrite -sts_ownS_op; eauto using i_states_closed. * rewrite -sts_ownS_op; eauto using i_states_closed.
+ apply sts_own_weaken; eauto using sts.closed_op, i_states_closed. + apply sts_own_weaken; eauto using sts.closed_op, i_states_closed.
rewrite !mkSet_elem_of; set_solver. rewrite !elem_of_mkSet; set_solver.
+ set_solver. + set_solver.
* rewrite const_equiv // !left_id. * rewrite const_equiv // !left_id.
rewrite {1}[heap_ctx _]always_sep_dup {1}[sts_ctx _ _ _]always_sep_dup. rewrite {1}[heap_ctx _]always_sep_dup {1}[sts_ctx _ _ _]always_sep_dup.
...@@ -319,7 +319,7 @@ Proof. ...@@ -319,7 +319,7 @@ Proof.
apply sep_mono. apply sep_mono.
* rewrite -sts_ownS_op; eauto using i_states_closed. * rewrite -sts_ownS_op; eauto using i_states_closed.
+ apply sts_own_weaken; eauto using sts.closed_op, i_states_closed. + apply sts_own_weaken; eauto using sts.closed_op, i_states_closed.
rewrite !mkSet_elem_of; set_solver. rewrite !elem_of_mkSet; set_solver.
+ set_solver. + set_solver.
* rewrite const_equiv // !left_id. * rewrite const_equiv // !left_id.
rewrite {1}[heap_ctx _]always_sep_dup {1}[sts_ctx _ _ _]always_sep_dup. rewrite {1}[heap_ctx _]always_sep_dup {1}[sts_ctx _ _ _]always_sep_dup.
......
...@@ -18,7 +18,7 @@ Inductive prim_step : relation state := ...@@ -18,7 +18,7 @@ Inductive prim_step : relation state :=
| ChangePhase I : prim_step (State Low I) (State High I). | ChangePhase I : prim_step (State Low I) (State High I).
Definition change_tok (I : gset gname) : set token := Definition change_tok (I : gset gname) : set token :=
mkSet (λ t, match t with Change i => i I | Send => False end). {[ t | match t with Change i => i I | Send => False end ]}.
Definition send_tok (p : phase) : set token := Definition send_tok (p : phase) : set token :=
match p with Low => | High => {[ Send ]} end. match p with Low => | High => {[ Send ]} end.
Definition tok (s : state) : set token := Definition tok (s : state) : set token :=
...@@ -28,29 +28,27 @@ Global Arguments tok !_ /. ...@@ -28,29 +28,27 @@ Global Arguments tok !_ /.
Canonical Structure sts := sts.STS prim_step tok. Canonical Structure sts := sts.STS prim_step tok.
(* The set of states containing some particular i *) (* The set of states containing some particular i *)
Definition i_states (i : gname) : set state := Definition i_states (i : gname) : set state := {[ s | i state_I s ]}.
mkSet (λ s, i state_I s).
(* The set of low states *) (* The set of low states *)
Definition low_states : set state := Definition low_states : set state := {[ s | state_phase s = Low ]}.
mkSet (λ s, if state_phase s is Low then True else False).
Lemma i_states_closed i : sts.closed (i_states i) {[ Change i ]}. Lemma i_states_closed i : sts.closed (i_states i) {[ Change i ]}.
Proof. Proof.
split. split.
- move=>[p I]. rewrite /= !mkSet_elem_of /= =>HI. - move=>[p I]. rewrite /= !elem_of_mkSet /= =>HI.
destruct p; set_solver by eauto. destruct p; set_solver by eauto.
- (* If we do the destruct of the states early, and then inversion - (* 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 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 the equalities we need. So we destruct the states late, because this
means we can use "destruct" instead of "inversion". *) means we can use "destruct" instead of "inversion". *)
move=>s1 s2. rewrite !mkSet_elem_of. move=>s1 s2. rewrite !elem_of_mkSet.
intros Hs1 [T1 T2 Hdisj Hstep']. intros Hs1 [T1 T2 Hdisj Hstep'].
inversion_clear Hstep' as [? ? ? ? Htrans _ _ Htok]. inversion_clear Hstep' as [? ? ? ? Htrans _ _ Htok].
destruct Htrans; simpl in *; last done. destruct Htrans; simpl in *; last done.
move: Hs1 Hdisj Htok. rewrite elem_of_equiv_empty elem_of_equiv. move: Hs1 Hdisj Htok. rewrite elem_of_equiv_empty elem_of_equiv.
move=> ? /(_ (Change i)) Hdisj /(_ (Change i)); move: Hdisj. move=> ? /(_ (Change i)) Hdisj /(_ (Change i)); move: Hdisj.
rewrite elem_of_intersection elem_of_union !mkSet_elem_of. rewrite elem_of_intersection elem_of_union !elem_of_mkSet.
intros; apply dec_stable. intros; apply dec_stable.
destruct p; set_solver. destruct p; set_solver.
Qed. Qed.
...@@ -58,13 +56,13 @@ Qed. ...@@ -58,13 +56,13 @@ Qed.
Lemma low_states_closed : sts.closed low_states {[ Send ]}. Lemma low_states_closed : sts.closed low_states {[ Send ]}.
Proof. Proof.
split. split.
- move=>[p I]. rewrite /= /tok !mkSet_elem_of /= =>HI. - move=>[p I]. rewrite /= /tok !elem_of_mkSet /= =>HI.
destruct p; set_solver. destruct p; set_solver.
- move=>s1 s2. rewrite !mkSet_elem_of. - move=>s1 s2. rewrite !elem_of_mkSet.
intros Hs1 [T1 T2 Hdisj Hstep']. intros Hs1 [T1 T2 Hdisj Hstep'].
inversion_clear Hstep' as [? ? ? ? Htrans _ _ Htok]. inversion_clear Hstep' as [? ? ? ? Htrans _ _ Htok].
destruct Htrans; simpl in *; first by destruct p. destruct Htrans; simpl in *; first by destruct p.
set_solver. exfalso; set_solver.
Qed. Qed.
(* Proof that we can take the steps we need. *) (* Proof that we can take the steps we need. *)
...@@ -79,7 +77,7 @@ Proof. ...@@ -79,7 +77,7 @@ Proof.
constructor; first constructor; simpl; [set_solver by eauto..|]. constructor; first constructor; simpl; [set_solver by eauto..|].
(* TODO this proof is rather annoying. *) (* TODO this proof is rather annoying. *)
apply elem_of_equiv=>t. rewrite !elem_of_union. apply elem_of_equiv=>t. rewrite !elem_of_union.
rewrite !mkSet_elem_of /change_tok /=. rewrite !elem_of_mkSet /change_tok /=.
destruct t as [j|]; last set_solver. destruct t as [j|]; last set_solver.
rewrite elem_of_difference elem_of_singleton. rewrite elem_of_difference elem_of_singleton.
destruct (decide (i = j)); set_solver. destruct (decide (i = j)); set_solver.
...@@ -96,11 +94,11 @@ Proof. ...@@ -96,11 +94,11 @@ Proof.
- destruct p; set_solver. - destruct p; set_solver.
(* This gets annoying... and I think I can see a pattern with all these proofs. Automatable? *) (* This gets annoying... and I think I can see a pattern with all these proofs. Automatable? *)
- apply elem_of_equiv=>t. destruct t; last set_solver. - apply elem_of_equiv=>t. destruct t; last set_solver.
rewrite !mkSet_elem_of !not_elem_of_union !not_elem_of_singleton rewrite !elem_of_mkSet !not_elem_of_union !not_elem_of_singleton
not_elem_of_difference elem_of_singleton !(inj_iff Change). not_elem_of_difference elem_of_singleton !(inj_iff Change).
destruct p; naive_solver. destruct p; naive_solver.
- apply elem_of_equiv=>t. destruct t as [j|]; last set_solver. - apply elem_of_equiv=>t. destruct t as [j|]; last set_solver.
rewrite !mkSet_elem_of !not_elem_of_union !not_elem_of_singleton rewrite !elem_of_mkSet !not_elem_of_union !not_elem_of_singleton
not_elem_of_difference elem_of_singleton !(inj_iff Change). not_elem_of_difference elem_of_singleton !(inj_iff Change).
destruct (decide (i1 = j)) as [->|]; first tauto. destruct (decide (i1 = j)) as [->|]; first tauto.
destruct (decide (i2 = j)) as [->|]; intuition. destruct (decide (i2 = j)) as [->|]; intuition.
......
(* Copyright (c) 2012-2015, Robbert Krebbers. *) (* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *)
(** This file implements sets as functions into Prop. *) (** This file implements sets as functions into Prop. *)
From prelude Require Export prelude. From prelude Require Export tactics.
Record set (A : Type) : Type := mkSet { set_car : A Prop }. Record set (A : Type) : Type := mkSet { set_car : A Prop }.
Add Printing Constructor set.
Arguments mkSet {_} _. Arguments mkSet {_} _.
Arguments set_car {_} _ _. Arguments set_car {_} _ _.
Instance set_all {A} : Top (set A) := mkSet (λ _, True). Notation "{[ x | P ]}" := (mkSet (λ x, P))
Instance set_empty {A} : Empty (set A) := mkSet (λ _, False). (at level 1, format "{[ x | P ]}") : C_scope.
Instance set_singleton {A} : Singleton A (set A) := λ x, mkSet (x =).
Instance set_elem_of {A} : ElemOf A (set A) := λ x X, set_car X x. Instance set_elem_of {A} : ElemOf A (set A) := λ x X, set_car X x.
Instance set_union {A} : Union (set A) := λ X1 X2, mkSet (λ x, x X1 x X2).
Instance set_all {A} : Top (set A) := {[ _ | True ]}.
Instance set_empty {A} : Empty (set A) := {[ _ | False ]}.
Instance set_singleton {A} : Singleton A (set A) := λ y, {[ x | y = x ]}.
Instance set_union {A} : Union (set A) := λ X1 X2, {[ x | x X1 x X2 ]}.
Instance set_intersection {A} : Intersection (set A) := λ X1 X2, Instance set_intersection {A} : Intersection (set A) := λ X1 X2,
mkSet (λ x, x X1 x X2). {[ x | x X1 x X2 ]}.
Instance set_difference {A} : Difference (set A) := λ X1 X2, Instance set_difference {A} : Difference (set A) := λ X1 X2,
mkSet (λ x, x X1 x X2). {[ x | x X1 x X2 ]}.
Instance set_collection : Collection A (set A). Instance set_collection : Collection A (set A).
Proof. by split; [split | |]; repeat intro. Qed. Proof. split; [split | |]; by repeat intro. Qed.
Lemma mkSet_elem_of {A} (f : A Prop) x : (x mkSet f) = f x. Lemma elem_of_mkSet {A} (P : A Prop) x : (x {[ x | P x ]}) = P x.
Proof. done. Qed. Proof. done. Qed.
Lemma mkSet_not_elem_of {A} (f : A Prop) x : (x mkSet f) = (¬f x). Lemma not_elem_of_mkSet {A} (P : A Prop) x : (x {[ x | P x ]}) = (¬P x).
Proof. done. Qed. Proof. done. Qed.
Instance set_ret : MRet set := λ A (x : A), {[ x ]}. Instance set_ret : MRet set := λ A (x : A), {[ x ]}.
Instance set_bind : MBind set := λ A B (f : A set B) (X : set A), Instance set_bind : MBind set := λ A B (f : A set B) (X : set A),
mkSet (λ b, a, b f a a X). mkSet (λ b, a, b f a a X).
Instance set_fmap : FMap set := λ A B (f : A B) (X : set A), Instance set_fmap : FMap set := λ A B (f : A B) (X : set A),
mkSet (λ b, a, b = f a a X). {[ b | a, b = f a a X ]}.
Instance set_join : MJoin set := λ A (XX : set (set A)), Instance set_join : MJoin set := λ A (XX : set (set A)),
mkSet (λ a, X, a X X XX). {[ a | X, a X X XX ]}.
Instance set_collection_monad : CollectionMonad set. Instance set_collection_monad : CollectionMonad set.
Proof. by split; try apply _. Qed. Proof. by split; try apply _. Qed.
......
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