Commit e0b8224a authored by Ralf Jung's avatar Ralf Jung

prove ghost update rule

parent 3f93532c
......@@ -195,17 +195,17 @@ Module Type IRIS_CORE (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
Invs w1 i = n = Some μ.
Proof.
move=> Hval [w' Hleq] Hlu. unfold Invs. rewrite -Hleq.
simpl morph. rewrite ra_op_prod_fst {1}/ra_op /ra_op_finprod fdComposeRed.
simpl morph. rewrite {1}/ra_op /ra_op_finprod fdComposeRed.
destruct n; first exact:dist_bound.
rewrite /Invs /= in Hlu. destruct (fst w2 i) as [μ2|] eqn:Hw2; last contradiction Hlu.
destruct (fst w' i) as [μ1|] eqn:Hw1; simpl in *.
- rewrite Hlu assoc (comm _ μ). apply ra_ag_prod_dist. eapply world_invs_valid; first eexact Hval; first reflexivity.
rewrite -Hleq. rewrite /Invs. simpl morph. instantiate (1:=i).
rewrite ra_op_prod_fst {1}/ra_op /ra_op_finprod fdComposeRed. rewrite Hw2 Hw1. simpl.
rewrite {1}/ra_op /ra_op_finprod fdComposeRed. rewrite Hw2 Hw1. simpl.
now rewrite Hlu (comm μ) assoc.
- rewrite Hlu comm. apply ra_ag_prod_dist. eapply world_invs_valid; first eexact Hval; first reflexivity.
rewrite -Hleq. rewrite /Invs. simpl morph. instantiate (1:=i).
rewrite ra_op_prod_fst {1}/ra_op /ra_op_finprod fdComposeRed. rewrite Hw2 Hw1. simpl.
rewrite {1}/ra_op /ra_op_finprod fdComposeRed. rewrite Hw2 Hw1. simpl.
now rewrite comm.
Qed.
End FinmapInvs.
......@@ -354,14 +354,15 @@ Module Type IRIS_CORE (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
Lemma box_star P Q :
(P * Q) == P * Q.
Proof.
intros w n. split; (destruct n; first (intro; exact:bpred)); intros [[wP wQ] [Heq [HP HQ]]]; simpl in *.
- exists (1 w, w). split_conjs; simpl.
intros w n. split; (destruct n; first (intro; exact:bpred)); intros [[wP wQ] [Heq [HP HQ]]].
- rewrite (lock (1 w)) in Heq; simpl in Heq; unlock in Heq.
exists (1 w, w). simpl; split_conjs; simpl.
+ now rewrite ra_op_unit.
+ rewrite ra_unit_idem. eapply propsNE; first eexact Heq.
eapply propsMW, HP. eexists; now erewrite comm.
+ eapply propsNE; first eexact Heq.
eapply propsMW, HQ. eexists; now erewrite comm.
- exists (1 w, 1 w). split_conjs.
eapply propsMW, HQ. simpl. eexists; now erewrite comm.
- simpl in Heq. exists (1 w, 1 w). rewrite (lock (1w)); simpl; unlock; split_conjs.
+ rewrite /fst /snd. rewrite -{1}(ra_unit_idem w). rewrite ra_op_unit. reflexivity.
+ simpl. eapply propsNE; first (eapply cmra_unit_dist; eexact Heq).
eapply propsMW, HP. apply ra_unit_proper_pord. exists wQ; now rewrite comm.
......@@ -369,6 +370,17 @@ Module Type IRIS_CORE (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
eapply propsMW, HQ. apply ra_unit_proper_pord. exists wP; now rewrite comm.
Qed.
Lemma box_conj_star P Q :
P * Q == P Q.
Proof.
apply pord_antisym; first by eapply sc_and.
intros w n [HP HQ]. destruct n; first exact I. exists (1w, w).
split; last split; simpl.
- now rewrite ra_op_unit.
- rewrite ra_unit_idem. assumption.
- assumption.
Qed.
(* TODO RJ: show relation to implication *)
Lemma box_dup P :
......
......@@ -87,7 +87,7 @@ Module Type IRIS_HT_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP:
Qed.
(** Consequence **)
Lemma wpImpl safe m e φ φ':
Lemma wpImpl safe m e φ φ': (* RJ TODO: Using box_conj_star, this can be weakened to a monotonicity statement. *)
(all (lift_bin BI.impl φ φ')) wp safe m e φ wp safe m e φ'.
Proof.
move=>w n. move: n w e. elim/wf_nat_ind=>n0 IH w0 e [Himpl Hwp].
......
......@@ -26,7 +26,7 @@ Module Type IRIS_PLOG (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
Definition comp_finmap w0 : (nat -f> Wld) -> Wld :=
fdFold w0 (fun k w' wt => wt · w').
Global Instance comp_finmap_nexp n: Proper (dist n ==> dist n ==> dist n) comp_finmap.
Global Instance comp_finmap_dist n: Proper (dist n ==> dist n ==> dist n) comp_finmap.
Proof.
move=>w01 w02 EQw0 s1 s2 EQs. rewrite /comp_finmap.
etransitivity.
......@@ -45,7 +45,7 @@ Module Type IRIS_PLOG (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
Global Instance comp_finmap_ext: Proper (equiv ==> equiv ==> equiv) comp_finmap.
Proof.
move=>w01 w02 EQw0 s1 s2 EQs. apply dist_refl=>n.
apply comp_finmap_nexp; assumption || apply dist_refl; assumption.
apply comp_finmap_dist; assumption || apply dist_refl; assumption.
Qed.
Lemma comp_finmap_remove w0 (s: nat -f> Wld) i w:
......@@ -73,17 +73,17 @@ Module Type IRIS_PLOG (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
rewrite /comp_finmap in IH. apply IH.
Qed.
Lemma comp_finmap_move w1 w0 f:
comp_finmap (w0 · w1) f == comp_finmap w0 f · w1.
Lemma comp_finmap_move w0 w1 f:
comp_finmap (w0 · w1) f == w0 · comp_finmap w1 f.
Proof.
rewrite /comp_finmap. revert f. apply:fdRect.
- move=>f1 f2 EQf IH.
etransitivity; last (etransitivity; first eapply IH).
+ now rewrite EQf.
+ apply ra_op_proper; last reflexivity. now rewrite EQf.
+ f_equiv. now rewrite EQf.
- rewrite !fdFoldEmpty. reflexivity.
- move=>k v f Hnew IH. erewrite !fdFoldAdd by assumption.
rewrite -assoc (comm v) assoc. apply ra_op_proper; last reflexivity.
rewrite assoc. apply ra_op_proper; last reflexivity.
eapply IH.
Qed.
......@@ -115,17 +115,16 @@ Module Type IRIS_PLOG (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
w0 comp_finmap w0 s.
Proof.
exists (comp_finmap (1 w0) s).
rewrite -comp_finmap_move ra_op_unit. reflexivity.
rewrite comm -comp_finmap_move comm ra_op_unit. reflexivity.
Qed.
(* Go through some struggle to even write down world satisfaction... *)
Local Open Scope finmap_scope.
Lemma world_inv_val {w} {s : nat -f> Wld} {n}:
let wt := comp_finmap w s in
Lemma world_inv_val {wt n}:
forall (pv: cmra_valid wt n) {i agP} (Heq: (Invs wt) i = n = Some agP), cmra_valid agP n.
Proof.
intros wt pv i agP Heq.
intros pv i agP Heq.
destruct wt as [I O]. destruct pv as [HIval _]. specialize (HIval i).
simpl Invs in Heq. destruct (I i).
- eapply spredNE, HIval. apply cmra_valid_dist.
......@@ -134,21 +133,42 @@ Module Type IRIS_PLOG (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
- destruct n; first exact:bpred. destruct Heq.
Qed.
Definition wsatTotal n' σ s m wt :=
exists pv : (cmra_valid wt (S n')),
(State wt ex_own σ) /\
forall i agP (Heq: (Invs wt) i = S n' = Some agP),
match (i m)%de, s i with
| true , Some w => let P := ra_ag_unInj agP (S n') (HVal:=world_inv_val pv Heq) in
unhalved (ı P) w n'
| false, None => True
| _ , _ => False
end.
Global Instance wsatTotal_proper n' σ s:
Proper (equiv ==> dist (S n') ==> equiv) (wsatTotal n' σ s).
Proof.
apply proper_sym_impl_iff_2; try apply _; [].
move=>m1 m2 EQm wt1 wt2 EQwt. move=>[pv [HS HI]].
assert (pv': cmra_valid wt2 (S n')).
{ eapply spredNE, pv. apply cmra_valid_dist. assumption. }
exists pv'. split.
{ rewrite <-HS. apply pordR. destruct EQwt as [_ [HwtS _]].
symmetry. exact HwtS. }
move=>i agP Heq.
move:(HI i agP). case/(_ _)/Wrap; last move=>{HI} Heq' HI.
{ rewrite -Heq. rewrite EQwt. reflexivity. }
rewrite -EQm. destruct (i m1)%de; last exact HI.
destruct (s i); last exact HI.
simpl. simpl in HI. erewrite ra_ag_unInj_pi. eassumption.
Qed.
(* It may be possible to use "later_sp" here, but let's avoid indirections where possible. *)
Definition wsatF σ m w n :=
match n with
| O => True
| S n' => exists s : nat -f> Wld,
let wt := comp_finmap w s in
exists pv : (cmra_valid wt n),
(State wt ex_own σ) /\
forall i agP (Heq: (Invs wt) i = n = Some agP),
match (i m)%de, s i with
| true , Some w => let P := ra_ag_unInj agP n (HVal:=world_inv_val pv Heq) in
unhalved (ı P) w n'
| false, None => True
| _ , _ => False
end
let wt := comp_finmap w s in
wsatTotal n' σ s m wt
end.
Program Definition wsat σ m w : SPred :=
......@@ -180,20 +200,10 @@ Module Type IRIS_PLOG (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
eapply dist_spred_simpl2; try apply _; [].
intros m1 m2 w1 w2 m Hlt EQm EQw. destruct m; first reflexivity.
destruct n as [| n]; [now inversion Hlt |].
intros [s [pv [HS HI]]]; exists s; intro wt.
assert (Hwt: comp_finmap w1 s = S m = wt).
{ subst wt. rewrite EQw. reflexivity. }
assert (pv': cmra_valid wt (S m)).
{ eapply spredNE, pv. apply cmra_valid_dist. assumption. }
exists pv'. split.
{ rewrite <-HS. apply pordR. destruct Hwt as [_ [HwtS _]].
symmetry. exact HwtS. }
move=>i agP Heq.
move:(HI i agP). case/(_ _)/Wrap; last move=>{HI} Heq' HI.
{ rewrite -Heq. rewrite Hwt. reflexivity. }
rewrite -EQm. destruct (i m1)%de; last exact HI.
destruct (s i); last exact HI.
simpl. simpl in HI. erewrite ra_ag_unInj_pi. eassumption.
intros [s HwsT]; exists s; intro wt.
eapply wsatTotal_proper, HwsT; symmetry; first assumption.
rewrite /wt. eapply comp_finmap_dist; last reflexivity.
eapply mono_dist, EQw. omega.
Qed.
Global Instance wsat_equiv σ : Proper (equiv ==> equiv ==> equiv) (wsat σ).
......
......@@ -50,8 +50,8 @@ Module Type IRIS_VS_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP:
clear HLu HInv HP.
exists (fdStrongUpdate i None rs). intros wt.
assert (Heqwt: comp_finmap (w · wf) rs == wt).
{ rewrite /wt -assoc (comm wi) assoc (comp_finmap_move wi).
rewrite -comp_finmap_remove; last now rewrite HLr. reflexivity. }
{ rewrite /wt (comm _ wi) -assoc (comp_finmap_move wi).
rewrite (comm wi) -comp_finmap_remove; last now rewrite HLr. reflexivity. }
assert (pv': (cmra_valid wt) (S (S k))).
{ eapply spredNE, pv. rewrite -Heqwt. reflexivity. }
exists pv'. split.
......@@ -93,7 +93,7 @@ Module Type IRIS_VS_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP:
{ move:(HD i). clear. de_tauto. }
destruct (rs i); first move=> [].
move=>_. reflexivity. }
rewrite -(comp_finmap_move w) -assoc (comm wf) assoc ra_op_unit.
rewrite -(comm w) -(comp_finmap_move w) assoc (comm _ (1w)) ra_op_unit.
reflexivity. }
assert (pv': (cmra_valid wt) (S (S k))).
{ eapply spredNE, pv. rewrite -Heqwt. reflexivity. }
......@@ -101,9 +101,9 @@ Module Type IRIS_VS_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP:
- rewrite /State -Heqwt. assumption.
- move=>j agP Hlu. destruct (dec_eq i j) as [EQ|NEQ].
+ subst j. erewrite de_in_true by de_tauto.
rewrite fdStrongUpdate_eq. clear HS HM. simpl in *.
rewrite fdStrongUpdate_eq. clear HS HM. simpl in HP.
eapply spredNE, dpred, HP; last omega.
rewrite ->Heqwt, ->Hlu in HeqP. simpl in HeqP.
rewrite ->Heqwt, ->Hlu in HeqP. simpl. simpl in HeqP.
etransitivity; last first.
* assert(Heq:=halve_eq (T:=Props) (S k)). apply Heq=>{Heq}.
eapply (met_morph_nonexp ı). eapply ra_ag_unInj_dist.
......@@ -144,7 +144,7 @@ Module Type IRIS_VS_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP:
eapply propsMN, HP. omega.
Qed.
Lemma pvsImpl P Q m1 m2 :
Lemma pvsImpl P Q m1 m2 : (* RJ TODO: Using box_conj_star, this can be weakened to a monotonicity statement. *)
(P Q) pvs m1 m2 P pvs m1 m2 Q.
Proof.
move => w0 n [HPQ HvsP].
......@@ -182,7 +182,7 @@ Module Type IRIS_VS_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP:
eapply mono_dist, HEr. omega. }
exists (w2 · wq). split.
- exists (w2, wq). split; last split.
+ simpl. reflexivity.
+ rewrite [ra_op]lock. simpl. reflexivity.
+ assumption.
+ apply propsMN, HQ. omega.
- now rewrite -assoc.
......@@ -198,28 +198,28 @@ Module Type IRIS_VS_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP:
Definition ownLP (P : RL.res -> Prop) : {s : RL.res | P s} -n> Props :=
ownL <M< inclM.
Lemma pvsGhostUpd m rl (P : RL.res -> Prop) (HU : rl P) :
ownL rl pvs m m (xist (ownLP P)).
Lemma pvsGhostUpd m g (P : RL.res -> Prop) (HU : g P) :
ownL g pvs m m (xist (ownLP P)).
Proof.
unfold ownLP. intros w n [rp' rl'] HG w'; intros.
destruct HE as [rs [ Hsat HE] ]. rewrite <-assoc in Hsat. destruct Hsat as [Hval Hst].
destruct HG as [ [rdp rdl] [_ EQrl] ]. simpl in EQrl. clear rdp.
destruct (HU (rdl · snd(rf · comp_map rs))) as [rsl [HPrsl HCrsl] ].
- clear - Hval EQrl. eapply ra_prod_valid in Hval. destruct Hval as [_ Hsnd].
rewrite ->assoc, (comm rl), EQrl.
rewrite ra_op_prod_snd in Hsnd. exact Hsnd.
- exists w' (rp', rsl).
split; first reflexivity. split.
+ exists (exist _ rsl HPrsl). simpl.
exists (rp', 1:RL.res). simpl.
rewrite ra_op_unit ra_op_unit2. split; reflexivity.
+ exists rs. split; [| assumption]; clear HE. rewrite <-assoc. split; [eapply ra_prod_valid; split|].
* clear - Hval. eapply ra_prod_valid in Hval. destruct Hval as [Hfst _].
rewrite ra_op_prod_fst in Hfst.
rewrite ra_op_prod_fst. exact Hfst.
* clear -HCrsl. rewrite ->!assoc, (comm rsl), <-assoc in HCrsl.
apply ra_op_valid2 in HCrsl. rewrite ra_op_prod_snd. exact HCrsl.
* clear -Hst. rewrite ra_op_prod_fst. rewrite ra_op_prod_fst in Hst. exact Hst.
unfold ownLP. intros w n. destruct n; first (intros; exact:bpred).
intros [g' Hg'] wf; intros.
destruct HE as [rs HwsT ]. simpl in HwsT. rewrite ->comp_finmap_move in HwsT.
destruct HwsT as [pv [HS HI]]. move:(pv). move/cmra_prod_valid=>[HIval]. move/cmra_prod_valid=>[HSval Hgval].
destruct w as [I0 [S0 g0]]. simpl in Hg'.
destruct (HU (g' · Res (comp_finmap wf rs))) as [g1 [HP HVal1] ].
- clear - Hgval Hg'. simpl in Hgval. now rewrite assoc (comm g) Hg'.
- exists (I0, (S0, g1 · g')). split.
+ simpl. exists (exist _ _ HP). simpl.
eexists. now erewrite comm.
+ exists rs. simpl. rewrite comp_finmap_move. clear HP Hgval.
assert (pv':(cmra_valid ((I0, (S0, g1 · g')) · comp_finmap wf rs)) (S (S k))).
{ split; last split; try assumption; [].
now rewrite ->assoc in HVal1. }
exists pv'. split; first assumption.
move=>i agP Heq. move:(HI i agP Heq).
destruct (i _); last tauto.
destruct (rs i); last tauto.
move=>H. erewrite ra_ag_unInj_pi. eassumption.
Qed.
Program Definition inv' m : Props -n> {n : nat | m n} -n> Props :=
......
......@@ -117,6 +117,11 @@ Section PairsCMRA.
+ move=>n. split; eapply cmra_ra_valid; eapply H.
- move=>[s1 t1] [s2 t2] n H. split; eapply cmra_op_valid; eapply H.
Qed.
Lemma cmra_prod_valid {p n} :
cmra_valid p n <-> cmra_valid (fst p) n /\ cmra_valid (snd p) n.
Proof. by move: p=>[s t]. Qed.
End PairsCMRA.
Section PairsMap.
......
Require Import Ssreflect.ssreflect.
Require Import CSetoid List ListSet.
Require Import Omega CSetoid List ListSet.
Set Bullet Behavior "Strict Subproofs".
......@@ -140,6 +140,20 @@ Section FilterDup.
End FilterDup.
Section ListMax.
Definition list_max := fold_right max 0.
Lemma list_gax_ge l n:
In n l -> n <= list_max l.
Proof.
revert n. induction l; intros n HIn.
- destruct HIn.
- simpl. apply NPeano.Nat.max_le_iff. destruct HIn as [Heq|HIn].
+ left. subst. reflexivity.
+ right. now apply IHl.
Qed.
End ListMax.
Section Fold.
Context {V T: Type} {eqT: relation T} {eqRT: Equivalence eqT}.
......
......@@ -189,13 +189,11 @@ Section Pairs.
Global Instance ra_unit_prod : RA_unit (S * T) := fun st => (1 (fst st), 1 (snd st)).
Global Instance ra_op_prod : RA_op (S * T) :=
fun st1 st2 =>
match st1, st2 with
| (s1, t1), (s2, t2) => (s1 · s2, t1 · t2)
end.
fun st1 st2 => (fst st1 · fst st2, snd st1 · snd st2).
Arguments ra_op_prod !st1 !st2 /.
Global Instance ra_valid_prod : RA_valid (S * T) :=
fun st => match st with (s, t) => ra_valid s /\ ra_valid t
end.
fun st => ra_valid (fst st) /\ ra_valid (snd st).
Arguments ra_valid_prod !st /.
Global Instance ra_prod : RA (S * T).
Proof.
split.
......
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