Commit 68cf2dd0 authored by Ralf Jung's avatar Ralf Jung

port BI and iris_core to resource algebras

parent f64e97f0
This diff is collapsed.
Require Import PreoMet.
Require Import PCM.
Require Import RA.
Section CompleteBI.
Context {T : Type}.
......@@ -140,28 +140,30 @@ Section UPredLater.
End UPredLater.
Section UPredBI.
Context Res `{pcmRes : PCM Res}.
Local Open Scope pcm_scope.
Context res `{raRes : RA res}.
Local Open Scope ra_scope.
Local Obligation Tactic := intros; eauto with typeclass_instances.
Definition pres := ra_pos res.
(* Standard interpretations of propositional connectives. *)
Global Program Instance top_up : topBI (UPred Res) := up_cr (const True).
Global Program Instance bot_up : botBI (UPred Res) := up_cr (const False).
Global Program Instance top_up : topBI (UPred pres) := up_cr (const True).
Global Program Instance bot_up : botBI (UPred pres) := up_cr (const False).
Global Program Instance and_up : andBI (UPred Res) :=
Global Program Instance and_up : andBI (UPred pres) :=
fun P Q =>
mkUPred (fun n r => P n r /\ Q n r) _.
Next Obligation.
intros n m r1 r2 HLe HSub; rewrite HSub, HLe; tauto.
Qed.
Global Program Instance or_up : orBI (UPred Res) :=
Global Program Instance or_up : orBI (UPred pres) :=
fun P Q =>
mkUPred (fun n r => P n r \/ Q n r) _.
Next Obligation.
intros n m r1 r2 HLe HSub; rewrite HSub, HLe; tauto.
Qed.
Global Program Instance impl_up : implBI (UPred Res) :=
Global Program Instance impl_up : implBI (UPred pres) :=
fun P Q =>
mkUPred (fun n r => forall m r', m <= n -> r r' -> P m r' -> Q m r') _.
Next Obligation.
......@@ -170,40 +172,44 @@ Section UPredBI.
Qed.
(* BI connectives. *)
Global Program Instance sc_up : scBI (UPred Res) :=
Global Program Instance sc_up : scBI (UPred pres) :=
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, ra_proj r1 · ra_proj r2 == ra_proj r /\ P n r1 /\ Q n r2) _.
Next Obligation.
intros n m r1 r2 HLe [rd HEq] [r11 [r12 [HEq' [HP HQ]]]].
rewrite <- HEq', assoc in HEq; setoid_rewrite HLe.
destruct (Some rd · Some r11) as [r11' |] eqn: HEq'';
[| erewrite pcm_op_zero in HEq by apply _; contradiction].
repeat eexists; [eassumption | | assumption].
eapply uni_pred, HP; [reflexivity |].
exists rd; rewrite HEq''; reflexivity.
assert(VAL: (rd · ra_proj r11) = true).
{ eapply ra_op_pos_valid; eassumption. }
exists (ra_cr_pos VAL) r12.
split; [|split;[|assumption] ].
- simpl. assumption.
- eapply uni_pred, HP; [reflexivity|].
exists rd. reflexivity.
Qed.
Global Program Instance si_up : siBI (UPred Res) :=
Global Program Instance si_up : siBI (UPred pres) :=
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, ra_proj r · ra_proj r' == ra_proj rr -> m <= n -> P m r' -> Q m rr) _.
Next Obligation.
intros n m r1 r2 HLe [r12 HEq] HSI k r rr HEq' HSub HP.
rewrite comm in HEq; rewrite <- HEq, <- assoc in HEq'.
destruct (Some r12 · Some r) as [r' |] eqn: HEq'';
[| erewrite comm, pcm_op_zero in HEq' by apply _; contradiction].
eapply HSI; [eassumption | etransitivity; eassumption |].
eapply uni_pred, HP; [| exists r12; rewrite HEq'']; reflexivity.
assert (VAL: (r12 · ra_proj r) = true).
{ eapply ra_op_pos_valid. erewrite comm. eassumption. }
pose (rc := ra_cr_pos VAL).
eapply HSI with (r':=rc); [| etransitivity; eassumption |].
- simpl. assumption.
- eapply uni_pred, HP; [reflexivity|]. exists r12. reflexivity.
Qed.
(* Quantifiers. *)
Global Program Instance all_up : allBI (UPred Res) :=
Global Program Instance all_up : allBI (UPred pres) :=
fun T eqT mT cmT R =>
mkUPred (fun n r => forall t, R t n r) _.
Next Obligation.
intros n m r1 r2 HLe HSub HR t; rewrite HLe, <- HSub; apply HR.
Qed.
Global Program Instance xist_up : xistBI (UPred Res) :=
Global Program Instance xist_up : xistBI (UPred pres) :=
fun T eqT mT cmT R =>
mkUPred (fun n r => exists t, R t n r) _.
Next Obligation.
......@@ -254,7 +260,7 @@ Section UPredBI.
Global Instance impl_up_dist n : Proper (dist n ==> dist n ==> dist n) impl_up.
Proof.
intros P1 P2 EQP Q1 Q2 EQQ m r HLt; simpl.
split; intros; apply EQQ, H, EQP; now eauto with arith.
split; intros; apply EQQ, H0, EQP; now eauto with arith.
Qed.
Global Instance impl_up_ord : Proper (pord --> pord ++> pord) impl_up.
Proof.
......@@ -287,7 +293,7 @@ Section UPredBI.
Global Instance si_up_dist n : Proper (dist n ==> dist n ==> dist n) si_up.
Proof.
intros P1 P2 EQP Q1 Q2 EQQ m r HLt; simpl.
split; intros; eapply EQQ, H, EQP; now eauto with arith.
split; intros; eapply EQQ, H0, EQP; now eauto with arith.
Qed.
Global Instance si_up_ord : Proper (pord --> pord ++> pord) si_up.
Proof.
......@@ -300,23 +306,23 @@ Section UPredBI.
Existing Instance nonexp_type.
Global Instance all_up_equiv : Proper (equiv (T := V -n> UPred Res) ==> equiv) all.
Global Instance all_up_equiv : Proper (equiv (T := V -n> UPred pres) ==> equiv) all.
Proof.
intros R1 R2 EQR n r; simpl.
setoid_rewrite EQR; tauto.
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 pres) n ==> dist n) all.
Proof.
intros R1 R2 EQR m r HLt; simpl.
split; intros; apply EQR; now auto.
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 pres) ==> equiv) xist.
Proof.
intros R1 R2 EQR n r; simpl.
setoid_rewrite EQR; tauto.
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 pres)n ==> dist n) xist.
Proof.
intros R1 R2 EQR m r HLt; simpl.
split; intros [t HR]; exists t; apply EQR; now auto.
......@@ -324,7 +330,7 @@ Section UPredBI.
End Quantifiers.
Global Program Instance bi_up : ComplBI (UPred Res).
Global Program Instance bi_up : ComplBI (UPred pres).
Next Obligation.
intros n r _; exact I.
Qed.
......@@ -356,30 +362,32 @@ Section UPredBI.
Qed.
Next Obligation.
intros P Q n r; simpl.
setoid_rewrite (comm (Commutative := pcm_op_comm _)) at 1.
setoid_rewrite (comm (Commutative := ra_op_comm _)) at 1.
firstorder.
Qed.
Next Obligation.
intros P Q R n r; split.
- intros [r1 [rr [EQr [HP [r2 [r3 [EQrr [HQ HR]]]]]]]].
rewrite <- EQrr, assoc in EQr.
destruct (Some r1 · Some r2) as [r12 |] eqn: EQr';
[| now erewrite pcm_op_zero in EQr by apply _].
rewrite <- EQrr, assoc in EQr. unfold sc.
assert(VAL: (ra_proj r1 · ra_proj r2) = true).
{ eapply ra_op_pos_valid; eassumption. }
pose (r12 := ra_cr_pos VAL).
exists r12 r3; split; [assumption | split; [| assumption] ].
exists r1 r2; split; [rewrite EQr'; reflexivity | split; assumption].
exists r1 r2; split; [reflexivity | split; assumption].
- intros [rr [r3 [EQr [[r1 [r2 [EQrr [HP HQ]]]] HR]]]].
rewrite <- EQrr, <- assoc in EQr; clear EQrr.
destruct (Some r2 · Some r3) as [r23 |] eqn: EQ23;
[| now erewrite comm, pcm_op_zero in EQr by apply _].
assert(VAL: (ra_proj r2 · ra_proj r3) = true).
{ eapply ra_op_pos_valid. rewrite comm. eassumption. }
pose (r23 := ra_cr_pos VAL).
exists r1 r23; split; [assumption | split; [assumption |] ].
exists r2 r3; split; [rewrite EQ23; reflexivity | split; assumption].
exists r2 r3; split; [reflexivity | split; assumption].
Qed.
Next Obligation.
intros n r; split.
- intros [r1 [r2 [EQr [_ HP]]]].
eapply uni_pred, HP; [| exists r1]; trivial.
- intros HP; exists (pcm_unit _) r; split;
[erewrite pcm_op_unit by apply _; reflexivity |].
eapply uni_pred, HP; [reflexivity|]. exists (ra_proj r1). assumption.
- intros HP. exists (ra_pos_unit (T:=res)) r. split;
[simpl; erewrite ra_op_unit by apply _; reflexivity |].
simpl; unfold const; tauto.
Qed.
Next Obligation.
......@@ -394,7 +402,7 @@ Section UPredBI.
- intros HH u n r HP; apply HH; assumption.
Qed.
Next Obligation.
intros n r HA u; apply H, HA.
intros n r HA u; apply H0, HA.
Qed.
Next Obligation.
split.
......@@ -405,7 +413,7 @@ Section UPredBI.
intros n t [t1 [t2 [EQt [[u HP] HQ]]]]; exists u t1 t2; tauto.
Qed.
Next Obligation.
intros n r [u HA]; exists u; apply H, HA.
intros n r [u HA]; exists u; apply H0, HA.
Qed.
End UPredBI.
......
......@@ -30,7 +30,7 @@ End Definitions.
Notation "1" := (ra_unit _) : ra_scope.
Notation "p · q" := (ra_op _ p q) (at level 40, left associativity) : ra_scope.
Notation "'valid' p" := (ra_valid _ p) (at level 35) : ra_scope.
Notation "'' p" := (ra_valid _ p) (at level 35) : ra_scope.
Delimit Scope ra_scope with ra.
......@@ -44,19 +44,19 @@ Section RAs.
rewrite comm. now eapply ra_op_unit.
Qed.
Lemma ra_op_invalid2 t1 t2: valid t2 = false -> valid (t1 · t2) = false.
Lemma ra_op_invalid2 t1 t2: t2 = false -> (t1 · t2) = false.
Proof.
rewrite comm. now eapply ra_op_invalid.
Qed.
Lemma ra_op_valid t1 t2: valid (t1 · t2) = true -> valid t1 = true.
Lemma ra_op_valid t1 t2: (t1 · t2) = true -> t1 = true.
Proof.
intros Hval.
destruct (valid t1) eqn:Heq; [reflexivity|].
destruct ( t1) eqn:Heq; [reflexivity|].
rewrite <-Hval. symmetry. now eapply ra_op_invalid.
Qed.
Lemma ra_op_valid2 t1 t2: valid (t1 · t2) = true -> valid t2 = true.
Lemma ra_op_valid2 t1 t2: (t1 · t2) = true -> t2 = true.
Proof.
rewrite comm. now eapply ra_op_valid.
Qed.
......@@ -74,8 +74,7 @@ Section Products.
| (s1, t1), (s2, t2) => (s1 · s2, t1 · t2)
end.
Global Instance ra_valid_prod : RA_valid (S * T) :=
fun st => match st with (s, t) =>
valid s && valid t
fun st => match st with (s, t) => s && t
end.
Global Instance ra_prod : RA (S * T).
Proof.
......@@ -99,27 +98,28 @@ Section PositiveCarrier.
Context {T} `{raT : RA T}.
Local Open Scope ra_scope.
Definition ra_pos: Type := { r | valid r = true }.
Definition ra_pos: Type := { r | r = true }.
Coercion ra_proj (t:ra_pos): T := proj1_sig t.
Definition ra_mk_pos t (VAL: valid t = true): ra_pos := exist _ t VAL.
Definition ra_mk_pos t {VAL: t = true}: ra_pos := exist _ t VAL.
Definition ra_cr_pos {t} (VAL: t = true) := ra_mk_pos t (VAL:=VAL).
Program Definition ra_pos_unit: ra_pos := exist _ 1 _.
Next Obligation.
now erewrite ra_valid_unit by apply _.
Qed.
Lemma ra_pos_mult_valid t1 t2 t:
t1 · t2 == ra_proj t -> valid t1 = true.
Lemma ra_op_pos_valid t1 t2 t:
t1 · t2 == ra_proj t -> t1 = true.
Proof.
destruct t as [t Hval]; simpl. intros Heq. rewrite <-Heq in Hval.
eapply ra_op_valid. eassumption.
Qed.
Lemma ra_pos_mult_valid2 t1 t2 t:
t1 · t2 == ra_proj t -> valid t2 = true.
Lemma ra_op_pos_valid2 t1 t2 t:
t1 · t2 == ra_proj t -> t2 = true.
Proof.
rewrite comm. now eapply ra_pos_mult_valid.
rewrite comm. now eapply ra_op_pos_valid.
Qed.
End PositiveCarrier.
......@@ -130,58 +130,62 @@ Section Order.
Context T `{raT : RA T}.
Local Open Scope ra_scope.
Definition ra_ord (t1 t2 : ra_pos T) :=
exists td, (ra_proj td) · (ra_proj t1) == (ra_proj t2).
Definition pra_ord (t1 t2 : ra_pos T) :=
exists td, td · (ra_proj t1) == (ra_proj t2).
Global Program Instance RA_preo : preoType (ra_pos T) | 0 := mkPOType ra_ord.
Global Program Instance pRA_preo : preoType (ra_pos T) | 0 := mkPOType pra_ord.
Next Obligation.
split.
- intros x; exists ra_pos_unit. simpl. erewrite ra_op_unit by apply _; reflexivity.
- intros z yz xyz [y Hyz] [x Hxyz]; unfold ra_ord.
- intros x; exists 1. simpl. erewrite ra_op_unit by apply _; reflexivity.
- intros z yz xyz [y Hyz] [x Hxyz]; unfold pra_ord.
rewrite <- Hyz, assoc in Hxyz; setoid_rewrite <- Hxyz.
assert (VAL:valid (ra_proj x · ra_proj y) = true).
{ now eapply ra_pos_mult_valid in Hxyz. }
exists (ra_mk_pos (ra_proj x · ra_proj y) VAL). reflexivity.
exists (x · y). reflexivity.
Qed.
(* Definition opcm_ord (t1 t2 : option T) :=
exists otd, otd · t1 == t2.
Global Program Instance opcm_preo : preoType (option T) :=
mkPOType opcm_ord.
Global Instance equiv_pord_pra : Proper (equiv ==> equiv ==> equiv) (pord (T := ra_pos T)).
Proof.
intros s1 s2 EQs t1 t2 EQt; split; intros [s HS].
- exists s; rewrite <- EQs, <- EQt; assumption.
- exists s; rewrite EQs, EQt; assumption.
Qed.
Lemma unit_min r : ra_pos_unit r.
Proof.
exists (ra_proj r). simpl.
now erewrite ra_op_unit2 by apply _.
Qed.
Definition ra_ord (t1 t2 : T) :=
exists t, t · t1 == t2.
Global Program Instance ra_preo : preoType T := mkPOType ra_ord.
Next Obligation.
split.
- intros r; exists 1; erewrite pcm_op_unit by apply _; reflexivity.
- intros r; exists 1; erewrite ra_op_unit by apply _; reflexivity.
- intros z yz xyz [y Hyz] [x Hxyz]; exists (x · y).
rewrite <- Hxyz, <- Hyz; symmetry; apply assoc.
Qed.
Global Instance equiv_pord_pcm : Proper (equiv ==> equiv ==> equiv) (pord (T := option T)).
Global Instance equiv_pord_ra : Proper (equiv ==> equiv ==> equiv) (pord (T := T)).
Proof.
intros s1 s2 EQs t1 t2 EQt; split; intros [s HS].
- exists s; rewrite <- EQs, <- EQt; assumption.
- exists s; rewrite EQs, EQt; assumption.
Qed.
Global Instance pcm_op_monic : Proper (pord ==> pord ==> pord) (pcm_op _).
Global Instance ra_op_monic : Proper (pord ++> pord ++> pord) (ra_op _).
Proof.
intros x1 x2 [x EQx] y1 y2 [y EQy]; exists (x · y).
intros x1 x2 [x EQx] y1 y2 [y EQy]. exists (x · y).
rewrite <- assoc, (comm y), <- assoc, assoc, (comm y1), EQx, EQy; reflexivity.
Qed.
Lemma ord_res_optRes r s :
(r ⊑ s) <-> (Some r ⊑ Some s).
(r s) <-> (ra_proj r ra_proj s).
Proof.
split; intros HR.
- destruct HR as [d EQ]; exists (Some d); assumption.
- destruct HR as [[d |] EQ]; [exists d; assumption |].
erewrite pcm_op_zero in EQ by apply _; contradiction.
- destruct HR as [d EQ]. exists d. assumption.
- destruct HR as [d EQ]. exists d. assumption.
Qed.
Lemma unit_min r : pcm_unit _ ⊑ r.
Proof.
exists r; now erewrite comm, pcm_op_unit by apply _.
Qed.*)
End Order.
Section Exclusive.
......
......@@ -2,10 +2,12 @@
domain equations to build a higher-order separation logic *)
Require Import ModuRes.PreoMet ModuRes.MetricRec ModuRes.CBUltInst.
Require Import ModuRes.Finmap ModuRes.Constr.
Require Import ModuRes.PCM ModuRes.UPred.
Require Import ModuRes.RA ModuRes.UPred.
(* This interface keeps some of the details of the solution opaque *)
Module Type WORLD_PROP (Res : PCM_T).
Module Type WORLD_PROP (Res : RA_T).
Definition pres := ra_pos Res.res.
(* PreProp: The solution to the recursive equation. Equipped with a discrete order. *)
Parameter PreProp : cmtyp.
Instance PProp_preo : preoType PreProp := disc_preo PreProp.
......@@ -14,7 +16,7 @@ Module Type WORLD_PROP (Res : PCM_T).
(* Defines Worlds, Propositions *)
Definition Wld := nat -f> PreProp.
Definition Props := Wld -m> UPred Res.res.
Definition Props := Wld -m> UPred pres.
(* Define all the things on Props, so they have names - this shortens the terms later. *)
Instance Props_ty : Setoid Props | 1 := _.
......@@ -32,10 +34,10 @@ End WORLD_PROP.
(* Now we come to the actual implementation *)
Module WorldProp (Res : PCM_T) : WORLD_PROP Res.
Module WorldProp (Res : RA_T) : WORLD_PROP Res.
(** The construction is parametric in the monoid we choose *)
Import Res.
Definition pres := ra_pos Res.res.
(** We need to build a functor that would describe the following
recursive domain equation:
......@@ -51,7 +53,7 @@ Module WorldProp (Res : PCM_T) : WORLD_PROP Res.
Local Instance pcm_disc P `{cmetric P} : pcmType P | 2000 := disc_pcm P.
Definition FProp P `{cmP : cmetric P} :=
(nat -f> P) -m> UPred res.
(nat -f> P) -m> UPred pres.
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