Commit f072ab70 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coq

parents 99cbb525 f72563c7
...@@ -35,7 +35,7 @@ Notation "P ⊣⊢ Q" := (equiv (A:=uPred M) P%I Q%I). (* Force implicit argumen ...@@ -35,7 +35,7 @@ Notation "P ⊣⊢ Q" := (equiv (A:=uPred M) P%I Q%I). (* Force implicit argumen
(* Derived logical stuff *) (* Derived logical stuff *)
Lemma False_elim P : False P. Lemma False_elim P : False P.
Proof. by apply (pure_elim False). Qed. Proof. by apply (pure_elim' False). Qed.
Lemma True_intro P : P True. Lemma True_intro P : P True.
Proof. by apply pure_intro. Qed. Proof. by apply pure_intro. Qed.
...@@ -212,6 +212,11 @@ Proof. ...@@ -212,6 +212,11 @@ Proof.
- apply or_elim; apply exist_elim=> a; rewrite -(exist_intro a); auto. - apply or_elim; apply exist_elim=> a; rewrite -(exist_intro a); auto.
Qed. Qed.
Lemma pure_elim φ Q R : (Q ⌜φ⌝) (φ Q R) Q R.
Proof.
intros HQ HQR. rewrite -(idemp uPred_and Q) {1}HQ.
apply impl_elim_l', pure_elim'=> ?. by apply entails_impl, HQR.
Qed.
Lemma pure_mono φ1 φ2 : (φ1 φ2) ⌜φ1 ⌜φ2. Lemma pure_mono φ1 φ2 : (φ1 φ2) ⌜φ1 ⌜φ2.
Proof. intros; apply pure_elim with φ1; eauto. Qed. Proof. intros; apply pure_elim with φ1; eauto. Qed.
Global Instance pure_mono' : Proper (impl ==> ()) (@uPred_pure M). Global Instance pure_mono' : Proper (impl ==> ()) (@uPred_pure M).
......
...@@ -318,10 +318,8 @@ Global Instance bupd_proper : Proper ((≡) ==> (≡)) (@uPred_bupd M) := ne_pro ...@@ -318,10 +318,8 @@ Global Instance bupd_proper : Proper ((≡) ==> (≡)) (@uPred_bupd M) := ne_pro
(** Introduction and elimination rules *) (** Introduction and elimination rules *)
Lemma pure_intro φ P : φ P ⌜φ⌝. Lemma pure_intro φ P : φ P ⌜φ⌝.
Proof. by intros ?; unseal; split. Qed. Proof. by intros ?; unseal; split. Qed.
Lemma pure_elim φ Q R : (Q ⌜φ⌝) (φ Q R) Q R. Lemma pure_elim' φ P : (φ True P) ⌜φ⌝ P.
Proof. Proof. unseal; intros HP; split=> n x ??. by apply HP. Qed.
unseal; intros HQP HQR; split=> n x ??; apply HQR; first eapply HQP; eauto.
Qed.
Lemma pure_forall_2 {A} (φ : A Prop) : ( x : A, ⌜φ x) x : A, φ x. Lemma pure_forall_2 {A} (φ : A Prop) : ( x : A, ⌜φ x) x : A, φ x.
Proof. by unseal. Qed. Proof. by unseal. 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