Commit 0de5b6a9 authored by Filip Sieczkowski's avatar Filip Sieczkowski

Propositions are now uniform predicates over monoid elements (not 0);

definitions pushed through, some lemmas commented out for now.
parent 8688ed6e
......@@ -4,7 +4,7 @@ Require Import RecDom.PCM RecDom.UPred RecDom.BI RecDom.PreoMet RecDom.Finmap.
Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
Module Import L := Lang RP RL C.
Module R <: PCM_T.
Module Import R <: PCM_T.
Definition res := (RP.res * RL.res)%type.
Instance res_op : PCM_op res := _.
Instance res_unit : PCM_unit res := _.
......@@ -12,8 +12,6 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
End R.
Module Import WP := WorldProp R.
Definition res := option R.res.
Delimit Scope iris_scope with iris.
Local Open Scope iris_scope.
......@@ -37,7 +35,7 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
Local Obligation Tactic := intros; resp_set || eauto with typeclass_instances.
Program Definition box : Props -n> Props :=
n[(fun p => m[(fun w => mkUPred (fun n r => p w n 1%pcm) _)])].
n[(fun p => m[(fun w => mkUPred (fun n r => p w n (pcm_unit _)) _)])].
Next Obligation.
intros n m r s HLe _ Hp; rewrite HLe; assumption.
Qed.
......@@ -66,7 +64,7 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
intros n1 n2 _ _ HLe _; apply mono_dist; now auto with arith.
Qed.
Program Definition intEq (t1 t2 : T) : Props := pcmconst (intEqP t1 t2).
Definition intEq (t1 t2 : T) : Props := pcmconst (intEqP t1 t2).
Instance intEq_equiv : Proper (equiv ==> equiv ==> equiv) intEqP.
Proof.
......@@ -126,23 +124,6 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
End Invariants.
(** Ownership **)
Definition own (r : res) : Props :=
pcmconst (up_cr (pord r)).
Definition injFst (r : option RP.res) : res :=
option_map (fun r => (r, pcm_unit _)) r.
Definition injSnd (r : option RL.res) : res :=
option_map (fun r => (pcm_unit _, r)) r.
(** Physical part **)
Definition ownP (r : RP.res) : Props :=
own (injFst (Some r)).
(** Logical part **)
Definition ownL (r : RL.res) : Props :=
own (injSnd (Some r)).
Notation "□ p" := (box p) (at level 30, right associativity) : iris_scope.
Notation "⊤" := (top : Props) : iris_scope.
Notation "⊥" := (bot : Props) : iris_scope.
......@@ -156,64 +137,82 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
Notation "∀ x : T , p" := (all n[(fun x : T => p)] : Props) (at level 60, x ident, no associativity) : iris_scope.
Notation "∃ x : T , p" := (all n[(fun x : T => p)] : Props) (at level 60, x ident, no associativity) : iris_scope.
(** Ownership **)
Definition ownR (r : res) : Props :=
pcmconst (up_cr (pord r)).
(** Physical part **)
Definition ownRP (r : RP.res) : Props :=
ownR (r, pcm_unit _).
(** Logical part **)
Definition ownRL (r : RL.res) : Props :=
ownR (pcm_unit _, r).
(** Proper ghost state: ownership of logical w/ possibility of undefined **)
Definition ownL (r : option RL.res) : Props :=
match r with
| Some r => ownRL r
| None =>
end.
Section Erasure.
Local Open Scope pcm_scope.
Local Open Scope bi_scope.
Local Instance eqRes : Setoid res := discreteType.
(* First, we need to erase a finite map. This won't be pretty, for
now, since the library does not provide enough
constructs. Hopefully we can provide a fold that'd work for
that at some point
*)
Fixpoint comp_list (xs : list res) : res :=
Fixpoint comp_list (xs : list res) : option res :=
match xs with
| nil => 1
| (x :: xs)%list => x · comp_list xs
| (x :: xs)%list => Some x · comp_list xs
end.
Definition cod (m : nat -f> res) : list res := List.map snd (findom_t m).
Definition erase (m : nat -f> res) : res := comp_list (cod m).
Definition erase (m : nat -f> res) : option res := comp_list (cod m).
Lemma erase_remove (rs : nat -f> res) i r (HLu : rs i = Some r) :
erase rs = r · erase (fdRemove i rs).
erase rs == Some r · erase (fdRemove i rs).
Proof.
destruct rs as [rs rsP]; unfold erase, cod, findom_f in *; simpl in *.
induction rs as [| [j s] ]; [discriminate |]; simpl in *.
destruct rs as [rs rsP]; unfold erase, cod, findom_f in *; simpl findom_t in *.
induction rs as [| [j s] ]; [discriminate |]; simpl comp_list; simpl in HLu.
destruct (comp i j); [inversion HLu; reflexivity | discriminate |].
simpl; rewrite IHrs by eauto using SS_tail.
rewrite !assoc; f_equal; rewrite comm; reflexivity.
simpl comp_list; rewrite IHrs by eauto using SS_tail.
rewrite !assoc, (comm (Some s)); reflexivity.
Qed.
Lemma erase_insert_new (rs : nat -f> res) i r (HNLu : rs i = None) :
r · erase rs = erase (fdUpdate i r rs).
Some r · erase rs == erase (fdUpdate i r rs).
Proof.
destruct rs as [rs rsP]; unfold erase, cod, findom_f in *; simpl in *.
induction rs as [| [j s] ]; simpl in *; [reflexivity |].
destruct rs as [rs rsP]; unfold erase, cod, findom_f in *; simpl findom_t in *.
induction rs as [| [j s] ]; [reflexivity | simpl comp_list; simpl in HNLu].
destruct (comp i j); [discriminate | reflexivity |].
simpl; rewrite <- IHrs by eauto using SS_tail.
rewrite !assoc; f_equal; rewrite comm; reflexivity.
simpl comp_list; rewrite <- IHrs by eauto using SS_tail.
rewrite !assoc, (comm (Some r)); reflexivity.
Qed.
Lemma erase_insert_old (rs : nat -f> res) i r1 r2 (HLu : rs i = Some r1) :
r2 · erase rs = erase (fdUpdate i (r1 · r2) rs).
Lemma erase_insert_old (rs : nat -f> res) i r1 r2 r
(HLu : rs i = Some r1) (HEq : Some r1 · Some r2 == Some r) :
Some r2 · erase rs == erase (fdUpdate i r rs).
Proof.
destruct rs as [rs rsP]; unfold erase, cod, findom_f in *; simpl in *.
induction rs as [| [j s] ]; [discriminate |]; simpl in *.
destruct rs as [rs rsP]; unfold erase, cod, findom_f in *; simpl findom_t in *.
induction rs as [| [j s] ]; [discriminate |]; simpl comp_list; simpl in HLu.
destruct (comp i j); [inversion HLu; subst; clear HLu | discriminate |].
- simpl; rewrite assoc, (comm r2); reflexivity.
- simpl; rewrite <- IHrs by eauto using SS_tail.
rewrite !assoc, (comm r2); reflexivity.
- simpl comp_list; rewrite assoc, (comm (Some r2)), <- HEq; reflexivity.
- simpl comp_list; rewrite <- IHrs by eauto using SS_tail.
rewrite !assoc, (comm (Some r2)); reflexivity.
Qed.
Global Instance preo_unit : preoType () := disc_preo ().
(* XXX: logical state omitted, since it looks weird. Also, later over the whole deal. *)
Program Definition erasure (σ : state) (m : mask) (r s : res) (w : Wld) : UPred () :=
(mkUPred (fun n _ =>
erase_state (option_map fst (r · s)) σ
erase_state (option_map fst (Some r · Some s)) σ
/\ exists rs : nat -f> res,
erase rs = s /\
erase rs == Some s /\
forall i (Hm : m i),
(i dom rs <-> i dom w) /\
forall π ri (HLw : w i == Some π) (HLrs : rs i == Some ri),
......@@ -263,22 +262,26 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
Local Open Scope mask_scope.
Local Open Scope pcm_scope.
Local Obligation Tactic := intros.
Local Existing Instance eqRes.
Program Definition preVS (m1 m2 : mask) (p : Props) (w : Wld) : UPred res :=
mkUPred (fun n r => forall w1 s rf mf σ k (HSub : w w1) (HLe : k <= n)
(HGt : k > 0) (HD : mf # m1 m2)
(HE : erasure σ (m1 mf) (r · rf) s w1 @ k),
exists w2 r' s', w1 w2 /\ p w2 k r' /\
erasure σ (m2 mf) (r' · rf) s' w2 @ k) _.
mkUPred (fun n r => forall w1 rf rr s mf σ k (HSub : w w1) (HLe : k < n)
(HD : mf # m1 m2) (HEq : Some r · Some rf == Some rr)
(HE : erasure σ (m1 mf) rr s w1 @ S k),
exists w2 r' rr' s',
w1 w2 /\ p w2 (S k) r' /\ Some r' · Some rf == Some rr'
/\ erasure σ (m2 mf) rr' s' w2 @ S k) _.
Next Obligation.
intros n1 n2 r1 r2 HLe [rd HR] HP; intros.
destruct (HP w1 s (rd · rf) mf σ k) as [w2 [r1' [s' [HW [HP' HE'] ] ] ] ]; try assumption; [| |].
- etransitivity; eassumption.
- rewrite assoc, (comm r1), HR; assumption.
- exists w2 (rd · r1') s'; split; [assumption | split].
+ eapply uni_pred, HP'; [| eexists]; reflexivity.
+ rewrite (comm rd), <- assoc; assumption.
rewrite <- HR, (comm (Some rd)), <- assoc in HEq; clear r2 HR.
destruct (Some rd · Some rf) as [rf' |] eqn: HR;
[| erewrite comm, pcm_op_zero in HEq by apply _; contradiction].
destruct (HP w1 rf' rr s mf σ k) as [w2 [r1' [rr' [s' [HW [HP' [HR' HE'] ] ] ] ] ] ]; try assumption; [|].
- eauto with arith.
- rewrite <- HR, assoc in HR'; clear rf' HR HEq HP.
destruct (Some r1' · Some rd) as [r2' |] eqn: HR;
[| erewrite pcm_op_zero in HR' by apply _; contradiction].
exists w2 r2' rr' s'; split; [assumption | split; [| split; assumption] ].
eapply uni_pred, HP'; [| exists rd; rewrite comm, HR]; reflexivity.
Qed.
Program Definition pvs (m1 m2 : mask) : Props -n> Props :=
......@@ -294,19 +297,19 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
intros w1 w2 EQw n' r HLt; destruct n as [| n]; [now inversion HLt |]; split; intros HP w2'; intros.
- symmetry in EQw; assert (HDE := extend_dist _ _ _ _ EQw HSub).
assert (HSE := extend_sub _ _ _ _ EQw HSub); specialize (HP (extend w2' w1)).
edestruct HP as [w1'' [r' [s' [HW HH] ] ] ]; try eassumption; clear HP; [ | ].
edestruct HP as [w1'' [r' [rr' [s' [HW HH] ] ] ] ]; try eassumption; clear HP; [ | ].
+ eapply erasure_dist, HE; [symmetry; eassumption | now eauto with arith].
+ symmetry in HDE; assert (HDE' := extend_dist _ _ _ _ HDE HW).
assert (HSE' := extend_sub _ _ _ _ HDE HW); destruct HH as [HP HE'];
exists (extend w1'' w2') r' s'; repeat split; [assumption | |].
assert (HSE' := extend_sub _ _ _ _ HDE HW); destruct HH as [HP [HR HE'] ];
exists (extend w1'' w2') r' rr' s'; split; [assumption | split; [| split; [assumption |] ] ].
* eapply (met_morph_nonexp _ _ p), HP ; [symmetry; eassumption | now eauto with arith].
* eapply erasure_dist, HE'; [symmetry; eassumption | now eauto with arith].
- assert (HDE := extend_dist _ _ _ _ EQw HSub); assert (HSE := extend_sub _ _ _ _ EQw HSub); specialize (HP (extend w2' w2)).
edestruct HP as [w1'' [r' [s' [HW HH] ] ] ]; try eassumption; clear HP; [ | ].
edestruct HP as [w1'' [r' [rr' [s' [HW HH] ] ] ] ]; try eassumption; clear HP; [ | ].
+ eapply erasure_dist, HE; [symmetry; eassumption | now eauto with arith].
+ symmetry in HDE; assert (HDE' := extend_dist _ _ _ _ HDE HW).
assert (HSE' := extend_sub _ _ _ _ HDE HW); destruct HH as [HP HE'];
exists (extend w1'' w2') r' s'; repeat split; [assumption | |].
assert (HSE' := extend_sub _ _ _ _ HDE HW); destruct HH as [HP [HR HE'] ];
exists (extend w1'' w2') r' rr' s'; split; [assumption | split; [| split; [assumption |] ] ].
* eapply (met_morph_nonexp _ _ p), HP ; [symmetry; eassumption | now eauto with arith].
* eapply erasure_dist, HE'; [symmetry; eassumption | now eauto with arith].
Qed.
......@@ -321,11 +324,11 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
Qed.
Next Obligation.
intros p1 p2 EQp w n' r HLt; split; intros HP w1; intros.
- edestruct HP as [w2 [r' [s' [HW [HP' HE'] ] ] ] ]; try eassumption; [].
clear HP; repeat eexists; try eassumption; [].
- edestruct HP as [w2 [r' [rr' [s' [HW [HP' HE'] ] ] ] ] ]; try eassumption; [].
clear HP; repeat (eexists; try eassumption); [].
apply EQp; [now eauto with arith | assumption].
- edestruct HP as [w2 [r' [s' [HW [HP' HE'] ] ] ] ]; try eassumption; [].
clear HP; repeat eexists; try eassumption; [].
- edestruct HP as [w2 [r' [rr' [s' [HW [HP' HE'] ] ] ] ] ]; try eassumption; [].
clear HP; repeat (eexists; try eassumption); [].
apply EQp; [now eauto with arith | assumption].
Qed.
......@@ -338,7 +341,8 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
Local Open Scope mask_scope.
Local Open Scope pcm_scope.
Local Open Scope bi_scope.
Local Existing Instance eqRes.
Implicit Types (p q r : Props) (i : nat) (m : mask).
Definition mask_sing i := mask_set mask_emp i True.
......@@ -351,18 +355,33 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
apply ı in HInv; rewrite (isoR p) in HInv.
(* get rid of the invisible 1/2 *)
do 8 red in HInv.
destruct k as [| k]; [now inversion HGt |].
destruct HE as [HES [rs [HE HM] ] ].
destruct (rs i) as [ri |] eqn: HLr.
- exists w' (r · ri) (erase (fdRemove i rs)); split; [reflexivity | split; [| split] ].
- rewrite erase_remove with (i := i) (r := ri) in HE by assumption.
destruct (Some rr · Some s) as [ss |] eqn: HR; setoid_rewrite HR in HES;
[| contradiction (erase_state_nonzero _ HES) ].
destruct (Some r · Some rf) as [rr' |] eqn: HR1;
[simpl in HEq; subst rr' | contradiction].
destruct (Some ri · erase (fdRemove i rs)) as [s' |] eqn: HR2;
[simpl in HE; subst s' | contradiction].
assert (HEq : Some r · Some ri · Some rf · erase (fdRemove i rs) == Some ss).
{ rewrite <- (assoc (Some r)), (comm (Some ri)), assoc, HR1, <- assoc, HR2, HR; reflexivity. }
clear HR HR1 HR2; destruct (Some r · Some ri) as [rri |] eqn: HR1;
[| now erewrite !pcm_op_zero in HEq by apply _].
destruct (Some rri · Some rf) as [rr' |] eqn: HR2;
[| now erewrite pcm_op_zero in HEq by apply _].
destruct (erase (fdRemove i rs)) as [s' |] eqn: HRS;
[| now erewrite comm, pcm_op_zero in HEq by apply _].
exists w' rri rr' s'; split; [reflexivity | split; [| split; [rewrite HR2; reflexivity | split] ] ].
+ simpl; eapply HInv; [now auto with arith |].
specialize (HSub i); rewrite HLu in HSub.
eapply uni_pred, HM with i; [| exists r | | | rewrite HLr]; try reflexivity; [|].
eapply uni_pred, HM with i; [| exists r; rewrite <- HR1 | | | rewrite HLr]; try reflexivity; [|].
* left; unfold mask_sing, mask_set.
destruct (Peano_dec.eq_nat_dec i i); tauto.
* symmetry; destruct (w' i); [assumption | contradiction].
+ rewrite <- assoc, (comm ri), assoc, <- (assoc _ ri), <- erase_remove, HE; assumption.
+ exists (fdRemove i rs); split; [reflexivity | intros j Hm].
+ destruct (Some rr' · Some s') as [ss' |] eqn: HR; [| contradiction].
setoid_rewrite HR; simpl in HEq; subst; assumption.
+ exists (fdRemove i rs); split; [rewrite HRS; reflexivity | intros j Hm].
destruct Hm as [| Hm]; [contradiction |]; specialize (HD j); simpl in HD.
unfold mask_sing, mask_set in HD; destruct (Peano_dec.eq_nat_dec i j);
[subst j; contradiction HD; tauto | clear HD].
......@@ -374,10 +393,7 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
destruct (Peano_dec.eq_nat_dec i i); tauto.
Qed.
(* XXX: move up *)
Implicit Types (p q r : Props) (i : nat) (m : mask).
Lemma vsClose i p :
(*Lemma vsClose i p :
valid (vs mask_emp (mask_sing i) (inv i p * ▹ p) ⊤).
Proof.
intros pw nn r w _; clear r pw.
......@@ -410,39 +426,43 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
subst r; rewrite assoc; eexists; reflexivity.
+ rewrite fdLookup_in_strong, fdUpdate_neq, <- fdLookup_in_strong by assumption.
auto.
Qed.
Qed.*)
Lemma vsTrans p q r m1 m2 m3 (HMS : m2 m1 m3) :
vs m1 m2 p q vs m2 m3 q r vs m1 m3 p r.
Proof.
intros w' n r1 [Hpq Hqr] w HSub; specialize (Hpq _ HSub); rewrite HSub in Hqr; clear w' HSub.
intros np rp HLe HS Hp w1; intros; specialize (Hpq _ _ HLe HS Hp).
edestruct Hpq as [w2 [rq [sq [HSw12 [Hq HEq] ] ] ] ]; try eassumption; [|].
edestruct Hpq as [w2 [rq [rrq [sq [HSw12 [Hq [HEq' HErq] ] ] ] ] ] ]; try eassumption; [|].
{ (* XXX: possible lemma *)
clear - HD HMS.
intros j [Hmf Hm12]; apply (HD j); split; [assumption |].
destruct Hm12 as [Hm1 | Hm2]; [left; assumption | apply HMS, Hm2].
}
clear HS; assert (HS : 1 rq) by (exists rq; rewrite comm; apply pcm_op_unit, _).
clear HS; assert (HS : pcm_unit _ rq) by (exists rq; now erewrite comm, pcm_op_unit by apply _).
rewrite <- HLe, HSub in Hqr; specialize (Hqr _ HSw12); clear Hpq HE w HSub Hp.
edestruct (Hqr k _ HLe0 HS Hq w2) as [w3 [rr [sr [HSw23 [Hr HEr] ] ] ] ];
try (reflexivity || eassumption); [|].
edestruct (Hqr (S k) _ HLe0 HS Hq w2) as [w3 [rR [rrR [sR [HSw23 [Hr [HR HEr] ] ] ] ] ] ];
try (reflexivity || eassumption); [now auto with arith | |].
{ (* XXX: possible lemma *)
clear - HD HMS.
intros j [Hmf Hm23]; apply (HD j); split; [assumption |].
destruct Hm23 as [Hm2 | Hm3]; [apply HMS, Hm2 | right; assumption].
}
clear HEq Hq HS.
setoid_rewrite HSw12; eauto 6.
setoid_rewrite HSw12; eauto 8.
Qed.
(* Warning: weak statement *)
Lemma vsEnt p q m1 m2 (HEnt : p q) :
valid (vs m1 m2 p q).
Lemma vsEnt p q m :
(p q) vs m m p q.
Proof.
Admitted.
intros w' n r1 Himp w HSub; rewrite HSub in Himp; clear w' HSub.
intros np rp HLe HS Hp w1; intros.
exists w1 rp rr s; split; [reflexivity | split; [| split; assumption ] ].
eapply Himp; [assumption | now eauto with arith | exists rp; now erewrite comm, pcm_op_unit by apply _ |].
unfold lt in HLe0; rewrite HLe0, <- HSub; assumption.
Qed.
Lemma vsFrame p q r m1 m2 mf (HDisj : mf # m1 m2) :
(* Lemma vsFrame p q r m1 m2 mf (HDisj : mf # m1 ∪ m2) :
vs m1 m2 p q ⊑ vs (m1 ∪ mf) (m2 ∪ mf) (p * r) (q * r).
Proof.
intros w' n r1 HVS w HSub; specialize (HVS _ HSub); clear w' r1 HSub.
......@@ -459,7 +479,7 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
+ rewrite HSub, HSub', <- HLe0 in Hr; exists rq rr; now auto.
+ rewrite <- assoc; eapply erasure_equiv, HEq; try reflexivity; [].
clear; intros i; tauto.
Qed.
Qed.*)
Lemma vsFalse m1 m2 :
valid (vs m1 m2 ).
......@@ -478,48 +498,66 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
Local Open Scope pcm_scope.
Local Open Scope bi_scope.
Local Open Scope lang_scope.
Local Existing Instance eqRes.
Global Instance expr_type : Setoid expr := discreteType.
Global Instance expr_metr : metric expr := discreteMetric.
Global Instance expr_cmetr : cmetric expr := discreteCMetric.
Instance LP_isval : LimitPreserving is_value.
Proof.
intros σ σc HC; apply HC.
Qed.
Implicit Types (P Q R : Props) (i : nat) (m : mask) (e : expr) (w : Wld) (φ : value -n> Props) (r : res).
Local Obligation Tactic := intros; eauto with typeclass_instances.
Definition wpFP m (WP : expr -n> (value -n> Props) -n> Props) e φ w n r :=
forall w' k s rf σ (HSw : w w') (HLt : k < n)
(HE : erasure σ m (r · rf) s w' @ S k),
forall w' k s rf rr σ
(HSw : w w') (HLt : k < n) (HR : Some r · Some rf == Some rr)
(HE : erasure σ m rr s w' @ S k),
(forall (HV : is_value e),
exists w'' r' s', w' w'' /\ φ (exist _ e HV) w'' (S k) r'
/\ erasure σ m (r' · rf) s' w'' @ S k) /\
exists w'' r' rr' s', w' w'' /\ φ (exist _ e HV) w'' (S k) r'
/\ Some r' · Some rf == Some rr'
/\ erasure σ m rr' s' w'' @ S k) /\
(forall σ' ei ei' K (HDec : e = K [[ ei ]])
(HStep : prim_step (ei, σ) (ei', σ')),
exists w'' r' s', w' w'' /\ WP (K [[ ei' ]]) φ w'' k r'
/\ erasure σ' m (r' · rf) s' w'' @ k) /\
exists w'' r' rr' s', w' w'' /\ WP (K [[ ei' ]]) φ w'' k r'
/\ Some r' · Some rf == Some rr'
/\ erasure σ' m rr' s' w'' @ k) /\
(forall e' K (HDec : e = K [[ e' ]]),
exists w'' rfk rret s', w' w'' /\ erasure σ m (rfk · rret · rf) s' w'' @ k
/\ WP (K [[ fork_ret ]]) φ w'' k rret
/\ WP e' (umconst ) w'' k rfk).
exists w'' rfk rret rr' s', w' w'' /\ Some rfk · Some rret · Some rf == Some rr'
/\ WP (K [[ fork_ret ]]) φ w'' k rret
/\ WP e' (umconst ) w'' k rfk
/\ erasure σ m rr' s' w'' @ k).
Program Definition wpF m : (expr -n> (value -n> Props) -n> Props) -n> expr -n> (value -n> Props) -n> Props :=
n[(fun WP => n[(fun e => n[(fun φ => m[(fun w => mkUPred (wpFP m WP e φ w) _)])])])].
Next Obligation.
intros n1 n2 r1 r2 HLe [rd EQr] Hp w' k s rf σ HSw HLt HE.
specialize (Hp w' k s (rd · rf) σ); destruct Hp as [HV [HS HF] ];
[assumption | now eauto with arith | rewrite assoc, (comm r1), EQr; assumption |].
intros n1 n2 r1 r2 HLe [rd EQr] Hp w' k s rf rr σ HSw HLt HR HE.
rewrite <- EQr, (comm (Some rd)), <- assoc in HR.
destruct (Some rd · Some rf) as [rf' |] eqn: HRF;
[| now erewrite comm, pcm_op_zero in HR by apply _].
specialize (Hp w' k s rf' rr σ); destruct Hp as [HV [HS HF] ];
[| now eauto with arith | ..]; try assumption; [].
split; [clear HS HF | split; [clear HV HF | clear HV HS] ]; intros.
- specialize (HV HV0); destruct HV as [w'' [r' [s' [HSw' [Hφ HE'] ] ] ] ];
exists w'' (r' · rd) s'; split; [assumption | split; [| rewrite <- assoc; assumption] ].
eapply uni_pred, Hφ; [reflexivity | eexists; rewrite comm; reflexivity].
- specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [s' [HSw' [HWP HE'] ] ] ] ];
exists w'' (r' · rd) s'; split; [assumption | split; [| rewrite <- assoc; assumption] ].
eapply uni_pred, HWP; [reflexivity | eexists; rewrite comm; reflexivity].
- specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [s' [HSw' [HE' [HWR HWF] ] ] ] ] ] ];
exists w'' rfk (rret · rd) s'; split; [assumption | split; [| split] ].
+ rewrite assoc in HE'; rewrite assoc; assumption.
+ eapply uni_pred, HWR; [reflexivity | eexists; rewrite comm; reflexivity].
+ assumption.
- specialize (HV HV0); destruct HV as [w'' [r2' [rr' [s' [HSw' [Hφ [HR' HE'] ] ] ] ] ] ].
rewrite <- HRF, assoc, (comm (Some r2')) in HR'.
destruct (Some rd · Some r2') as [r1' |] eqn: HR1;
[| now erewrite pcm_op_zero in HR' by apply _].
exists w'' r1' rr' s'; split; [assumption | split; [| split; assumption] ].
eapply uni_pred, Hφ; [| eexists; rewrite <- HR1]; reflexivity.
- specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r2' [rr' [s' [HSw' [HWP [HR' HE'] ] ] ] ] ] ].
rewrite <- HRF, assoc, (comm (Some r2')) in HR'.
destruct (Some rd · Some r2') as [r1' |] eqn: HR1;
[| now erewrite pcm_op_zero in HR' by apply _].
exists w'' r1' rr' s'; split; [assumption | split; [| split; assumption] ].
eapply uni_pred, HWP; [| eexists; rewrite <- HR1]; reflexivity.
- specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret2 [rr' [s' [HSw' [HR' [HWR [HWF HE'] ] ] ] ] ] ] ] ].
rewrite <- HRF, assoc, <- (assoc (Some rfk)), (comm (Some rret2)) in HR'.
destruct (Some rd · Some rret2) as [rret1 |] eqn: HR1;
[| now erewrite (comm _ 0), !pcm_op_zero in HR' by apply _].
exists w'' rfk rret1 rr'; exists s'; repeat (split; try assumption); [].
eapply uni_pred, HWR; [| eexists; rewrite <- HR1]; reflexivity.
Qed.
Next Obligation.
intros w1 w2 EQw n r; simpl.
......@@ -533,46 +571,46 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
edestruct (Hp (extend w2' w1)) as [HV [HS HF] ]; try eassumption;
[eapply erasure_dist, HE; [eassumption | now eauto with arith] |].
split; [clear HS HF | split; [clear HV HF | clear HV HS] ]; intros.
+ specialize (HV HV0); destruct HV as [w1'' [r' [s' [HSw'' [Hφ HE'] ] ] ] ].
+ specialize (HV HV0); destruct HV as [w1'' [r' [rr' [s' [HSw'' [Hφ [HR' HE'] ] ] ] ] ] ].
assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
exists (extend w1'' w2') r' s'; split; [assumption |].
split; [| eapply erasure_dist, HE'; [eassumption | now eauto with arith] ].
exists (extend w1'' w2') r' rr' s'; split; [assumption |].
split; [| split; [assumption | eapply erasure_dist, HE'; [eassumption | now eauto with arith] ] ].
eapply (met_morph_nonexp _ _ (φ _)), Hφ; [eassumption | now eauto with arith].
+ specialize (HS _ _ _ _ HDec HStep); destruct HS as [w1'' [r' [s' [HSw'' [HWP HE'] ] ] ] ].
+ specialize (HS _ _ _ _ HDec HStep); destruct HS as [w1'' [r' [rr' [s' [HSw'' [HWP [HR' HE'] ] ] ] ] ] ].
assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
exists (extend w1'' w2') r' s'; split; [assumption |].
split; [| eapply erasure_dist, HE'; [eassumption | now eauto with arith] ].
exists (extend w1'' w2') r' rr' s'; split; [assumption |].
split; [| split; [assumption | eapply erasure_dist, HE'; [eassumption | now eauto with arith] ] ].
eapply (met_morph_nonexp _ _ (WP _ _)), HWP; [eassumption | now eauto with arith].
+ specialize (HF _ _ HDec); destruct HF as [w1'' [rfk [rret [s' [HSw'' [HE' [HWR HWF] ] ] ] ] ] ].
+ specialize (HF _ _ HDec); destruct HF as [w1'' [rfk [rret [rr' [s' [HSw'' [HR' [HWR [HWF HE'] ] ] ] ] ] ] ] ].
assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
exists (extend w1'' w2') rfk rret s'; split; [assumption |].
split; [eapply erasure_dist, HE'; [eassumption | now eauto with arith] |].
split; eapply (met_morph_nonexp _ _ (WP _ _)); try eassumption; now eauto with arith.
exists (extend w1'' w2') rfk rret rr'; exists s'; do 2 (split; [assumption |]).
split; [| split; [| eapply erasure_dist, HE'; [eassumption | now eauto with arith] ] ];
eapply (met_morph_nonexp _ _ (WP _ _)); try eassumption; now eauto with arith.
- assert (EQw' := extend_dist _ _ _ _ EQw HSw); assert (HSw' := extend_sub _ _ _ _ EQw HSw); symmetry in EQw'.
edestruct (Hp (extend w2' w2)) as [HV [HS HF] ]; try eassumption;
[eapply erasure_dist, HE; [eassumption | now eauto with arith] |].
split; [clear HS HF | split; [clear HV HF | clear HV HS] ]; intros.
+ specialize (HV HV0); destruct HV as [w1'' [r' [s' [HSw'' [Hφ HE'] ] ] ] ].
+ specialize (HV HV0); destruct HV as [w1'' [r' [rr' [s' [HSw'' [Hφ [HR' HE'] ] ] ] ] ] ].
assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
exists (extend w1'' w2') r' s'; split; [assumption |].
split; [| eapply erasure_dist, HE'; [eassumption | now eauto with arith] ].
exists (extend w1'' w2') r' rr' s'; split; [assumption |].
split; [| split; [assumption | eapply erasure_dist, HE'; [eassumption | now eauto with arith] ] ].
eapply (met_morph_nonexp _ _ (φ _)), Hφ; [eassumption | now eauto with arith].
+ specialize (HS _ _ _ _ HDec HStep); destruct HS as [w1'' [r' [s' [HSw'' [HWP HE'] ] ] ] ].
+ specialize (HS _ _ _ _ HDec HStep); destruct HS as [w1'' [r' [rr' [s' [HSw'' [HWP [HR' HE'] ] ] ] ] ] ].
assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
exists (extend w1'' w2') r' s'; split; [assumption |].
split; [| eapply erasure_dist, HE'; [eassumption | now eauto with arith] ].
exists (extend w1'' w2') r' rr' s'; split; [assumption |].
split; [| split; [assumption | eapply erasure_dist, HE'; [eassumption | now eauto with arith] ] ].
eapply (met_morph_nonexp _ _ (WP _ _)), HWP; [eassumption | now eauto with arith].
+ specialize (HF _ _ HDec); destruct HF as [w1'' [rfk [rret [s' [HSw'' [HE' [HWR HWF] ] ] ] ] ] ].
+ specialize (HF _ _ HDec); destruct HF as [w1'' [rfk [rret [rr' [s' [HSw'' [HR' [HWR [HWF HE'] ] ] ] ] ] ] ] ].
assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
exists (extend w1'' w2') rfk rret s'; split; [assumption |].
split; [eapply erasure_dist, HE'; [eassumption | now eauto with arith] |].
split; eapply (met_morph_nonexp _ _ (WP _ _)); try eassumption; now eauto with arith.
exists (extend w1'' w2') rfk rret rr'; exists s'; do 2 (split; [assumption |]).
split; [| split; [| eapply erasure_dist, HE'; [eassumption | now eauto with arith] ] ];
eapply (met_morph_nonexp _ _ (WP _ _)); try eassumption; now eauto with arith.
Qed.
Next Obligation.
intros w1 w2 Sw n r; simpl; intros Hp w'; intros; eapply Hp; try eassumption.
......@@ -586,24 +624,24 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
intros φ1 φ2 EQφ w k r HLt; simpl; destruct n as [| n]; [now inversion HLt |].
split; intros Hp w'; intros; edestruct Hp as [HV [HS HF] ]; try eassumption; [|].
- split; [| split]; intros.
+ clear HS HF; specialize (HV HV0); destruct HV as [w'' [r' [s' [HSw' [Hφ HE'] ] ] ] ].
exists w'' r' s'; split; [assumption | split; [| assumption] ].
+ clear HS HF; specialize (HV HV0); destruct HV as [w'' [r' [rr' [s' [HSw' [Hφ [HR' HE'] ] ] ] ] ] ].
exists w'' r' rr' s'; split; [assumption | split; [| split; assumption] ].
apply EQφ, Hφ; now eauto with arith.
+ clear HV HF; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [s' [HSw' [Hφ HE'] ] ] ] ].
exists w'' r' s'; split; [assumption | split; [| assumption] ].
+ clear HV HF; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [rr' [s' [HSw' [Hφ [HR' HE'] ] ] ] ] ] ].
exists w'' r' rr' s'; split; [assumption | split; [| split; assumption] ].
eapply (met_morph_nonexp _ _ (WP _)), Hφ; [symmetry; eassumption | now eauto with arith].
+ clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [s' [HSw' [HE' [HWR HWF] ] ] ] ] ] ].
exists w'' rfk rret s'; repeat (split; try assumption); [].
+ clear HV HS; specialize (