Commit cfa1ef3b authored by Ralf Jung's avatar Ralf Jung

introduce "CMRAExt", and extension property on CMRAs. We will need it to show...

introduce "CMRAExt", and extension property on CMRAs. We will need it to show that later commutes with star. For now, just assume it holds.
parent d1e66633
......@@ -74,6 +74,12 @@ Module Type IRIS_CORE (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
Instance vPred_metr : metric vPred := _.
Instance vPred_cmetr : cmetric vPred := _.
(* FIXME TODO RJ: This should hold. But the construction is not entirely trivial. And of course it should not be proven here. *)
Local Instance Wld_Ext: CMRAExt Wld.
Proof.
admit.
Qed.
(** The final thing we'd like to check is that the space of
propositions does indeed form a complete BI algebra.
......@@ -286,6 +292,41 @@ Module Type IRIS_CORE (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
- move=>wf /= m Hle HP. apply (H wf (S m)); assumption || omega.
Qed.
Lemma later_top P:
== .
Proof.
intros w [|n]; split; simpl; tauto.
Qed.
Lemma later_disj P Q :
(P Q) == P Q.
Proof.
intros w [|n]; split; simpl; tauto.
Qed.
Lemma later_conj P Q :
(P Q) == P Q.
Proof.
intros w [|n]; split; simpl; tauto.
Qed.
Lemma later_star P Q:
(P * Q) == P * Q.
Proof.
intros w n; split; (destruct n; first tauto).
- destruct n.
{ move=>_. exists (1 w, w). simpl.
split; last (split; exact:bpred).
now rewrite ra_op_unit. }
move=>[[w1 w2] [/= Heq [HP HQ]]].
edestruct Wld_Ext as [w'1 [w'2 [Heq' [Hdist1 Hdist2]]]]; first eexact Heq; first reflexivity.
exists (w'1, w'2). split; first now rewrite Heq'. simpl in *.
split; (eapply propsNE; last eassumption); assumption.
- move=>[[w1 w2] [Heq [HP HQ]]]. destruct n; first exact I.
exists (w1, w2). simpl in *. split; last tauto.
now apply dist_mono.
Qed.
Lemma strong_loeb P: (P P) P.
Proof.
transitivity ( (P P)).
......@@ -354,7 +395,7 @@ Module Type IRIS_CORE (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
exists w. now rewrite comm ra_op_unit.
Qed.
Lemma box_top : == .
Lemma box_top : == .
Proof.
now auto.
Qed.
......@@ -430,15 +471,7 @@ Module Type IRIS_CORE (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
Context {T} `{cT : cmetric T}.
Context (φ : T -n> Props).
Program Definition box_all_lhs : Props := t, □φ t.
Next Obligation.
move=> t t' HEq w k HLt. simpl.
split.
- apply spredNE. eapply mono_dist; last by rewrite HEq. omega.
- apply spredNE. eapply mono_dist; last by rewrite HEq. omega.
Qed.
Lemma box_all : all φ == box_all_lhs.
Lemma box_all : all φ == all (box <M< φ).
Proof. done. Qed.
End BoxAll.
End NecessitationProps.
......
......@@ -247,6 +247,35 @@ Section ComplBIProps.
move=>f1 f2 Hf. apply pord_antisym; eapply all_pord; rewrite Hf; reflexivity.
Qed.
Lemma all_and U `{cmU : cmetric U} : (* the converse does not hold for empty U *)
forall (P : U -n> B) Q, (all P) Q all (lift_bin and P (umconst Q)).
Proof.
move=>P Q.
apply all_R=>u. apply and_impl. apply (all_L u). apply and_impl. reflexivity.
Qed.
Lemma all_sc U `{cmU : cmetric U} :
forall (P : U -n> B) Q, (all P) * Q all (lift_bin sc P (umconst Q)).
Proof.
move=>P Q. apply all_R=>u. apply sc_si.
apply (all_L u). apply sc_si. reflexivity.
Qed.
Lemma all_sc_r U `{cmU : cmetric U} :
forall (P : U -n> B) Q, Q * (all P) all (lift_bin sc (umconst Q) P).
Proof.
move=>P Q. rewrite (comm Q). etransitivity; first eapply all_sc.
eapply all_pord. move=>u. simpl morph. rewrite comm. reflexivity.
Qed.
Lemma all_and_r U `{cmU : cmetric U} :
forall (P : U -n> B) Q, Q (all P) all (lift_bin and (umconst Q) P).
Proof.
move=>P Q. rewrite (comm Q). etransitivity; first eapply all_and.
eapply all_pord. move=>u. simpl morph. rewrite comm. reflexivity.
Qed.
Lemma xist_R {U} `{cmU : cmetric U} u P (Q: U -n> B):
P Q u -> P xist Q.
Proof.
......
......@@ -56,6 +56,14 @@ Section CMRAProps.
End CMRAProps.
Section CMRAExt.
Context (T: Type).
Class CMRAExt `{cmraT: CMRA T}: Prop :=
cmra_extend: forall n (t1 t11 t12 t2: T) (EQt: t1 = n = t2) (EQt1: t1 == t11 · t12),
exists t21 t22, t2 == t21 · t22 /\ (t11, t12) = n = (t21, t22).
End CMRAExt.
Section DiscreteCMRA.
Context {T: Type} `{raT: RA T}.
Existing Instance discreteMetric.
......@@ -83,6 +91,15 @@ Section DiscreteCMRA.
- move=>t1 t2 n. destruct n; first reflexivity.
exact: ra_op_valid.
Qed.
Instance discreteCMRAExt : CMRAExt T.
Proof.
move=>n; intros. destruct n.
{ exists (1 t2) t2. split; last exact:dist_bound.
now rewrite ra_op_unit. }
exists t11 t12. split; last reflexivity. rewrite /dist /= in EQt.
rewrite -EQt EQt1. reflexivity.
Qed.
End DiscreteCMRA.
(* Pairs work as CMRA *)
......
......@@ -157,7 +157,7 @@ Section MonotoneProducts.
intros [a1 b1] [a2 b2] [Ha Hb]; assumption.
Qed.
Global Instance msnd_proper : Proper (pord ==> pord) (@snd U V).
Global Instance mmsnd_proper : Proper (pord ==> pord) (@snd U V).
Proof.
intros [a1 b1] [a2 b2] [Ha Hb]; assumption.
Qed.
......
......@@ -92,6 +92,15 @@ Section Exclusive.
Proof.
exists ex_unit. exact I.
Qed.
Lemma ex_own_le t r t':
ex_own t r -> r ex_own t' ->
t == t'.
Proof.
move=>[r1 Heq1] [r2 Heq2]. destruct r1, r2, r; simpl in *; try contradiction; [].
rewrite Heq1 Heq2. reflexivity.
Qed.
End Exclusive.
Arguments ex T : clear implicits.
......
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