Commit 160cc780 authored by Ralf Jung's avatar Ralf Jung

prove the last missing view shift rules

parent cae9dd85
......@@ -33,23 +33,34 @@ Module Type IRIS_DERIVED_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C)
apply vsValid. apply bot_false.
Qed.
Lemma vsNotOwnInvalid m1 m2 l
(Hnval: ~l):
valid (vs m1 m2 (ownL l) ).
Lemma vsOwnValid m l:
valid (vs m m (ownL l) (ownL l pcmconst (sp_const (l)))).
Proof.
apply vsValid. etransitivity.
{ rewrite ownL_iff /own_ghost. reflexivity. }
apply xist_L=>I. apply xist_L=>S. rewrite {1}/met_morph /mkNMorph {1}/morph.
etransitivity; last by eapply pvsNotOwnInvalid.
apply and_R; split; last reflexivity.
apply and_impl.
(* We now prove this in the model. It does not really warrant it's own metatheory... *)
move=>w n. destruct n; first (intro; exact:bpred).
intros [[Hw' Heq] Hval]. simpl in *.
tauto.
etransitivity; first by eapply pvsOwnValid.
eapply pvsMon. apply and_pord.
- rewrite ownL_iff. apply (xist_R I). apply (xist_R S). reflexivity.
- (* We now prove this in the model. It does not really warrant it's own metatheory... *)
move=>w n. destruct n; first (intro; exact:bpred). simpl. tauto.
Qed.
(* TODO RJ: ownS * ownS => ⊥ *)
Lemma vsOwnSTwice m σ1 σ2:
valid (vs m m (ownS σ1 * ownS σ2) ).
Proof.
apply vsValid. etransitivity.
{ rewrite !ownS_iff /own_state. reflexivity. }
etransitivity; first apply xist_sc. apply xist_L=>I1. simpl.
etransitivity; first apply xist_sc. apply xist_L=>g1. simpl.
etransitivity; first apply xist_sc_r. apply xist_L=>I2. simpl.
etransitivity; first apply xist_sc_r. apply xist_L=>g2. simpl.
rewrite /const. rewrite- own_sc. etransitivity; first eapply pvsOwnValid.
eapply pvsMon. rewrite ->and_projR.
(* We now prove this in the model. It does not really warrant it's own metatheory... *)
move=>w n [_ [HSval _]]. destruct n; first exact:bpred.
destruct HSval.
Qed.
Lemma vsTimeless m P : (* TODO RJ: the box is missing in the appendix? timeless will become a modality anyway. *)
(timeless P) vs m m (P) P.
......
......@@ -308,6 +308,9 @@ Module Type IRIS_HT_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP:
End HoareTripleProperties.
Global Opaque pvs.
Global Opaque wpF.
End IRIS_HT_RULES.
Module IrisHTRules (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PROP R) (CORE: IRIS_CORE RL C R WP) (PLOG: IRIS_PLOG RL C R WP CORE) : IRIS_HT_RULES RL C R WP CORE PLOG.
......
......@@ -198,7 +198,7 @@ Module Type IRIS_PLOG (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
end.
Program Definition wsat σ m w : SPred :=
mkSPred (wsatF σ m w) _ _.
p[(wsatF σ m w)].
Next Obligation.
intros n1 n2 HLe. do 2 (destruct n2; first (intro; exact I)).
do 2 (destruct n1; first (exfalso; omega)).
......@@ -242,11 +242,11 @@ Module Type IRIS_PLOG (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
Local Obligation Tactic := intros.
Program Definition preVS m1 m2 P w : SPred :=
mkSPred (fun n => forall (wf: Wld) k mf σ (HLe : S k < n)
p[(fun n => forall (wf: Wld) k mf σ (HLe : S k < n)
(HD : mf # m1 m2)
(HE : wsat σ (m1 mf) (w · wf) (S (S k))),
exists w', P w' (S (S k))
/\ wsat σ (m2 mf) (w' · wf) (S (S k))) _ _.
/\ wsat σ (m2 mf) (w' · wf) (S (S k)))].
Next Obligation.
inversion HLe.
Qed.
......@@ -350,7 +350,7 @@ Module Type IRIS_PLOG (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
(* Define the function wp will be a fixed-point of *)
Program Definition wpF safe m : (expr -n> vPred -n> Props) -> (expr -n> vPred -n> Props) :=
fun WP => n[(fun e => n[(fun φ => m[(fun w => mkSPred (wpFP safe m WP e φ w) _ _)])])].
fun WP => n[(fun e => n[(fun φ => m[(fun w => p[(wpFP safe m WP e φ w)] )])])].
Next Obligation.
intro. intros. inversion HLt.
Qed.
......
......@@ -256,25 +256,24 @@ Module Type IRIS_VS_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP:
tauto.
Qed.
Lemma pvsNotOwnInvalid m1 m2 w:
(pcmconst (cmra_valid w) ) own w pvs m1 m2 .
Lemma pvsOwnValid m w:
own w pvs m m (own w pcmconst (cmra_valid w)).
Proof.
intros w0 n. destruct n; first (intro; exact:bpred).
move=>[Hinval [wr Heq]] wf; intros. exfalso.
change ((⊥:Props) w0 (S (S k))).
eapply (applyImpl Hinval); [reflexivity|omega|].
rewrite /= /const. destruct HE as [rs [pv _]].
eapply cmra_valid_ord, spredNE, dpred, pv; last omega; last first.
- apply cmra_valid_dist. simpl in Heq. rewrite comp_finmap_move.
eapply cmra_op_dist; last reflexivity.
symmetry. eapply mono_dist, Heq. omega.
- eexists. erewrite (comm _ w), <-assoc. reflexivity.
move=>Hown wf; intros. exists w0.
split; last done. split; first (eapply propsMN, Hown; omega).
destruct HE as [rs [pv _]]. simpl. destruct Hown as [wr Heq]. simpl in Heq.
eapply cmra_valid_ord, spredNE, pv; last first.
- eapply cmra_valid_dist. erewrite comp_finmap_move.
eapply cmra_op_dist; last reflexivity. symmetry. eapply mono_dist, Heq. omega.
- rewrite -assoc. eexists. now erewrite (comm _ w).
Qed.
(* TODO: can always get own of some unit *)
End ViewShiftProps.
Global Opaque pvs.
Global Opaque wpF.
End IRIS_VS_RULES.
Module IrisVSRules (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PROP R) (CORE: IRIS_CORE RL C R WP) (PLOG: IRIS_PLOG RL C R WP CORE): IRIS_VS_RULES RL C R WP CORE PLOG.
......
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