Commit a29598fa authored by Ralf Jung's avatar Ralf Jung

show the derived view shift rules

parent e7d481aa
This diff is collapsed.
......@@ -111,40 +111,21 @@ Module Type IRIS_HT_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP:
(** Consequence **)
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 φ'.
φ φ' -> 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].
move=>Himpl w n. move: n w e. elim/wf_nat_ind=>n0 IH w0 e Hwp.
rewrite ->unfold_wp in Hwp. rewrite unfold_wp. intros wf; intros.
edestruct (Hwp (1 w0 · wf)) as [Hval [Hstep [Hfork Hsafe]]]; try eassumption; [|].
{ rewrite assoc (comm w0) ra_op_unit. eassumption. }
split; last split; last split.
edestruct (Hwp wf) as [Hval [Hstep [Hfork Hsafe]]]; try eassumption; [].
split; last split; last split; last assumption.
- move=>Hisval. destruct (Hval Hisval) as [w2 [Hφ Hsat]]=>{Hval Hstep Hfork Hsafe}.
exists (w2 · 1 w0). split.
+ eapply (applyImpl (Himpl (exist _ e Hisval))), propsMW, Hφ.
* exists w2. reflexivity.
* omega.
* exists (1 w0). now rewrite comm.
+ now rewrite -assoc.
exists w2. split; last assumption.
eapply Himpl, Hφ.
- move=>σ' ei ei' K Hfill Hpstep. destruct (Hstep _ _ _ _ Hfill Hpstep) as [w2 [Hnext Hsat]]=>{Hval Hstep Hfork Hsafe}.
exists (w2 · 1 w0). split.
+ eapply IH; last split.
* omega.
* eapply (propsM (w':=1(w2 · 1 w0)) (w:=1 w0)); last eexact Himpl; last omega.
destruct (ra_unit_mono (1 w0) w2) as [w' Heq]. rewrite comm Heq ra_unit_idem.
exists w'. now rewrite comm.
* eapply propsMW, Hnext. eexists; now erewrite comm.
+ now rewrite -assoc.
exists w2. split; last assumption.
eapply IH; assumption.
- move=>? ? Heq. destruct (Hfork _ _ Heq) as (wfk & wret & Hnext1 & Hnext2 & Hsat)=>{Hval Hstep Hfork Hsafe}.
exists wfk (wret · 1 w0). split; last split.
+ eapply IH; last split.
* omega.
* eapply (propsM (w':=1(wret · 1 w0)) (w:=1 w0)); last eexact Himpl; last omega.
destruct (ra_unit_mono (1 w0) wret) as [w' Heq']. rewrite comm Heq' ra_unit_idem.
exists w'. now rewrite comm.
* eapply propsMW, Hnext1. eexists; now erewrite comm.
+ assumption.
+ rewrite -!assoc. rewrite <-!assoc in Hsat. assumption.
- assumption.
exists wfk wret. split; last (split; assumption).
eapply IH; assumption.
Qed.
Lemma wpPreVS m safe e φ:
......
......@@ -287,6 +287,18 @@ Module Type IRIS_PLOG (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
apply EQp; assumption || omega.
Qed.
Global Instance pvs_mproper:
Proper (equiv ==> equiv ==> equiv) pvs.
Proof.
move=>m11 m12 EQm1 m21 m22 EQm2 P w n. split=>Hvs.
- move=>wf; intros.
destruct (Hvs wf k mf σ) as [w' [HP HW]]; [assumption|de_auto_eq|now rewrite EQm1|].
exists w'. split; first assumption. now rewrite <-EQm2.
- move=>wf; intros.
destruct (Hvs wf k mf σ) as [w' [HP HW]]; [assumption|de_auto_eq|now rewrite <-EQm1|].
exists w'. split; first assumption. now rewrite EQm2.
Qed.
End PrimitiveViewShifts.
......@@ -449,6 +461,44 @@ Module Type IRIS_PLOG (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
rewrite unfold_wp; intros w'; intros; now inversion HLt.
Qed.
Global Instance wp_mproper safe:
Proper (equiv ==> equiv) (wp safe).
Proof.
move=>m1 m2 EQm e φ w n. move:n φ w e. induction n using wf_nat_ind; intros; rename H into IH.
rewrite [wp safe m1]unfold_wp [wp safe m2]unfold_wp.
split=>Hwp.
- move=>wf; intros.
destruct (Hwp wf k mf σ) as (Hval & Hstep & Hfork & Hsafe); [assumption|de_auto_eq|now rewrite EQm|].
split; last split; last split; last assumption.
+ move=>HV. specialize (Hval HV). destruct Hval as (w' & HP & HW).
exists w'. split; first assumption. now rewrite -EQm.
+ move=>? ? ? ? Hfill Hpstep. specialize (Hstep _ _ _ _ Hfill Hpstep).
destruct Hstep as (w' & Hwp' & HW). exists w'. split.
* erewrite <-IH by assumption. assumption.
* now rewrite -EQm.
+ move=>? ? Hfill. specialize (Hfork _ _ Hfill).
destruct Hfork as (wfk & wret & Hwp' & Hwp'' & HW).
exists wfk wret. split; last split.
* erewrite <-IH by assumption. assumption.
* erewrite <-IH by assumption. assumption.
* now rewrite -EQm.
- move=>wf; intros.
destruct (Hwp wf k mf σ) as (Hval & Hstep & Hfork & Hsafe); [assumption|de_auto_eq|now rewrite -EQm|].
split; last split; last split; last assumption.
+ move=>HV. specialize (Hval HV). destruct Hval as (w' & HP & HW).
exists w'. split; first assumption. now rewrite EQm.
+ move=>? ? ? ? Hfill Hpstep. specialize (Hstep _ _ _ _ Hfill Hpstep).
destruct Hstep as (w' & Hwp' & HW). exists w'. split.
* erewrite ->IH by assumption. assumption.
* now rewrite EQm.
+ move=>? ? Hfill. specialize (Hfork _ _ Hfill).
destruct Hfork as (wfk & wret & Hwp' & Hwp'' & HW).
exists wfk wret. split; last split.
* erewrite ->IH by assumption. assumption.
* erewrite ->IH by assumption. assumption.
* now rewrite EQm.
Qed.
End WeakestPre.
Section DerivedForms.
......@@ -457,21 +507,22 @@ Module Type IRIS_PLOG (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
Definition vs m1 m2 P Q : Props :=
(P pvs m1 m2 Q).
Global Instance vsProper m1 m2: Proper (equiv ==> equiv ==> equiv) (vs m1 m2).
Global Instance vsProper: Proper (equiv ==> equiv ==> equiv ==> equiv ==> equiv) vs.
Proof.
move=>P1 P2 EQP Q1 Q2 EQQ. unfold vs. apply morph_resp. apply impl_equiv; first assumption.
now rewrite EQQ.
move=>m11 m12 EQm1 m21 m22 EQm2 P1 P2 EQP Q1 Q2 EQQ. unfold vs.
apply morph_resp. apply impl_equiv; first assumption.
apply equiv_morph; last assumption.
now rewrite EQm1 EQm2.
Qed.
Definition ht safe m P e Q := (P wp safe m e Q).
Global Instance ht_proper safe m: Proper (equiv ==> equiv ==> equiv ==> equiv) (ht safe m).
Global Instance ht_proper safe: Proper (equiv ==> equiv ==> equiv ==> equiv ==> equiv) (ht safe).
Proof.
move=> P0 P1 HEQP e0 e1 HEQe Q0 Q1 HEQQ.
(* TODO these rewrites are *slow* *)
move=>m0 m1 EQm P0 P1 HEQP e0 e1 HEQe Q0 Q1 HEQQ.
unfold ht. apply morph_resp. apply impl_equiv; first assumption.
apply equiv_morph; last assumption.
hnf in HEQe. subst e1. reflexivity.
hnf in HEQe. subst e1. now rewrite EQm.
Qed.
End DerivedForms.
......
......@@ -55,10 +55,10 @@ Module Type IRIS_VS_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP:
assert (pv': (cmra_valid wt) (S (S k))).
{ eapply spredNE, pv. rewrite -Heqwt. reflexivity. }
exists pv'. split.
- rewrite /State -Heqwt. assumption.
- rewrite /= -Heqwt. assumption.
- move=>j agP Hlu. rewrite (comm de_emp) de_emp_union. move:(HM j agP)=>{HM}.
case/(_ _)/Wrap; last move=>Heq'.
{ rewrite /Invs Heqwt. exact Hlu. }
{ rewrite Heqwt. exact Hlu. }
destruct (j mf) eqn:Hm.
+ erewrite de_in_true by de_tauto.
destruct (dec_eq i j) as [EQ|NEQ].
......@@ -139,19 +139,14 @@ 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 : (* RJ TODO: Using box_conj_star, this can be weakened to a monotonicity statement. *)
(P Q) pvs m1 m2 P pvs m1 m2 Q.
Lemma pvsMon P Q m1 m2 :
P Q -> pvs m1 m2 P pvs m1 m2 Q.
Proof.
move => w0 n [HPQ HvsP].
move => HPQ w0 n HvsP.
intros wf k mf σ Hlt HD HSat.
destruct (HvsP (1 w0 · wf ) _ mf σ Hlt) as (w1 & HP & HSat2); [de_auto_eq| |].
{ rewrite assoc (comm w0) ra_op_unit. assumption. }
exists (w1 · 1 w0). split.
- eapply (applyImpl HPQ).
+ exists w1. reflexivity.
+ omega.
+ eapply propsMW, HP. eexists. erewrite comm. reflexivity.
- now rewrite -assoc.
destruct (HvsP wf _ mf σ Hlt) as (w1 & HP & HSat2); [de_auto_eq|assumption|].
exists w1. split; last assumption.
eapply HPQ, HP.
Qed.
Lemma pvsFrameMask P m1 m2 mf (HDisj : mf # m1 m2) :
......
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