Commit f90f06b6 authored by Ralf Jung's avatar Ralf Jung

define view shifts and weakest-pre, and show they are all the things though...

define view shifts and weakest-pre, and show they are all the things though ought to be (downclosed, non-expansive, monotone)

On branch hackgreement
	modified:   coq-ho/iris_plog.v
no changes added to commit (use "git add" and/or "git commit -a")
parent 6214b229
......@@ -85,7 +85,7 @@ Module Type IRIS_CORE (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
Instance Props_CBI : ComplBI Props | 0 := _.
Instance Props_Eq : EqBI Props | 0 := _.
Implicit Types (P Q : Props) (w : Wld) (n i k : nat) (r u v : res) (σ : state).
Implicit Types (P Q : Props) (w : Wld) (n i k : nat) (r : res) (σ : state).
Definition Invs (w: Wld) := fst w.
Definition State (w: Wld) := fst (snd w).
......@@ -132,6 +132,27 @@ Module Type IRIS_CORE (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
End Views.
Section SimplProper.
Lemma dist_props_simpl U (R : relation U) (f : U -> Props) n {RS : Symmetric R}
(HP : forall u1 u2 w m, m <= n -> R u1 u2 -> f u1 w m -> f u2 w m) :
Proper (R ==> dist n) f.
Proof.
intros u1 u2 HRu m; split; intros HF;
eapply HP; eassumption || symmetry; eassumption.
Qed.
Lemma dist_props_simpl2 U V (RU : relation U) (RV : relation V)
(f : U -> V -> Props) n {RS : Symmetric RU} {VS : Symmetric RV}
(HP : forall u1 u2 v1 v2 w m, m <= n -> RU u1 u2 -> RV v1 v2 -> f u1 v1 w m -> f u2 v2 w m) :
Proper (RU ==> RV ==> dist n) f.
Proof.
intros u1 u2 HRu v1 v2 HRv m; split; intros HF;
eapply HP; eassumption || symmetry; eassumption.
Qed.
End SimplProper.
Section Resources.
Lemma state_sep {σ g rf} (Hv : (ex_own σ, g) · rf) : fst rf == 1 (ex_own σ)
......
This diff is collapsed.
......@@ -142,17 +142,32 @@ Section Definitions.
(HP : forall u1 u2 n, R u1 u2 -> f u1 n -> f u2 n) :
Proper (R ==> equiv) f.
Proof.
intros u1 u2 HRu; split; intros HF; (eapply HP; [| eassumption]);
[| symmetry]; assumption.
split; intros HF;
eapply HP; eassumption || symmetry; eassumption.
Qed.
Lemma dist_spred_simpl U (R : relation U) (f : U -> SPred) n {RS : Symmetric R}
(HP : forall u1 u2 m (HLt : m <= n), R u1 u2 -> f u1 m -> f u2 m) :
Proper (R ==> dist n) f.
Proof.
intros u1 u2 HRu m; split; intros HF;
(eapply HP; [eassumption | | eassumption]); [| symmetry]; assumption.
split; intros HF;
eapply HP; eassumption || symmetry; eassumption.
Qed.
Lemma equiv_spred_simpl2 U V (RU : relation U) (RV : relation V) (f : U -> V -> SPred) {US : Symmetric RU} {VS : Symmetric RV}
(HP : forall u1 u2 v1 v2 n, RU u1 u2 -> RV v1 v2 -> f u1 v1 n -> f u2 v2 n) :
Proper (RU ==> RV ==> equiv) f.
Proof.
split; intros HF;
eapply HP; eassumption || symmetry; eassumption.
Qed.
Lemma dist_spred_simpl2 U V (RU : relation U) (RV : relation V) (f : U -> V -> SPred) n {US : Symmetric RU} {VS : Symmetric RV}
(HP : forall u1 u2 v1 v2 m (HLt : m <= n), RU u1 u2 -> RV v1 v2 -> f u1 v1 m -> f u2 v2 m) :
Proper (RU ==> RV ==> dist n) f.
Proof.
split; intros HF;
eapply HP; eassumption || symmetry; eassumption.
Qed.
End Definitions.
Arguments dpred {s} {n m} _ _.
......
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