Commit 56dcb30c authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Merge branch 'jh/exist_plainly' into 'gen_proofmode'

Remove plainly_exist_1 from the BI axioms.

See merge request FP/iris-coq!95
parents ca0996a8 c2e7d39b
......@@ -31,10 +31,6 @@ Proof.
apply limit_preserving_and; by apply limit_preserving_entails.
Qed.
(* Affine *)
Global Instance uPred_affine : BiAffine (uPredI M) | 0.
Proof. intros P. rewrite /Affine. by apply bi.pure_intro. Qed.
(* Own and valid derived *)
Lemma persistently_cmra_valid_1 {A : cmraT} (a : A) :
a bi_persistently ( a : uPred M).
......
......@@ -474,8 +474,6 @@ Proof.
unseal; split=> n x ?? //.
- (* (∀ a, bi_plainly (Ψ a)) ⊢ bi_plainly (∀ a, Ψ a) *)
by unseal.
- (* bi_plainly (∃ a, Ψ a) ⊢ ∃ a, bi_plainly (Ψ a) *)
by unseal.
- (* bi_plainly ((P → Q) ∧ (Q → P)) ⊢ P ≡ Q *)
unseal; split=> n x ? /= HPQ; split=> n' x' ? HP;
split; eapply HPQ; eauto using @ucmra_unit_least.
......@@ -610,6 +608,14 @@ Proof.
Qed.
Global Instance bupd_proper : Proper (() ==> ()) (@uPred_bupd M) := ne_proper _.
(** BI instances *)
Global Instance uPred_affine : BiAffine (uPredI M) | 0.
Proof. intros P. rewrite /Affine. by apply bi.pure_intro. Qed.
Global Instance uPred_plainly_exist_1 : BiPlainlyExist (uPredI M).
Proof. unfold BiPlainlyExist. by unseal. Qed.
(** Limits *)
Lemma entails_lim (cP cQ : chain (uPredC M)) :
( n, cP n cQ n) compl cP compl cQ.
......
......@@ -45,6 +45,11 @@ Existing Instance absorbing_bi | 0.
Class BiPositive (PROP : bi) :=
bi_positive (P Q : PROP) : bi_affinely (P Q) bi_affinely P Q.
Class BiPlainlyExist (PROP : bi) :=
plainly_exist_1 A (Ψ : A PROP) :
bi_plainly ( a, Ψ a) a, bi_plainly (Ψ a).
Arguments plainly_exist_1 _ {_ _} _.
Definition bi_absorbingly {PROP : bi} (P : PROP) : PROP := (True P)%I.
Arguments bi_absorbingly {_} _%I : simpl never.
Instance: Params (@bi_absorbingly) 1.
......
......@@ -1075,15 +1075,18 @@ Proof.
apply (anti_symm _); auto using plainly_forall_2.
apply forall_intro=> x. by rewrite (forall_elim x).
Qed.
Lemma plainly_exist {A} (Ψ : A PROP) :
Lemma plainly_exist_2 {A} (Ψ : A PROP) :
( a, bi_plainly (Ψ a)) bi_plainly ( a, Ψ a).
Proof. apply exist_elim=> x. by rewrite (exist_intro x). Qed.
Lemma plainly_exist `{BiPlainlyExist PROP} {A} (Ψ : A PROP) :
bi_plainly ( a, Ψ a) a, bi_plainly (Ψ a).
Proof.
apply (anti_symm _); auto using plainly_exist_1.
apply exist_elim=> x. by rewrite (exist_intro x).
Qed.
Proof. apply (anti_symm _); auto using plainly_exist_1, plainly_exist_2. Qed.
Lemma plainly_and P Q : bi_plainly (P Q) bi_plainly P bi_plainly Q.
Proof. rewrite !and_alt plainly_forall. by apply forall_proper=> -[]. Qed.
Lemma plainly_or P Q : bi_plainly (P Q) bi_plainly P bi_plainly Q.
Lemma plainly_or_2 P Q : bi_plainly P bi_plainly Q bi_plainly (P Q).
Proof. rewrite !or_alt -plainly_exist_2. by apply exist_mono=> -[]. Qed.
Lemma plainly_or `{BiPlainlyExist PROP} P Q :
bi_plainly (P Q) bi_plainly P bi_plainly Q.
Proof. rewrite !or_alt plainly_exist. by apply exist_proper=> -[]. Qed.
Lemma plainly_impl P Q : bi_plainly (P Q) bi_plainly P bi_plainly Q.
Proof.
......@@ -1254,9 +1257,14 @@ Proof.
Qed.
Lemma affinely_plainly_and P Q : (P Q) P Q.
Proof. by rewrite plainly_and affinely_and. Qed.
Lemma affinely_plainly_or P Q : (P Q) P Q.
Lemma affinely_plainly_or_2 P Q : P Q (P Q).
Proof. by rewrite -plainly_or_2 affinely_or. Qed.
Lemma affinely_plainly_or `{BiPlainlyExist PROP} P Q : (P Q) P Q.
Proof. by rewrite plainly_or affinely_or. Qed.
Lemma affinely_plainly_exist {A} (Φ : A PROP) : ( x, Φ x) x, Φ x.
Lemma affinely_plainly_exist_2 {A} (Φ : A PROP) : ( x, Φ x) ( x, Φ x).
Proof. by rewrite -plainly_exist_2 affinely_exist. Qed.
Lemma affinely_plainly_exist `{BiPlainlyExist PROP} {A} (Φ : A PROP) :
( x, Φ x) x, Φ x.
Proof. by rewrite plainly_exist affinely_exist. Qed.
Lemma affinely_plainly_sep_2 P Q : P Q (P Q).
Proof. by rewrite affinely_sep_2 plainly_sep_2. Qed.
......@@ -1415,9 +1423,17 @@ Lemma plainly_if_pure p φ : bi_plainly_if p ⌜φ⌝ ⊣⊢ ⌜φ⌝.
Proof. destruct p; simpl; auto using plainly_pure. Qed.
Lemma plainly_if_and p P Q : bi_plainly_if p (P Q) bi_plainly_if p P bi_plainly_if p Q.
Proof. destruct p; simpl; auto using plainly_and. Qed.
Lemma plainly_if_or p P Q : bi_plainly_if p (P Q) bi_plainly_if p P bi_plainly_if p Q.
Lemma plainly_if_or_2 p P Q :
bi_plainly_if p P bi_plainly_if p Q bi_plainly_if p (P Q).
Proof. destruct p; simpl; auto using plainly_or_2. Qed.
Lemma plainly_if_or `{BiPlainlyExist PROP} p P Q :
bi_plainly_if p (P Q) bi_plainly_if p P bi_plainly_if p Q.
Proof. destruct p; simpl; auto using plainly_or. Qed.
Lemma plainly_if_exist {A} p (Ψ : A PROP) : (bi_plainly_if p ( a, Ψ a)) a, bi_plainly_if p (Ψ a).
Lemma plainly_if_exist_2 {A} p (Ψ : A PROP) :
( a, bi_plainly_if p (Ψ a)) bi_plainly_if p ( a, Ψ a).
Proof. destruct p; simpl; auto using plainly_exist_2. Qed.
Lemma plainly_if_exist `{BiPlainlyExist PROP} {A} p (Ψ : A PROP) :
bi_plainly_if p ( a, Ψ a) a, bi_plainly_if p (Ψ a).
Proof. destruct p; simpl; auto using plainly_exist. Qed.
Lemma plainly_if_sep `{BiPositive PROP} p P Q :
bi_plainly_if p (P Q) bi_plainly_if p P bi_plainly_if p Q.
......@@ -1442,9 +1458,15 @@ Lemma affinely_plainly_if_emp p : ■?p emp ⊣⊢ emp.
Proof. destruct p; simpl; auto using affinely_plainly_emp. Qed.
Lemma affinely_plainly_if_and p P Q : ?p (P Q) ?p P ?p Q.
Proof. destruct p; simpl; auto using affinely_plainly_and. Qed.
Lemma affinely_plainly_if_or p P Q : ?p (P Q) ?p P ?p Q.
Lemma affinely_plainly_if_or_2 p P Q : ?p P ?p Q ?p (P Q).
Proof. destruct p; simpl; auto using affinely_plainly_or_2. Qed.
Lemma affinely_plainly_if_or `{BiPlainlyExist PROP} p P Q :
?p (P Q) ?p P ?p Q.
Proof. destruct p; simpl; auto using affinely_plainly_or. Qed.
Lemma affinely_plainly_if_exist {A} p (Ψ : A PROP) :
Lemma affinely_plainly_if_exist_2 {A} p (Ψ : A PROP) :
( a, ?p Ψ a) ?p a, Ψ a .
Proof. destruct p; simpl; auto using affinely_plainly_exist_2. Qed.
Lemma affinely_plainly_if_exist `{BiPlainlyExist PROP} {A} p (Ψ : A PROP) :
(?p a, Ψ a) a, ?p Ψ a.
Proof. destruct p; simpl; auto using affinely_plainly_exist. Qed.
Lemma affinely_plainly_if_sep_2 p P Q : ?p P ?p Q ?p (P Q).
......@@ -1683,7 +1705,7 @@ Proof. apply plainly_emp_intro. Qed.
Global Instance and_plain P Q : Plain P Plain Q Plain (P Q).
Proof. intros. by rewrite /Plain plainly_and -!plain. Qed.
Global Instance or_plain P Q : Plain P Plain Q Plain (P Q).
Proof. intros. by rewrite /Plain plainly_or -!plain. Qed.
Proof. intros. by rewrite /Plain -plainly_or_2 -!plain. Qed.
Global Instance forall_plain {A} (Ψ : A PROP) :
( x, Plain (Ψ x)) Plain ( x, Ψ x).
Proof.
......@@ -1692,7 +1714,7 @@ Qed.
Global Instance exist_plain {A} (Ψ : A PROP) :
( x, Plain (Ψ x)) Plain ( x, Ψ x).
Proof.
intros. rewrite /Plain plainly_exist. apply exist_mono=> x. by rewrite -plain.
intros. rewrite /Plain -plainly_exist_2. apply exist_mono=> x. by rewrite -plain.
Qed.
Global Instance internal_eq_plain {A : ofeT} (a b : A) :
......@@ -1744,7 +1766,7 @@ Proof.
split; [split|]; try apply _. apply plainly_and. apply plainly_pure.
Qed.
Global Instance bi_plainly_or_homomorphism :
Global Instance bi_plainly_or_homomorphism `{BiPlainlyExist PROP} :
MonoidHomomorphism bi_or bi_or () (@bi_plainly PROP).
Proof.
split; [split|]; try apply _. apply plainly_or. apply plainly_pure.
......@@ -2053,7 +2075,10 @@ Proof.
Qed.
Lemma except_0_later P : P P.
Proof. by rewrite /bi_except_0 -later_or False_or. Qed.
Lemma except_0_plainly P : bi_plainly P bi_plainly ( P).
Lemma except_0_plainly_1 P : bi_plainly P bi_plainly ( P).
Proof. by rewrite /bi_except_0 -plainly_or_2 -later_plainly plainly_pure. Qed.
Lemma except_0_plainly `{BiPlainlyExist PROP} P :
bi_plainly P bi_plainly ( P).
Proof. by rewrite /bi_except_0 plainly_or -later_plainly plainly_pure. Qed.
Lemma except_0_persistently P : bi_persistently P bi_persistently ( P).
Proof.
......@@ -2061,11 +2086,12 @@ Proof.
Qed.
Lemma except_0_affinely_2 P : bi_affinely ( P) bi_affinely P.
Proof. rewrite /bi_affinely except_0_and. auto using except_0_intro. Qed.
Lemma except_0_affinely_plainly_2 P : P P.
Lemma except_0_affinely_plainly_2 `{BiPlainlyExist PROP} P : P P.
Proof. by rewrite -except_0_plainly except_0_affinely_2. Qed.
Lemma except_0_affinely_persistently_2 P : P P.
Proof. by rewrite -except_0_persistently except_0_affinely_2. Qed.
Lemma except_0_affinely_plainly_if_2 p P : ?p P ?p P.
Lemma except_0_affinely_plainly_if_2 `{BiPlainlyExist PROP} p P :
?p P ?p P.
Proof. destruct p; simpl; auto using except_0_affinely_plainly_2. Qed.
Lemma except_0_affinely_persistently_if_2 p P : ?p P ?p P.
Proof. destruct p; simpl; auto using except_0_affinely_persistently_2. Qed.
......@@ -2142,7 +2168,8 @@ Proof.
- rewrite /bi_except_0; auto.
- apply exist_elim=> x. rewrite -(exist_intro x); auto.
Qed.
Global Instance plainly_timeless P : Timeless P Timeless (bi_plainly P).
Global Instance plainly_timeless P `{BiPlainlyExist PROP} :
Timeless P Timeless (bi_plainly P).
Proof.
intros. rewrite /Timeless /bi_except_0 later_plainly_1.
by rewrite (timeless P) /bi_except_0 plainly_or {1}plainly_elim.
......
......@@ -107,8 +107,6 @@ Section bi_mixin.
bi_mixin_plainly_forall_2 {A} (Ψ : A PROP) :
( a, bi_plainly (Ψ a)) bi_plainly ( a, Ψ a);
bi_mixin_plainly_exist_1 {A} (Ψ : A PROP) :
bi_plainly ( a, Ψ a) a, bi_plainly (Ψ a);
bi_mixin_prop_ext P Q : bi_plainly ((P Q) (Q P))
bi_internal_eq (OfeT PROP prop_ofe_mixin) P Q;
......@@ -449,9 +447,6 @@ Proof. eapply bi_mixin_plainly_idemp_2, bi_bi_mixin. Qed.
Lemma plainly_forall_2 {A} (Ψ : A PROP) :
( a, bi_plainly (Ψ a)) bi_plainly ( a, Ψ a).
Proof. eapply bi_mixin_plainly_forall_2, bi_bi_mixin. Qed.
Lemma plainly_exist_1 {A} (Ψ : A PROP) :
bi_plainly ( a, Ψ a) a, bi_plainly (Ψ a).
Proof. eapply bi_mixin_plainly_exist_1, bi_bi_mixin. Qed.
Lemma prop_ext P Q : bi_plainly ((P Q) (Q P)) P Q.
Proof. eapply (bi_mixin_prop_ext _ bi_entails), bi_bi_mixin. Qed.
Lemma persistently_impl_plainly P Q :
......
......@@ -495,7 +495,7 @@ Global Instance from_or_absorbingly P Q1 Q2 :
Proof. rewrite /FromOr=> <-. by rewrite absorbingly_or. Qed.
Global Instance from_or_plainly P Q1 Q2 :
FromOr P Q1 Q2 FromOr (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2).
Proof. rewrite /FromOr=> <-. by rewrite plainly_or. Qed.
Proof. rewrite /FromOr=> <-. by rewrite -plainly_or_2. Qed.
Global Instance from_or_persistently P Q1 Q2 :
FromOr P Q1 Q2
FromOr (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
......@@ -512,7 +512,7 @@ Proof. rewrite /IntoOr=>->. by rewrite affinely_or. Qed.
Global Instance into_or_absorbingly P Q1 Q2 :
IntoOr P Q1 Q2 IntoOr (bi_absorbingly P) (bi_absorbingly Q1) (bi_absorbingly Q2).
Proof. rewrite /IntoOr=>->. by rewrite absorbingly_or. Qed.
Global Instance into_or_plainly P Q1 Q2 :
Global Instance into_or_plainly `{BiPlainlyExist PROP} P Q1 Q2 :
IntoOr P Q1 Q2 IntoOr (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2).
Proof. rewrite /IntoOr=>->. by rewrite plainly_or. Qed.
Global Instance into_or_persistently P Q1 Q2 :
......@@ -534,7 +534,7 @@ Global Instance from_exist_absorbingly {A} P (Φ : A → PROP) :
Proof. rewrite /FromExist=> <-. by rewrite absorbingly_exist. Qed.
Global Instance from_exist_plainly {A} P (Φ : A PROP) :
FromExist P Φ FromExist (bi_plainly P) (λ a, bi_plainly (Φ a))%I.
Proof. rewrite /FromExist=> <-. by rewrite plainly_exist. Qed.
Proof. rewrite /FromExist=> <-. by rewrite -plainly_exist_2. Qed.
Global Instance from_exist_persistently {A} P (Φ : A PROP) :
FromExist P Φ FromExist (bi_persistently P) (λ a, bi_persistently (Φ a))%I.
Proof. rewrite /FromExist=> <-. by rewrite persistently_exist. Qed.
......@@ -564,7 +564,7 @@ Qed.
Global Instance into_exist_absorbingly {A} P (Φ : A PROP) :
IntoExist P Φ IntoExist (bi_absorbingly P) (λ a, bi_absorbingly (Φ a))%I.
Proof. rewrite /IntoExist=> HP. by rewrite HP absorbingly_exist. Qed.
Global Instance into_exist_plainly {A} P (Φ : A PROP) :
Global Instance into_exist_plainly `{BiPlainlyExist PROP} {A} P (Φ : A PROP) :
IntoExist P Φ IntoExist (bi_plainly P) (λ a, bi_plainly (Φ a))%I.
Proof. rewrite /IntoExist=> HP. by rewrite HP plainly_exist. Qed.
Global Instance into_exist_persistently {A} P (Φ : A PROP) :
......@@ -1051,7 +1051,7 @@ Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_affinely_2. Qed.
Global Instance into_except_0_absorbingly P Q :
IntoExcept0 P Q IntoExcept0 (bi_absorbingly P) (bi_absorbingly Q).
Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_absorbingly. Qed.
Global Instance into_except_0_plainly P Q :
Global Instance into_except_0_plainly `{BiPlainlyExist PROP} P Q :
IntoExcept0 P Q IntoExcept0 (bi_plainly P) (bi_plainly Q).
Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_plainly. Qed.
Global Instance into_except_0_persistently P Q :
......
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