Commit ae988e2f authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

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

parents 48ccc290 a983ad09
......@@ -5,31 +5,47 @@ Local Arguments valid _ _ !_ /.
Local Arguments op _ _ !_ !_ /.
Local Arguments unit _ _ !_ /.
Inductive sts {A B} (R : relation A) (tok : A set B) :=
| auth : A set B sts R tok
| frag : set A set B sts R tok.
Arguments auth {_ _ _ _} _ _.
Arguments frag {_ _ _ _} _ _.
Module sts.
Record Sts := {
state : Type;
token : Type;
trans : relation state;
tok : state set token;
}.
(* The type of bounds we can give to the state of an STS. This is the type
that we equip with an RA structure. *)
Inductive bound (sts : Sts) :=
| bound_auth : state sts set (token sts) bound sts
| bound_frag : set (state sts) set (token sts ) bound sts.
Arguments bound_auth {_} _ _.
Arguments bound_frag {_} _ _.
Section sts_core.
Context {A B : Type} (R : relation A) (tok : A set B).
Context (sts : Sts).
Infix "≼" := dra_included.
Inductive sts_equiv : Equiv (sts R tok) :=
| auth_equiv s T1 T2 : T1 T2 auth s T1 auth s T2
| frag_equiv S1 S2 T1 T2 : T1 T2 S1 S2 frag S1 T1 frag S2 T2.
Global Existing Instance sts_equiv.
Inductive step : relation (A * set B) :=
Notation state := (state sts).
Notation token := (token sts).
Notation trans := (trans sts).
Notation tok := (tok sts).
Inductive equiv : Equiv (bound sts) :=
| auth_equiv s T1 T2 : T1 T2 bound_auth s T1 bound_auth s T2
| frag_equiv S1 S2 T1 T2 : T1 T2 S1 S2
bound_frag S1 T1 bound_frag S2 T2.
Global Existing Instance equiv.
Inductive step : relation (state * set token) :=
| Step s1 s2 T1 T2 :
R s1 s2 tok s1 T1 tok s2 T2 tok s1 T1 tok s2 T2
step (s1,T1) (s2,T2).
trans s1 s2 tok s1 T1 tok s2 T2
tok s1 T1 tok s2 T2 step (s1,T1) (s2,T2).
Hint Resolve Step.
Inductive frame_step (T : set B) (s1 s2 : A) : Prop :=
Inductive frame_step (T : set token) (s1 s2 : state) : Prop :=
| Frame_step T1 T2 :
T1 (tok s1 T) step (s1,T1) (s2,T2) frame_step T s1 s2.
Hint Resolve Frame_step.
Record closed (S : set A) (T : set B) : Prop := Closed {
Record closed (S : set state) (T : set token) : Prop := Closed {
closed_ne : S ;
closed_disjoint s : s S tok s T ;
closed_step s1 s2 : s1 S frame_step T s1 s2 s2 S
......@@ -37,40 +53,50 @@ Record closed (S : set A) (T : set B) : Prop := Closed {
Lemma closed_steps S T s1 s2 :
closed S T s1 S rtc (frame_step T) s1 s2 s2 S.
Proof. induction 3; eauto using closed_step. Qed.
Global Instance sts_valid : Valid (sts R tok) := λ x,
match x with auth s T => tok s T | frag S' T => closed S' T end.
Definition up (s : A) (T : set B) : set A := mkSet (rtc (frame_step T) s).
Definition up_set (S : set A) (T : set B) : set A := S = λ s, up s T.
Global Instance sts_unit : Unit (sts R tok) := λ x,
Global Instance valid : Valid (bound sts) := λ x,
match x with
| bound_auth s T => tok s T | bound_frag S' T => closed S' T
end.
Definition up (s : state) (T : set token) : set state :=
mkSet (rtc (frame_step T) s).
Definition up_set (S : set state) (T : set token) : set state
:= S = λ s, up s T.
Global Instance unit : Unit (bound sts) := λ x,
match x with
| frag S' _ => frag (up_set S' ) | auth s _ => frag (up s )
| bound_frag S' _ => bound_frag (up_set S' )
| bound_auth s _ => bound_frag (up s )
end.
Inductive sts_disjoint : Disjoint (sts R tok) :=
Inductive disjoint : Disjoint (bound sts) :=
| frag_frag_disjoint S1 S2 T1 T2 :
S1 S2 T1 T2 frag S1 T1 frag S2 T2
| auth_frag_disjoint s S T1 T2 : s S T1 T2 auth s T1 frag S T2
| frag_auth_disjoint s S T1 T2 : s S T1 T2 frag S T1 auth s T2.
Global Existing Instance sts_disjoint.
Global Instance sts_op : Op (sts R tok) := λ x1 x2,
S1 S2 T1 T2 bound_frag S1 T1 bound_frag S2 T2
| auth_frag_disjoint s S T1 T2 : s S T1 T2
bound_auth s T1 bound_frag S T2
| frag_auth_disjoint s S T1 T2 : s S T1 T2
bound_frag S T1 bound_auth s T2.
Global Existing Instance disjoint.
Global Instance op : Op (bound sts) := λ x1 x2,
match x1, x2 with
| frag S1 T1, frag S2 T2 => frag (S1 S2) (T1 T2)
| auth s T1, frag _ T2 => auth s (T1 T2)
| frag _ T1, auth s T2 => auth s (T1 T2)
| auth s T1, auth _ T2 => auth s (T1 T2) (* never happens *)
| bound_frag S1 T1, bound_frag S2 T2 => bound_frag (S1 S2) (T1 T2)
| bound_auth s T1, bound_frag _ T2 => bound_auth s (T1 T2)
| bound_frag _ T1, bound_auth s T2 => bound_auth s (T1 T2)
| bound_auth s T1, bound_auth _ T2 =>
bound_auth s (T1 T2)(* never happens *)
end.
Global Instance sts_minus : Minus (sts R tok) := λ x1 x2,
Global Instance minus : Minus (bound sts) := λ x1 x2,
match x1, x2 with
| frag S1 T1, frag S2 T2 => frag (up_set S1 (T1 T2)) (T1 T2)
| auth s T1, frag _ T2 => auth s (T1 T2)
| frag _ T2, auth s T1 => auth s (T1 T2) (* never happens *)
| auth s T1, auth _ T2 => frag (up s (T1 T2)) (T1 T2)
| bound_frag S1 T1, bound_frag S2 T2 => bound_frag
(up_set S1 (T1 T2)) (T1 T2)
| bound_auth s T1, bound_frag _ T2 => bound_auth s (T1 T2)
| bound_frag _ T2, bound_auth s T1 =>
bound_auth s (T1 T2) (* never happens *)
| bound_auth s T1, bound_auth _ T2 => bound_frag (up s (T1 T2)) (T1 T2)
end.
Hint Extern 10 (equiv (A:=set _) _ _) => solve_elem_of : sts.
Hint Extern 10 (¬(equiv (A:=set _) _ _)) => solve_elem_of : sts.
Hint Extern 10 (base.equiv (A:=set _) _ _) => solve_elem_of : sts.
Hint Extern 10 (¬(base.equiv (A:=set _) _ _)) => solve_elem_of : sts.
Hint Extern 10 (_ _) => solve_elem_of : sts.
Hint Extern 10 (_ _) => solve_elem_of : sts.
Instance: Equivalence (() : relation (sts R tok)).
Instance: Equivalence (() : relation (bound sts)).
Proof.
split.
* by intros []; constructor.
......@@ -145,7 +171,7 @@ Proof.
unfold up_set; rewrite elem_of_bind; intros (s'&Hstep&?).
induction Hstep; eauto using closed_step.
Qed.
Global Instance sts_dra : DRA (sts R tok).
Global Instance dra : DRA (bound sts).
Proof.
split.
* apply _.
......@@ -211,40 +237,75 @@ Proof.
* solve_elem_of -Hstep Hs1 Hs2.
Qed.
End sts_core.
End sts.
Section stsRA.
Context {A B : Type} (R : relation A) (tok : A set B).
Context (sts : Sts).
Canonical Structure stsRA := validityRA (sts R tok).
Definition sts_auth (s : A) (T : set B) : stsRA := to_validity (auth s T).
Definition sts_frag (S : set A) (T : set B) : stsRA := to_validity (frag S T).
Canonical Structure RA := validityRA (bound sts).
Definition auth (s : state sts) (T : set (token sts)) : RA :=
to_validity (bound_auth s T).
Definition frag (S : set (state sts)) (T : set (token sts)) : RA :=
to_validity (bound_frag S T).
Lemma sts_update s1 s2 T1 T2 :
sts.step R tok (s1,T1) (s2,T2) sts_auth s1 T1 ~~> sts_auth s2 T2.
Lemma update_auth s1 s2 T1 T2 :
step sts (s1,T1) (s2,T2) auth s1 T1 ~~> auth s2 T2.
Proof.
intros ?; apply validity_update; inversion 3 as [|? S ? Tf|]; subst.
destruct (sts.step_closed R tok s1 s2 T1 T2 S Tf) as (?&?&?); auto.
destruct (step_closed sts s1 s2 T1 T2 S Tf) as (?&?&?); auto.
repeat (done || constructor).
Qed.
Lemma sts_frag_included S1 S2 T1 T2 Tdf :
sts.closed R tok S1 T1 sts.closed R tok S2 T2
T2 T1 Tdf T1 Tdf
S2 (S1 sts.up_set R tok S2 Tdf)
sts_frag S1 T1 sts_frag S2 T2.
Lemma sts_update_frag S1 S2 (T : set (token sts)) :
S1 S2 closed sts S2 T
frag S1 T ~~> frag S2 T.
Proof.
move=>Hcl1 Hcl2 Htk Hdf Hs. exists (sts_frag (sts.up_set R tok S2 Tdf) Tdf).
split; first split; simpl.
- intros _. split_ands.
+ done.
+ apply sts.closed_up_set.
* move=>s Hs2. move:(sts.closed_disjoint _ _ _ _ Hcl2 _ Hs2).
move=>HS Hcl. eapply validity_update; inversion 3 as [|? S ? Tf|]; subst.
- split; first done. constructor; last done. solve_elem_of.
- split; first done. constructor; solve_elem_of.
Qed.
Lemma frag_included S1 S2 T1 T2 :
closed sts S2 T2
frag S1 T1 frag S2 T2
(closed sts S1 T1 Tf, T2 T1 Tf T1 Tf
S2 (S1 up_set sts S2 Tf)).
Proof.
move=>Hcl2. split.
- intros [xf EQ]. destruct xf as [xf vf Hvf]. destruct xf as [Sf Tf|Sf Tf].
{ exfalso. inversion_clear EQ as [Hv EQ']. apply EQ' in Hcl2. simpl in Hcl2.
inversion Hcl2. }
inversion_clear EQ as [Hv EQ'].
move:(EQ' Hcl2)=>{EQ'} EQ. inversion_clear EQ as [|? ? ? ? HT HS].
destruct Hv as [Hv _]. move:(Hv Hcl2)=>{Hv} [/= Hcl1 [Hclf Hdisj]].
apply Hvf in Hclf. simpl in Hclf. clear Hvf.
inversion_clear Hdisj. split; last (exists Tf; split_ands); [done..|].
apply (anti_symm ()).
+ move=>s HS2. apply elem_of_intersection. split; first by apply HS.
by apply sts.subseteq_up_set.
+ move=>s /elem_of_intersection [HS1 Hscl]. apply HS. split; first done.
destruct Hscl as [s' [Hsup Hs']].
eapply sts.closed_steps; last (hnf in Hsup; eexact Hsup); first done.
solve_elem_of +HS Hs'.
- intros (Hcl1 & Tf & Htk & Hf & Hs).
exists (frag (up_set sts S2 Tf) Tf).
split; first split; simpl;[|done|].
+ intros _. split_ands; first done.
* apply sts.closed_up_set; last by eapply sts.closed_ne.
move=>s Hs2. move:(closed_disjoint sts _ _ Hcl2 _ Hs2).
solve_elem_of +Htk.
* by eapply sts.closed_ne.
+ constructor; last done. rewrite -Hs. by eapply sts.closed_ne.
- done.
- intros _. constructor; [ solve_elem_of +Htk | done].
Qed.
* constructor; last done. rewrite -Hs. by eapply sts.closed_ne.
+ intros _. constructor; [ solve_elem_of +Htk | done].
Qed.
Lemma frag_included' S1 S2 T :
closed sts S2 T closed sts S1 T
S2 (S1 sts.up_set sts S2 )
frag S1 T frag S2 T.
Proof.
intros. apply frag_included; first done.
split; first done. exists . split_ands; done || solve_elem_of+.
Qed.
End stsRA.
End sts.
......@@ -12,48 +12,62 @@ Module sts.
like you would use "auth_ctx" etc. *)
Export algebra.sts.sts.
Record Sts {A B} := {
st : relation A;
tok : A set B;
}.
Arguments Sts : clear implicits.
Class InG Λ Σ (i : gid) {A B} (sts : Sts A B) := {
inG :> ghost_ownership.InG Λ Σ i (stsRA sts.(st) sts.(tok));
inh :> Inhabited A;
Class InG Λ Σ (i : gid) (sts : Sts) := {
inG :> ghost_ownership.InG Λ Σ i (sts.RA sts);
inh :> Inhabited (state sts);
}.
Section definitions.
Context {Λ Σ A B} (i : gid) (sts : Sts A B) `{!InG Λ Σ i sts} (γ : gname).
Definition inv (φ : A iPropG Λ Σ) : iPropG Λ Σ :=
( s, own i γ (sts_auth sts.(st) sts.(tok) s ) φ s)%I.
Definition states (S : set A) (T: set B) : iPropG Λ Σ :=
own i γ (sts_frag sts.(st) sts.(tok) S T)%I.
Definition state (s : A) (T: set B) : iPropG Λ Σ :=
states (up sts.(st) sts.(tok) s T) T.
Definition ctx (N : namespace) (φ : A iPropG Λ Σ) : iPropG Λ Σ :=
Context {Λ Σ} (i : gid) (sts : Sts) `{!InG Λ Σ i sts} (γ : gname).
Definition inv (φ : state sts iPropG Λ Σ) : iPropG Λ Σ :=
( s, own i γ (auth sts s ) φ s)%I.
Definition in_states (S : set (state sts)) (T: set (token sts)) : iPropG Λ Σ:=
own i γ (frag sts S T)%I.
Definition in_state (s : state sts) (T: set (token sts)) : iPropG Λ Σ :=
in_states (up sts s T) T.
Definition ctx (N : namespace) (φ : state sts iPropG Λ Σ) : iPropG Λ Σ :=
invariants.inv N (inv φ).
End definitions.
Instance: Params (@inv) 8.
Instance: Params (@states) 8.
Instance: Params (@ctx) 9.
Instance: Params (@inv) 6.
Instance: Params (@in_states) 6.
Instance: Params (@in_state) 6.
Instance: Params (@ctx) 7.
Section sts.
Context {Λ Σ A B} (i : gid) (sts : Sts A B) `{!InG Λ Σ StsI sts}.
Context (φ : A iPropG Λ Σ).
Context {Λ Σ} (i : gid) (sts : Sts) `{!InG Λ Σ StsI sts}.
Context (φ : state sts iPropG Λ Σ).
Implicit Types N : namespace.
Implicit Types P Q R : iPropG Λ Σ.
Implicit Types γ : gname.
(* The same rule as implication does *not* hold, as could be shown using
sts_frag_included. *)
Lemma in_states_weaken E γ S1 S2 T :
S1 S2 closed sts S2 T
in_states StsI sts γ S1 T pvs E E (in_states StsI sts γ S2 T).
Proof.
rewrite /in_states=>Hs Hcl. apply own_update, sts_update_frag; done.
Qed.
Lemma in_state_states E γ s S T :
s S closed sts S T
in_state StsI sts γ s T pvs E E (in_states StsI sts γ S T).
Proof.
move=>Hs Hcl. apply in_states_weaken; last done.
move=>s' Hup. eapply closed_steps in Hcl;last (hnf in Hup; eexact Hup);done.
Qed.
Lemma alloc N s :
φ s pvs N N ( γ, ctx StsI sts γ N φ state StsI sts γ s (set_all sts.(tok) s)).
φ s pvs N N ( γ, ctx StsI sts γ N φ
in_state StsI sts γ s (set_all sts.(tok) s)).
Proof.
eapply sep_elim_True_r.
{ eapply (own_alloc StsI (sts_auth sts.(st) sts.(tok) s (set_all sts.(tok) s)) N).
{ eapply (own_alloc StsI (auth sts s (set_all sts.(tok) s)) N).
apply discrete_valid=>/=. solve_elem_of. }
rewrite pvs_frame_l. apply pvs_strip_pvs.
rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
transitivity ( inv StsI sts γ φ state StsI sts γ s (set_all sts.(tok) s))%I.
transitivity ( inv StsI sts γ φ
in_state StsI sts γ s (set_all sts.(tok) s))%I.
{ rewrite /inv -later_intro -(exist_intro s).
rewrite [(_ φ _)%I]comm -assoc. apply sep_mono; first done.
rewrite -own_op. apply equiv_spec, own_proper.
......@@ -68,16 +82,16 @@ Section sts.
Qed.
Lemma opened E γ S T :
( inv StsI sts γ φ states StsI sts γ S T)
pvs E E ( s, (s S) φ s own StsI γ (sts_auth sts.(st) sts.(tok) s T)).
( inv StsI sts γ φ in_states StsI sts γ S T)
pvs E E ( s, (s S) φ s own StsI γ (auth sts s T)).
Proof.
rewrite /inv /states. rewrite later_exist sep_exist_r. apply exist_elim=>s.
rewrite /inv /in_states later_exist sep_exist_r. apply exist_elim=>s.
rewrite later_sep pvs_timeless !pvs_frame_r. apply pvs_mono.
rewrite -(exist_intro s).
rewrite [(_ ▷φ _)%I]comm -!assoc -own_op -[(▷φ _ _)%I]comm.
rewrite own_valid_l discrete_validI.
rewrite -!assoc. apply const_elim_sep_l=>-[_ [Hcl Hdisj]]. simpl in Hdisj, Hcl.
inversion_clear Hdisj. rewrite const_equiv // left_id.
rewrite -!assoc. apply const_elim_sep_l=>-[_ [Hcl Hdisj]].
simpl in Hdisj, Hcl. inversion_clear Hdisj. rewrite const_equiv // left_id.
rewrite comm. apply sep_mono; first done.
apply equiv_spec, own_proper. split; first split; simpl.
- intros Hdisj. split_ands; first by solve_elem_of+.
......@@ -88,22 +102,22 @@ Section sts.
Qed.
Lemma closing E γ s T s' T' :
step sts.(st) sts.(tok) (s, T) (s', T')
( φ s' own StsI γ (sts_auth sts.(st) sts.(tok) s T))
pvs E E ( inv StsI sts γ φ state StsI sts γ s' T').
step sts (s, T) (s', T')
( φ s' own StsI γ (auth sts s T))
pvs E E ( inv StsI sts γ φ in_state StsI sts γ s' T').
Proof.
intros Hstep. rewrite /inv /states -(exist_intro s').
intros Hstep. rewrite /inv /in_states -(exist_intro s').
rewrite later_sep [(_ ▷φ _)%I]comm -assoc.
rewrite -pvs_frame_l. apply sep_mono; first done.
rewrite -later_intro.
rewrite own_valid_l discrete_validI. apply const_elim_sep_l=>Hval. simpl in Hval.
transitivity (pvs E E (own StsI γ (sts_auth sts.(st) sts.(tok) s' T'))).
{ by apply own_update, sts_update. }
rewrite own_valid_l discrete_validI. apply const_elim_sep_l=>Hval.
simpl in Hval. transitivity (pvs E E (own StsI γ (auth sts s' T'))).
{ by apply own_update, sts.update_auth. }
apply pvs_mono. rewrite -own_op. apply equiv_spec, own_proper.
split; first split; simpl.
- intros _.
set Tf := set_all sts.(tok) s T.
assert (closed (st sts) (tok sts) (up sts.(st) sts.(tok) s Tf) Tf).
assert (closed sts (up sts s Tf) Tf).
{ apply closed_up. rewrite /Tf. solve_elem_of+. }
eapply step_closed; [done..| |].
+ apply elem_of_up.
......@@ -119,11 +133,11 @@ Section sts.
Lemma states_fsa E N P (Q : V iPropG Λ Σ) γ S T :
fsaV nclose N E
P ctx StsI sts γ N φ
P (states StsI sts γ S T s,
P (in_states StsI sts γ S T s,
(s S) φ s -
fsa (E nclose N) (λ x, s' T',
(step sts.(st) sts.(tok) (s, T) (s', T')) φ s'
(state StsI sts γ s' T' - Q x)))
(step sts (s, T) (s', T')) φ s'
(in_state StsI sts γ s' T' - Q x)))
P fsa E Q.
Proof.
rewrite /ctx=>? HN Hinv Hinner.
......@@ -148,11 +162,11 @@ Section sts.
Lemma state_fsa E N P (Q : V iPropG Λ Σ) γ s0 T :
fsaV nclose N E
P ctx StsI sts γ N φ
P (state StsI sts γ s0 T s,
(s up sts.(st) sts.(tok) s0 T) φ s -
P (in_state StsI sts γ s0 T s,
(s up sts s0 T) φ s -
fsa (E nclose N) (λ x, s' T',
(step sts.(st) sts.(tok) (s, T) (s', T')) φ s'
(state StsI sts γ s' T' - Q x)))
(step sts (s, T) (s', T')) φ s'
(in_state StsI sts γ s' T' - Q x)))
P fsa E Q.
Proof.
rewrite {1}/state. apply states_fsa.
......
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