Commit b1fa82f0 authored by Ralf Jung's avatar Ralf Jung

proofmode: show that quantifiers preserve purity

parent 997c3ed8
Pipeline #3374 passed with stage
in 17 minutes and 56 seconds
......@@ -31,6 +31,19 @@ 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_exist {X : Type} (Φ : X uPred M) φ :
( x, @IntoPure M (Φ x) (φ x)) @IntoPure M ( x, Φ x) ( x, φ x).
Proof.
rewrite /IntoPure=>Hx. apply exist_elim=>x. rewrite Hx.
apply pure_elim'=>Hφ. apply pure_intro. eauto.
Qed.
Global Instance into_pure_forall {X : Type} (Φ : X uPred M) φ :
( x, @IntoPure M (Φ x) (φ x)) @IntoPure M ( x, Φ x) ( x, φ x).
Proof.
rewrite /IntoPure=>Hx. rewrite -pure_forall_2. by setoid_rewrite Hx.
Qed.
(* FromPure *)
Global Instance from_pure_pure φ : @FromPure M ⌜φ⌝ φ.
Proof. done. Qed.
......
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