Commit 0de297e1 authored by Ralf Jung's avatar Ralf Jung
Browse files

more FromPure and IntoPure instances

parent a928919c
......@@ -43,6 +43,24 @@ Global Instance into_pure_cmra_valid `{CMRADiscrete A} (a : A) :
@IntoPure M ( a) ( a).
Proof. by rewrite /IntoPure discrete_valid. Qed.
Global Instance into_pure_pure_conj (φ1 φ2 : uPred M) P1 P2 :
IntoPure φ1 P1 -> IntoPure φ2 P2 -> IntoPure (φ1 φ2) (P1 P2).
Proof. rewrite /IntoPure pure_and. by intros -> ->. Qed.
Global Instance into_pure_pure_sep (φ1 φ2 : uPred M) P1 P2 :
IntoPure φ1 P1 -> IntoPure φ2 P2 -> IntoPure (φ1 φ2) (P1 P2).
Proof. rewrite /IntoPure sep_and pure_and. by intros -> ->. Qed.
Global Instance into_pure_pure_disj (φ1 φ2 : uPred M) P1 P2 :
IntoPure φ1 P1 -> IntoPure φ2 P2 -> IntoPure (φ1 φ2) (P1 P2).
Proof. rewrite /IntoPure pure_or. by intros -> ->. Qed.
Global Instance into_pure_pure_impl (φ1 φ2 : uPred M) P1 P2 :
FromPure φ1 P1 -> IntoPure φ2 P2 -> IntoPure (φ1 φ2) (P1 P2).
Proof. rewrite /FromPure /IntoPure pure_impl. by intros -> ->. Qed.
Global Instance into_pure_pure_wand (φ1 φ2 : uPred M) P1 P2 :
FromPure φ1 P1 -> IntoPure φ2 P2 -> IntoPure (φ1 - φ2) (P1 P2).
Proof.
rewrite /FromPure /IntoPure pure_impl always_impl_wand. by intros -> ->.
Qed.
Global Instance into_pure_exist {X : Type} (Φ : X uPred M) φ :
( x, @IntoPure M (Φ x) (φ x)) @IntoPure M ( x, Φ x) ( x, φ x).
Proof.
......@@ -55,15 +73,6 @@ Global Instance into_pure_forall {X : Type} (Φ : X → uPred M) φ :
Proof.
rewrite /IntoPure=>Hx. rewrite -pure_forall_2. by setoid_rewrite Hx.
Qed.
Global Instance into_pure_pure_conj (φ1 φ2 : uPred M) P1 P2 :
IntoPure φ1 P1 -> IntoPure φ2 P2 -> IntoPure (φ1 φ2) (P1 P2).
Proof. rewrite /IntoPure pure_and. by intros -> ->. Qed.
Global Instance into_pure_pure_sep (φ1 φ2 : uPred M) P1 P2 :
IntoPure φ1 P1 -> IntoPure φ2 P2 -> IntoPure (φ1 φ2) (P1 P2).
Proof. rewrite /IntoPure sep_and pure_and. by intros -> ->. Qed.
Global Instance into_pure_pure_disj (φ1 φ2 : uPred M) P1 P2 :
IntoPure φ1 P1 -> IntoPure φ2 P2 -> IntoPure (φ1 φ2) (P1 P2).
Proof. rewrite /IntoPure pure_or. by intros -> ->. Qed.
(* FromPure *)
Global Instance from_pure_pure φ : @FromPure M ⌜φ⌝ φ.
......@@ -82,6 +91,38 @@ Qed.
Global Instance from_pure_bupd P φ : FromPure P φ FromPure (|==> P) φ.
Proof. rewrite /FromPure=> ->. apply bupd_intro. Qed.
Global Instance from_pure_pure_conj (φ1 φ2 : uPred M) P1 P2 :
FromPure φ1 P1 -> FromPure φ2 P2 -> FromPure (φ1 φ2) (P1 P2).
Proof. rewrite /FromPure pure_and. by intros -> ->. Qed.
Global Instance from_pure_pure_sep (φ1 φ2 : uPred M) P1 P2 :
FromPure φ1 P1 -> FromPure φ2 P2 -> FromPure (φ1 φ2) (P1 P2).
Proof. rewrite /FromPure pure_and always_and_sep_l. by intros -> ->. Qed.
Global Instance from_pure_pure_disj (φ1 φ2 : uPred M) P1 P2 :
FromPure φ1 P1 -> FromPure φ2 P2 -> FromPure (φ1 φ2) (P1 P2).
Proof. rewrite /FromPure pure_or. by intros -> ->. Qed.
Global Instance from_pure_pure_impl (φ1 φ2 : uPred M) P1 P2 :
IntoPure φ1 P1 -> FromPure φ2 P2 -> FromPure (φ1 φ2) (P1 P2).
Proof. rewrite /FromPure /IntoPure pure_impl. by intros -> ->. Qed.
Global Instance from_pure_pure_wand (φ1 φ2 : uPred M) P1 P2 :
IntoPure φ1 P1 -> FromPure φ2 P2 -> FromPure (φ1 - φ2) (P1 P2).
Proof.
rewrite /FromPure /IntoPure pure_impl always_impl_wand. by intros -> ->.
Qed.
Global Instance from_pure_exist {X : Type} (Φ : X uPred M) φ :
( x, @FromPure M (Φ x) (φ x)) @FromPure M ( x, Φ x) ( x, φ x).
Proof.
rewrite /FromPure=>Hx. apply pure_elim'=>-[x ?]. rewrite -(exist_intro x).
rewrite -Hx. apply pure_intro. done.
Qed.
Global Instance from_pure_forall {X : Type} (Φ : X uPred M) φ :
( x, @FromPure M (Φ x) (φ x)) @FromPure M ( x, Φ x) ( x, φ x).
Proof.
rewrite /FromPure=>Hx. apply forall_intro=>x. apply pure_elim'=>Hφ.
rewrite -Hx. apply pure_intro. done.
Qed.
(* IntoPersistentP *)
Global Instance into_persistentP_always_trans P Q :
IntoPersistentP P Q IntoPersistentP ( P) Q | 0.
......
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