Commit 5517602d authored by Filip Sieczkowski's avatar Filip Sieczkowski

Simplified definitions by taking UPreds over option T, where T is a

carrier of the monoid. This now corresponds exactly to the formulation
of monoids in rose.v
parent ddaf548e
...@@ -12,6 +12,8 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP). ...@@ -12,6 +12,8 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
End R. End R.
Module Import WP := WorldProp R. Module Import WP := WorldProp R.
Definition res := option R.res.
Delimit Scope iris_scope with iris. Delimit Scope iris_scope with iris.
Local Open Scope iris_scope. Local Open Scope iris_scope.
...@@ -35,7 +37,7 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP). ...@@ -35,7 +37,7 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
Local Obligation Tactic := intros; resp_set || eauto with typeclass_instances. Local Obligation Tactic := intros; resp_set || eauto with typeclass_instances.
Program Definition box : Props -n> Props := Program Definition box : Props -n> Props :=
n[(fun p => m[(fun w => mkUPred (fun n r => p w n (pcm_unit _)) _)])]. n[(fun p => m[(fun w => mkUPred (fun n r => p w n 1%pcm) _)])].
Next Obligation. Next Obligation.
intros n m r s HLe _ Hp; rewrite HLe; assumption. intros n m r s HLe _ Hp; rewrite HLe; assumption.
Qed. Qed.
...@@ -58,7 +60,7 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP). ...@@ -58,7 +60,7 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
Section IntEq. Section IntEq.
Context {T} `{mT : metric T}. Context {T} `{mT : metric T}.
Program Definition intEqP (t1 t2 : T) : UPred R.res := Program Definition intEqP (t1 t2 : T) : UPred res :=
mkUPred (fun n r => t1 = S n = t2) _. mkUPred (fun n r => t1 = S n = t2) _.
Next Obligation. Next Obligation.
intros n1 n2 _ _ HLe _; apply mono_dist; now auto with arith. intros n1 n2 _ _ HLe _; apply mono_dist; now auto with arith.
...@@ -88,8 +90,10 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP). ...@@ -88,8 +90,10 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
Notation "t1 '===' t2" := (intEq t1 t2) (at level 70) : iris_scope. Notation "t1 '===' t2" := (intEq t1 t2) (at level 70) : iris_scope.
Section Invariants.
(** Invariants **) (** Invariants **)
Definition invP (i : nat) (p : Props) (w : Wld) : UPred R.res := Definition invP (i : nat) (p : Props) (w : Wld) : UPred res :=
intEqP (w i) (Some (ı' p)). intEqP (w i) (Some (ı' p)).
Program Definition inv i : Props -n> Props := Program Definition inv i : Props -n> Props :=
n[(fun p => m[(invP i p)])]. n[(fun p => m[(invP i p)])].
...@@ -120,17 +124,24 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP). ...@@ -120,17 +124,24 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
apply dist_mono, (met_morph_nonexp _ _ ı'), EQp. apply dist_mono, (met_morph_nonexp _ _ ı'), EQp.
Qed. Qed.
End Invariants.
(** Ownership **) (** Ownership **)
Definition own (r : R.res) : Props := Definition own (r : res) : Props :=
pcmconst (up_cr (pord r)). 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 **) (** Physical part **)
Definition ownP (r : RP.res) : Props := Definition ownP (r : option RP.res) : Props :=
own (r, pcm_unit _). own (injFst r).
(** Logical part **) (** Logical part **)
Definition ownL (r : RL.res) : Props := Definition ownL (r : option RL.res) : Props :=
own (pcm_unit _, r). own (injSnd r).
Notation "□ p" := (box p) (at level 30, right associativity) : iris_scope. Notation "□ p" := (box p) (at level 30, right associativity) : iris_scope.
Notation "⊤" := (top : Props) : iris_scope. Notation "⊤" := (top : Props) : iris_scope.
...@@ -151,9 +162,9 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP). ...@@ -151,9 +162,9 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
Local Open Scope pcm_scope. Local Open Scope pcm_scope.
(* XXX: logical state omitted, since it looks weird. Also, later over the whole deal. *) (* XXX: logical state omitted, since it looks weird. Also, later over the whole deal. *)
Program Definition erasure (σ : state) (m : mask) (r s : R.res) (w : Wld) : UPred () := Program Definition erasure (σ : state) (m : mask) (r s : res) (w : Wld) : UPred () :=
(mkUPred (fun n _ => (mkUPred (fun n _ =>
erase_state (option_map fst (Some r · Some s)) σ erase_state (option_map fst (r · s)) σ
/\ forall i π, m i -> w i == Some π -> (ı π) w n s) _). /\ forall i π, m i -> w i == Some π -> (ı π) w n s) _).
Next Obligation. Next Obligation.
intros n1 n2 _ _ HLe _ [HES HRS]; split; [assumption | clear HES; intros]. intros n1 n2 _ _ HLe _ [HES HRS]; split; [assumption | clear HES; intros].
...@@ -165,9 +176,9 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP). ...@@ -165,9 +176,9 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
intros w1 w2 EQw [| n] []; [reflexivity |]. intros w1 w2 EQw [| n] []; [reflexivity |].
split; intros [HES HRS]; (split; [tauto | clear HES; intros ? ? HM HLu]). split; intros [HES HRS]; (split; [tauto | clear HES; intros ? ? HM HLu]).
- rewrite <- EQw; eapply HRS; [eassumption |]. - rewrite <- EQw; eapply HRS; [eassumption |].
change (w1 i == Some π); rewrite EQw; assumption. rewrite EQw; assumption.
- rewrite EQw; eapply HRS; [eassumption |]. - rewrite EQw; eapply HRS; [eassumption |].
change (w2 i == Some π); rewrite <- EQw; assumption. rewrite <- EQw; assumption.
Qed. Qed.
Global Instance erasure_dist n σ m r s : Proper (dist n ==> dist n) (erasure σ m r s). Global Instance erasure_dist n σ m r s : Proper (dist n ==> dist n) (erasure σ m r s).
...@@ -194,30 +205,22 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP). ...@@ -194,30 +205,22 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
Local Open Scope mask_scope. Local Open Scope mask_scope.
Local Open Scope pcm_scope. Local Open Scope pcm_scope.
Local Obligation Tactic := intros. Local Obligation Tactic := intros.
Local Instance eqRes : Setoid res := discreteType.
Program Definition preVS (m1 m2 : mask) (p : Props) (w : Wld) : UPred R.res :=
mkUPred (fun n r => forall w1 s rf rc mf σ k (HSub : w w1) (HLe : k <= n) Program Definition preVS (m1 m2 : mask) (p : Props) (w : Wld) : UPred res :=
(HGt : k > 0) (HR : Some rc = Some r · Some rf) mkUPred (fun n r => forall w1 s rf mf σ k (HSub : w w1) (HLe : k <= n)
(HE : erasure σ (m1 mf) rc s w1 @ k) (HD : mf # m1 m2), (HGt : k > 0) (HD : mf # m1 m2)
exists w2 rc' r' s', w1 w2 /\ p w2 k r' /\ (HE : erasure σ (m1 mf) (r · rf) s w1 @ k),
Some rc' = Some r' · Some rf /\ exists w2 r' s', w1 w2 /\ p w2 k r' /\
erasure σ (m2 mf) rc' s' w2 @ k) _. erasure σ (m2 mf) (r' · rf) s' w2 @ k) _.
Next Obligation. Next Obligation.
intros n1 n2 r1 r2 HLe HSub HP; intros. intros n1 n2 r1 r2 HLe [rd HR] HP; intros.
destruct HSub as [ [rd |] HSub]; [| erewrite pcm_op_zero in HSub by eauto with typeclass_instances; discriminate]. destruct (HP w1 s (rd · rf) mf σ k) as [w2 [r1' [s' [HW [HP' HE'] ] ] ] ]; try assumption; [| |].
rewrite (comm (Commutative := pcm_op_comm _)) in HSub; rewrite <- HSub in HR. - etransitivity; eassumption.
rewrite <- (assoc (Associative := pcm_op_assoc _)) in HR. - rewrite assoc, (comm r1), HR; assumption.
destruct (Some rd · Some rf) as [rf' |] eqn: HR'; - exists w2 (rd · r1') s'; split; [assumption | split].
[| erewrite (comm (Commutative := pcm_op_comm _)), pcm_op_zero in HR by apply _; discriminate]. + eapply uni_pred, HP'; [| eexists]; reflexivity.
edestruct (HP w1 s rf' rc mf σ k) as [w2 [rc' [r1' [s' HH] ] ] ]; + rewrite (comm rd), <- assoc; assumption.
try eassumption; [etransitivity; eassumption |]; clear - HR' HH.
destruct HH as [HW [HP [HR HE] ] ]; rewrite <- HR' in HR.
rewrite (assoc (Associative := pcm_op_assoc _)) in HR.
destruct (Some r1' · Some rd) as [r2' |] eqn: HR'';
[| erewrite pcm_op_zero in HR by apply _; discriminate].
exists w2 rc' r2' s'; intuition; [].
eapply uni_pred, HP; [reflexivity |].
exists (Some rd); rewrite (comm (Commutative := pcm_op_comm _)); assumption.
Qed. Qed.
Program Definition pvs (m1 m2 : mask) : Props -n> Props := Program Definition pvs (m1 m2 : mask) : Props -n> Props :=
...@@ -232,20 +235,21 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP). ...@@ -232,20 +235,21 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
Next Obligation. Next Obligation.
intros w1 w2 EQw n' r HLt; destruct n as [| n]; [now inversion HLt |]; split; intros HP w2'; intros. 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). - symmetry in EQw; assert (HDE := extend_dist _ _ _ _ EQw HSub).
assert (HSE := extend_sub _ _ _ _ EQw HSub); specialize (HP (extend w2' w1)). assert (HSE := extend_sub _ _ _ _ EQw HSub); specialize (HP (extend w2' w1)).
edestruct HP as [w1'' [rc' [r' [s' [HW HH] ] ] ] ]; try eassumption; clear HP; [ | ]. edestruct HP as [w1'' [r' [s' [HW HH] ] ] ]; try eassumption; clear HP; [ | ].
+ eapply erasure_dist, HE; [symmetry; eassumption | now eauto with arith]. + eapply erasure_dist, HE; [symmetry; eassumption | now eauto with arith].
+ symmetry in HDE; assert (HDE' := extend_dist _ _ _ _ HDE HW). + symmetry in HDE; assert (HDE' := extend_dist _ _ _ _ HDE HW).
assert (HSE' := extend_sub _ _ _ _ HDE HW); destruct HH as [HP [HR' HE'] ]; assert (HSE' := extend_sub _ _ _ _ HDE HW); destruct HH as [HP HE'];
exists (extend w1'' w2') rc' r' s'; repeat split; [assumption | | assumption |]. exists (extend w1'' w2') r' s'; repeat split; [assumption | |].
* eapply (met_morph_nonexp _ _ p), HP ; [symmetry; eassumption | now eauto with arith]. * eapply (met_morph_nonexp _ _ p), HP ; [symmetry; eassumption | now eauto with arith].
* eapply erasure_dist, HE'; [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)). - assert (HDE := extend_dist _ _ _ _ EQw HSub); assert (HSE := extend_sub _ _ _ _ EQw HSub); specialize (HP (extend w2' w2)).
edestruct HP as [w1'' [rc' [r' [s' [HW HH] ] ] ] ]; try eassumption; clear HP; [ | ]. edestruct HP as [w1'' [r' [s' [HW HH] ] ] ]; try eassumption; clear HP; [ | ].
+ eapply erasure_dist, HE; [symmetry; eassumption | now eauto with arith]. + eapply erasure_dist, HE; [symmetry; eassumption | now eauto with arith].
+ symmetry in HDE; assert (HDE' := extend_dist _ _ _ _ HDE HW). + symmetry in HDE; assert (HDE' := extend_dist _ _ _ _ HDE HW).
assert (HSE' := extend_sub _ _ _ _ HDE HW); destruct HH as [HP [HR' HE'] ]; assert (HSE' := extend_sub _ _ _ _ HDE HW); destruct HH as [HP HE'];
exists (extend w1'' w2') rc' r' s'; repeat split; [assumption | | assumption |]. exists (extend w1'' w2') r' s'; repeat split; [assumption | |].
* eapply (met_morph_nonexp _ _ p), HP ; [symmetry; eassumption | now eauto with arith]. * eapply (met_morph_nonexp _ _ p), HP ; [symmetry; eassumption | now eauto with arith].
* eapply erasure_dist, HE'; [symmetry; eassumption | now eauto with arith]. * eapply erasure_dist, HE'; [symmetry; eassumption | now eauto with arith].
Qed. Qed.
...@@ -260,10 +264,10 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP). ...@@ -260,10 +264,10 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
Qed. Qed.
Next Obligation. Next Obligation.
intros p1 p2 EQp w n' r HLt; split; intros HP w1; intros. intros p1 p2 EQp w n' r HLt; split; intros HP w1; intros.
- edestruct HP as [w2 [rc' [r' [s' [HW [HP' [HR' HE'] ] ] ] ] ] ]; try eassumption; []. - edestruct HP as [w2 [r' [s' [HW [HP' HE'] ] ] ] ]; try eassumption; [].
clear HP; repeat eexists; try eassumption; []. clear HP; repeat eexists; try eassumption; [].
apply EQp; [now eauto with arith | assumption]. apply EQp; [now eauto with arith | assumption].
- edestruct HP as [w2 [rc' [r' [s' [HW [HP' [HR' HE'] ] ] ] ] ] ]; try eassumption; []. - edestruct HP as [w2 [r' [s' [HW [HP' HE'] ] ] ] ]; try eassumption; [].
clear HP; repeat eexists; try eassumption; []. clear HP; repeat eexists; try eassumption; [].
apply EQp; [now eauto with arith | assumption]. apply EQp; [now eauto with arith | assumption].
Qed. Qed.
......
...@@ -143,26 +143,27 @@ Section UPredBI. ...@@ -143,26 +143,27 @@ Section UPredBI.
Context Res `{pcmRes : PCM Res}. Context Res `{pcmRes : PCM Res}.
Local Open Scope pcm_scope. Local Open Scope pcm_scope.
Local Obligation Tactic := intros; eauto with typeclass_instances. Local Obligation Tactic := intros; eauto with typeclass_instances.
Local Instance eqRes : Setoid Res := discreteType. Local Existing Instance eqT.
Definition oRes := option Res.
(* Standard interpretations of propositional connectives. *) (* Standard interpretations of propositional connectives. *)
Global Program Instance top_up : topBI (UPred Res) := up_cr (const True). Global Program Instance top_up : topBI (UPred oRes) := up_cr (const True).
Global Program Instance bot_up : botBI (UPred Res) := up_cr (const False). Global Program Instance bot_up : botBI (UPred oRes) := up_cr (const False).
Global Program Instance and_up : andBI (UPred Res) := Global Program Instance and_up : andBI (UPred oRes) :=
fun P Q => fun P Q =>
mkUPred (fun n r => P n r /\ Q n r) _. mkUPred (fun n r => P n r /\ Q n r) _.
Next Obligation. Next Obligation.
intros n m r1 r2 HLe HSub; rewrite HSub, HLe; tauto. intros n m r1 r2 HLe HSub; rewrite HSub, HLe; tauto.
Qed. Qed.
Global Program Instance or_up : orBI (UPred Res) := Global Program Instance or_up : orBI (UPred oRes) :=
fun P Q => fun P Q =>
mkUPred (fun n r => P n r \/ Q n r) _. mkUPred (fun n r => P n r \/ Q n r) _.
Next Obligation. Next Obligation.
intros n m r1 r2 HLe HSub; rewrite HSub, HLe; tauto. intros n m r1 r2 HLe HSub; rewrite HSub, HLe; tauto.
Qed. Qed.
Global Program Instance impl_up : implBI (UPred Res) := Global Program Instance impl_up : implBI (UPred oRes) :=
fun P Q => fun P Q =>
mkUPred (fun n r => forall m r', m <= n -> r r' -> P m r' -> Q m r') _. mkUPred (fun n r => forall m r', m <= n -> r r' -> P m r' -> Q m r') _.
Next Obligation. Next Obligation.
...@@ -171,53 +172,45 @@ Section UPredBI. ...@@ -171,53 +172,45 @@ Section UPredBI.
Qed. Qed.
(* BI connectives. *) (* BI connectives. *)
Global Program Instance sc_up : scBI (UPred Res) := Global Program Instance sc_up : scBI (UPred oRes) :=
fun P Q => fun P Q =>
mkUPred (fun n r => exists r1 r2, Some r1 · Some r2 = Some r /\ P n r1 /\ Q n r2) _. mkUPred (fun n r => exists r1 r2, r1 · r2 = r /\ P n r1 /\ Q n r2) _.
Next Obligation. Next Obligation.
intros n m r1 r2 HLe [r3 HEq] [r11 [r12 [HEq' [HP HQ]]]]. intros n m r1 r2 HLe [rd HEq] [r11 [r12 [HEq' [HP HQ]]]].
assert (PA := pcm_op_assoc Res r3 (Some r11) (Some r12)); simpl in PA. rewrite <- HEq', assoc in HEq; setoid_rewrite HLe.
erewrite <- HEq', (assoc (Associative := pcm_op_assoc _)) in HEq. repeat eexists; [eassumption | | assumption].
destruct (r3 · Some r11) as [r311 |] eqn: EQ; eapply uni_pred, HP; [| exists rd]; reflexivity.
[| erewrite pcm_op_zero in HEq by eassumption; discriminate].
exists r311 r12; rewrite HLe.
split; [assumption |].
assert (HS : r11 r311) by (eexists; eassumption).
rewrite <- HS; tauto.
Qed. Qed.
Global Program Instance si_up : siBI (UPred Res) := Global Program Instance si_up : siBI (UPred oRes) :=
fun P Q => fun P Q =>
mkUPred (fun n r => forall m r' rr, Some r · Some r' = Some rr -> m <= n -> P m r' -> Q m rr) _. mkUPred (fun n r => forall m r' rr, r · r' = rr -> m <= n -> P m r' -> Q m rr) _.
Next Obligation. Next Obligation.
intros n m r1 r2 HLe [[r12 |] HEq] HSI k r rr HEq' HSub HP; intros n m r1 r2 HLe [r12 HEq] HSI k r rr HEq' HSub HP.
[| erewrite pcm_op_zero in HEq by eassumption; discriminate]. rewrite comm in HEq; rewrite <- HEq, <- assoc in HEq'.
rewrite (comm (Commutative := pcm_op_comm _)) in HEq. eapply HSI; [| etransitivity |]; try eassumption; [].
rewrite <- HEq, <- (assoc (Associative := pcm_op_assoc _)) in HEq'. eapply uni_pred, HP; [| exists r12]; reflexivity.
destruct (Some r12 · Some r) as [r12r |] eqn: HEq'';
[| erewrite (comm (Commutative := pcm_op_comm _)), pcm_op_zero in HEq' by eassumption; discriminate].
eapply HSI; [eassumption | etransitivity; eassumption |]; [].
assert (HS : r r12r) by (eexists; eassumption).
rewrite <- HS; assumption.
Qed. Qed.
(* Quantifiers. *) (* Quantifiers. *)
Global Program Instance all_up : allBI (UPred Res) := Global Program Instance all_up : allBI (UPred oRes) :=
fun T eqT mT cmT R => fun T eqT mT cmT R =>
mkUPred (fun n r => forall t, R t n r) _. mkUPred (fun n r => forall t, R t n r) _.
Next Obligation. Next Obligation.
intros n m r1 r2 HLe HSub HR t; rewrite HLe, <- HSub; apply HR. intros n m r1 r2 HLe HSub HR t; rewrite HLe, <- HSub; apply HR.
Qed. Qed.
Global Program Instance xist_up : xistBI (UPred Res) := Global Program Instance xist_up : xistBI (UPred oRes) :=
fun T eqT mT cmT R => fun T eqT mT cmT R =>
mkUPred (fun n r => exists t, R t n r) _. mkUPred (fun n r => exists t, R t n r) _.
Next Obligation. Next Obligation.
intros n m r1 r2 HLe HSub [t HR]; exists t; rewrite HLe, <- HSub; apply HR. intros n m r1 r2 HLe HSub [t HR]; exists t; rewrite HLe, <- HSub; apply HR.
Qed. Qed.
(* All of the above preserve all the props it should. *) (* For some reason tc inference gets confused otherwise *)
Existing Instance up_type.
(* All of the above preserve all the props it should. *)
Global Instance and_up_equiv : Proper (equiv ==> equiv ==> equiv) and_up. Global Instance and_up_equiv : Proper (equiv ==> equiv ==> equiv) and_up.
Proof. Proof.
intros P1 P2 EQP Q1 Q2 EQQ n r; simpl. intros P1 P2 EQP Q1 Q2 EQQ n r; simpl.
...@@ -302,23 +295,25 @@ Section UPredBI. ...@@ -302,23 +295,25 @@ Section UPredBI.
Section Quantifiers. Section Quantifiers.
Context V `{pU : cmetric V}. Context V `{pU : cmetric V}.
Global Instance all_up_equiv : Proper (equiv (T := V -n> UPred Res) ==> equiv) all. Existing Instance nonexp_type.
Global Instance all_up_equiv : Proper (equiv (T := V -n> UPred oRes) ==> equiv) all.
Proof. Proof.
intros R1 R2 EQR n r; simpl. intros R1 R2 EQR n r; simpl.
setoid_rewrite EQR; tauto. setoid_rewrite EQR; tauto.
Qed. Qed.
Global Instance all_up_dist n : Proper (dist (T := V -n> UPred Res) n ==> dist n) all. Global Instance all_up_dist n : Proper (dist (T := V -n> UPred oRes) n ==> dist n) all.
Proof. Proof.
intros R1 R2 EQR m r HLt; simpl. intros R1 R2 EQR m r HLt; simpl.
split; intros; apply EQR; now auto. split; intros; apply EQR; now auto.
Qed. Qed.
Global Instance xist_up_equiv : Proper (equiv (T := V -n> UPred Res) ==> equiv) xist. Global Instance xist_up_equiv : Proper (equiv (T := V -n> UPred oRes) ==> equiv) xist.
Proof. Proof.
intros R1 R2 EQR n r; simpl. intros R1 R2 EQR n r; simpl.
setoid_rewrite EQR; tauto. setoid_rewrite EQR; tauto.
Qed. Qed.
Global Instance xist_up_dist n : Proper (dist (T := V -n> UPred Res)n ==> dist n) xist. Global Instance xist_up_dist n : Proper (dist (T := V -n> UPred oRes)n ==> dist n) xist.
Proof. Proof.
intros R1 R2 EQR m r HLt; simpl. intros R1 R2 EQR m r HLt; simpl.
split; intros [t HR]; exists t; apply EQR; now auto. split; intros [t HR]; exists t; apply EQR; now auto.
...@@ -326,7 +321,7 @@ Section UPredBI. ...@@ -326,7 +321,7 @@ Section UPredBI.
End Quantifiers. End Quantifiers.
Global Program Instance bi_up : ComplBI (UPred Res). Global Program Instance bi_up : ComplBI (UPred oRes).
Next Obligation. Next Obligation.
intros n r _; exact I. intros n r _; exact I.
Qed. Qed.
...@@ -364,24 +359,19 @@ Section UPredBI. ...@@ -364,24 +359,19 @@ Section UPredBI.
Next Obligation. Next Obligation.
intros P Q R n r; simpl; split. intros P Q R n r; simpl; split.
- intros [r1 [rr [EQr [HP [r2 [r3 [EQrr [HQ HR]]]]]]]]. - intros [r1 [rr [EQr [HP [r2 [r3 [EQrr [HQ HR]]]]]]]].
rewrite <- EQrr, (assoc (Associative := pcm_op_assoc _)) in EQr. rewrite <- EQrr, assoc in EQr.
destruct (Some r1 · Some r2) as [r12 |] eqn: EQr12; exists (r1 · r2) r3; split; [assumption | split; [| assumption] ].
[| erewrite pcm_op_zero in EQr by eassumption; discriminate]. exists r1 r2; tauto.
exists r12 r3; split; [assumption |].
split; [exists r1 r2; split; [assumption |] |]; tauto.
- intros [rr [r3 [EQr [[r1 [r2 [EQrr [HP HQ]]]] HR]]]]. - intros [rr [r3 [EQr [[r1 [r2 [EQrr [HP HQ]]]] HR]]]].
rewrite <- EQrr, <- (assoc (Associative := pcm_op_assoc _)) in EQr. rewrite <- EQrr, <- assoc in EQr.
destruct (Some r2 · Some r3) as [r23 |] eqn: EQr23; exists r1 (r2 · r3); split; [assumption | split; [assumption |] ].
[| erewrite (comm (Commutative := pcm_op_comm _)), pcm_op_zero in EQr by eassumption; discriminate]. exists r2 r3; tauto.
exists r1 r23; split; [assumption |].
split; [| exists r2; exists r3; split; [assumption |]]; tauto.
Qed. Qed.
Next Obligation. Next Obligation.
intros n r; simpl; split. intros n r; simpl; split.
- intros [r1 [r2 [EQr [_ HP]]]]. - intros [r1 [r2 [EQr [_ HP]]]].
assert (HT : r2 r) by (eexists; apply EQr). eapply uni_pred, HP; [| exists r1]; trivial.
rewrite <- HT; assumption. - intros HP; exists 1%pcm r; unfold const; intuition eauto using pcm_op_unit.
- intros HP; exists (pcm_unit _) r; unfold const; intuition eauto using pcm_op_unit.
Qed. Qed.
Next Obligation. Next Obligation.
split; intros HH n r. split; intros HH n r.
......
...@@ -89,10 +89,10 @@ Section Order. ...@@ -89,10 +89,10 @@ Section Order.
Local Open Scope pcm_scope. Local Open Scope pcm_scope.
Local Existing Instance eqT. Local Existing Instance eqT.
Definition pcm_ord (t1 t2 : T) := Definition pcm_ord (t1 t2 : option T) :=
exists ot, ot · Some t1 = Some t2. exists td, td · t1 = t2.
Global Program Instance PCM_preo : preoType T | 0 := mkPOType pcm_ord. Global Program Instance PCM_preo {pcmT : PCM T} : preoType (option T) | 0 := mkPOType pcm_ord.
Next Obligation. Next Obligation.
split. split.
- intros x; exists 1; eapply pcm_op_unit; assumption. - intros x; exists 1; eapply pcm_op_unit; assumption.
...@@ -100,23 +100,11 @@ Section Order. ...@@ -100,23 +100,11 @@ Section Order.
rewrite <- assoc; congruence. rewrite <- assoc; congruence.
Qed. Qed.
Local Existing Instance option_preo_top.
Global Instance prod_ord : Proper (pord ==> pord ==> pord) (pcm_op _). Global Instance prod_ord : Proper (pord ==> pord ==> pord) (pcm_op _).
Proof. Proof.
intros x1 x2 EQx y1 y2 EQy. intros x1 x2 [xd EQx] y1 y2 [yd EQy].
destruct x2 as [x2 |]; [| erewrite pcm_op_zero by eassumption; exact I]. exists (xd · yd).
destruct x1 as [x1 |]; [| contradiction]; destruct EQx as [x EQx]. rewrite <- assoc, (comm yd), <- assoc, assoc, (comm y1); congruence.
destruct y2 as [y2 |]; [| erewrite (comm (Some x2)), pcm_op_zero by eassumption; exact I].
destruct y1 as [y1 |]; [| contradiction]; destruct EQy as [y EQy].
destruct (Some x2 · Some y2) as [xy2 |] eqn: EQxy2; [| exact I].
destruct (Some x1 · Some y1) as [xy1 |] eqn: EQxy1.
- exists (x · y); rewrite <- EQxy1.
rewrite <- assoc, (comm y), <- assoc, assoc, (comm (Some y1)); congruence.
- rewrite <- EQx, <- EQy in EQxy2.
rewrite <- assoc, (assoc (Some x1)), (comm (Some x1)), <- assoc in EQxy2.
erewrite EQxy1, (comm y), comm, !pcm_op_zero in EQxy2 by eassumption.
discriminate.
Qed. Qed.
End Order. End Order.
......
...@@ -23,7 +23,7 @@ Module WorldProp (Res : PCM_T). ...@@ -23,7 +23,7 @@ Module WorldProp (Res : PCM_T).
Local Instance pcm_disc P `{cmetric P} : pcmType P | 2000 := disc_pcm P. Local Instance pcm_disc P `{cmetric P} : pcmType P | 2000 := disc_pcm P.
Definition FProp P `{cmP : cmetric P} := Definition FProp P `{cmP : cmetric P} :=
(nat -f> P) -m> UPred res. (nat -f> P) -m> UPred (option res).
Context {U V} `{cmU : cmetric U} `{cmV : cmetric V}. Context {U V} `{cmU : cmetric U} `{cmV : cmetric V}.
......
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