Commit 45b378c1 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'robbert/repair_plainly' into 'gen_proofmode'

Repair the plainly modality

See merge request FP/iris-coq!122
parents dad9e782 fbde58f6
Pipeline #7056 passed with stage
in 10 minutes and 50 seconds
......@@ -486,8 +486,6 @@ Proof.
intros P QR HP. unseal; split=> n x ? /=. by apply HP, cmra_core_validN.
- (* bi_persistently P ⊢ bi_persistently (bi_persistently P) *)
intros P. unseal; split=> n x ?? /=. by rewrite cmra_core_idemp.
- (* bi_plainly (bi_persistently P) ⊢ bi_plainly P (ADMISSIBLE) *)
intros P. unseal; split=> n x ?? /=. by rewrite -(core_id_core ε).
- (* (∀ a, bi_persistently (Ψ a)) ⊢ bi_persistently (∀ a, Ψ a) *)
by unseal.
- (* bi_persistently (∃ a, Ψ a) ⊢ ∃ a, bi_persistently (Ψ a) *)
......@@ -503,8 +501,8 @@ Qed.
Lemma uPred_sbi_mixin (M : ucmraT) : SbiMixin uPred_ofe_mixin
uPred_entails uPred_pure uPred_and uPred_or uPred_impl
(@uPred_forall M) (@uPred_exist M) uPred_sep uPred_plainly uPred_persistently
(@uPred_internal_eq M) uPred_later.
(@uPred_forall M) (@uPred_exist M) uPred_sep uPred_wand
uPred_plainly uPred_persistently (@uPred_internal_eq M) uPred_later.
Proof.
split.
- (* Contractive sbi_later *)
......@@ -525,9 +523,10 @@ Proof.
by unseal.
- (* Discrete a → a ≡ b ⊣⊢ ⌜a ≡ b⌝ *)
intros A a b ?. unseal; split=> n x ?; by apply (discrete_iff n).
- (* 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.
- (* bi_plainly ((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q *)
unseal; split=> n x ? /= HPQ. split=> n' x' ??.
move: HPQ=> [] /(_ n' x'); rewrite !left_id=> ?.
move=> /(_ n' x'); rewrite !left_id=> ?. naive_solver.
- (* Next x ≡ Next y ⊢ ▷ (x ≡ y) *)
by unseal.
- (* ▷ (x ≡ y) ⊢ Next x ≡ Next y *)
......
......@@ -957,8 +957,11 @@ Proof.
Qed.
Lemma plainly_persistently P : bi_plainly (bi_persistently P) bi_plainly P.
Proof.
apply (anti_symm _); first apply plainly_persistently_1.
by rewrite {1}plainly_idemp_2 (plainly_elim_persistently P).
apply (anti_symm _).
- rewrite -{1}(left_id True%I bi_and (bi_plainly _)) (plainly_emp_intro True%I).
rewrite -{2}(persistently_and_emp_elim P).
rewrite !and_alt -plainly_forall_2. by apply forall_mono=> -[].
- by rewrite {1}plainly_idemp_2 (plainly_elim_persistently P).
Qed.
Lemma absorbingly_plainly P : bi_absorbingly (bi_plainly P) bi_plainly P.
......@@ -1080,6 +1083,13 @@ Qed.
Lemma impl_wand_plainly_2 P Q : (bi_plainly P - Q) (bi_plainly P Q).
Proof. apply impl_intro_l. by rewrite plainly_and_sep_l_1 wand_elim_r. Qed.
Lemma valid_plainly P : bi_valid (bi_plainly P) bi_valid P.
Proof.
rewrite /bi_valid. split; intros HP.
- by rewrite -(idemp bi_and emp%I) {2}HP plainly_and_emp_elim.
- by rewrite (plainly_emp_intro emp%I) HP.
Qed.
Section plainly_affinely_bi.
Context `{BiAffine PROP}.
......@@ -1906,14 +1916,34 @@ Proof.
rewrite -(internal_eq_refl True%I a) plainly_pure; auto.
Qed.
Lemma plainly_alt P : bi_plainly P P True.
Lemma plainly_alt P : bi_plainly P bi_affinely P emp.
Proof.
rewrite -plainly_affinely. apply (anti_symm ()).
- rewrite -prop_ext. apply plainly_mono, and_intro; apply wand_intro_l.
+ by rewrite affinely_elim_emp left_id.
+ by rewrite left_id.
- rewrite internal_eq_sym (internal_eq_rewrite _ _ bi_plainly).
by rewrite -plainly_True_emp plainly_pure True_impl.
Qed.
Lemma plainly_alt_absorbing P `{!Absorbing P} : bi_plainly P P True.
Proof.
apply (anti_symm ()).
- rewrite -prop_ext. apply plainly_mono, and_intro; apply impl_intro_r; auto.
- rewrite -prop_ext. apply plainly_mono, and_intro; apply wand_intro_l; auto.
- rewrite internal_eq_sym (internal_eq_rewrite _ _ bi_plainly).
by rewrite plainly_pure True_impl.
Qed.
Lemma plainly_True_alt P : bi_plainly (True - P) P True.
Proof.
apply (anti_symm ()).
- rewrite -prop_ext. apply plainly_mono, and_intro; apply wand_intro_l; auto.
by rewrite wand_elim_r.
- rewrite internal_eq_sym (internal_eq_rewrite _ _
(λ Q, bi_plainly (True - Q)) ltac:(solve_proper)).
by rewrite -entails_wand // -(plainly_emp_intro True%I) True_impl.
Qed.
Global Instance internal_eq_absorbing {A : ofeT} (x y : A) :
Absorbing (x y : PROP)%I.
Proof. by rewrite /Absorbing absorbingly_internal_eq. Qed.
......
......@@ -129,8 +129,6 @@ Section bi_mixin.
(* In the ordered RA model: `core` is idempotent *)
bi_mixin_persistently_idemp_2 P :
bi_persistently P bi_persistently (bi_persistently P);
bi_mixin_plainly_persistently_1 P :
bi_plainly (bi_persistently P) bi_plainly P;
(* In the ordered RA model [P ⊢ persisently emp] (which can currently still
be derived from the plainly axioms, which will be removed): `ε ≼ core x` *)
......@@ -160,7 +158,7 @@ Section bi_mixin.
sbi_mixin_fun_ext {A} {B : A ofeT} (f g : ofe_fun B) : ( x, f x g x) f g;
sbi_mixin_sig_eq {A : ofeT} (P : A Prop) (x y : sig P) : `x `y x y;
sbi_mixin_discrete_eq_1 {A : ofeT} (a b : A) : Discrete a a b a b;
sbi_mixin_prop_ext P Q : bi_plainly ((P Q) (Q P))
sbi_mixin_prop_ext P Q : bi_plainly ((P - Q) (Q - P))
sbi_internal_eq (OfeT PROP prop_ofe_mixin) P Q;
(* Later *)
......@@ -263,8 +261,8 @@ Structure sbi := Sbi {
sbi_forall sbi_exist sbi_sep sbi_wand sbi_plainly
sbi_persistently;
sbi_sbi_mixin : SbiMixin sbi_ofe_mixin sbi_entails sbi_pure sbi_and sbi_or
sbi_impl sbi_forall sbi_exist sbi_sep sbi_plainly
sbi_persistently sbi_internal_eq sbi_later;
sbi_impl sbi_forall sbi_exist sbi_sep sbi_wand
sbi_plainly sbi_persistently sbi_internal_eq sbi_later;
}.
Instance: Params (@sbi_later) 1.
......@@ -453,9 +451,6 @@ Proof. eapply bi_mixin_persistently_mono, bi_bi_mixin. Qed.
Lemma persistently_idemp_2 P :
bi_persistently P bi_persistently (bi_persistently P).
Proof. eapply bi_mixin_persistently_idemp_2, bi_bi_mixin. Qed.
Lemma plainly_persistently_1 P :
bi_plainly (bi_persistently P) bi_plainly P.
Proof. eapply (bi_mixin_plainly_persistently_1 bi_entails), bi_bi_mixin. Qed.
Lemma persistently_forall_2 {A} (Ψ : A PROP) :
( a, bi_persistently (Ψ a)) bi_persistently ( a, Ψ a).
......@@ -493,7 +488,7 @@ Lemma discrete_eq_1 {A : ofeT} (a b : A) :
Discrete a a b (a b : PROP).
Proof. eapply sbi_mixin_discrete_eq_1, sbi_sbi_mixin. Qed.
Lemma prop_ext P Q : bi_plainly ((P Q) (Q P)) P Q.
Lemma prop_ext P Q : bi_plainly ((P - Q) (Q - P)) P Q.
Proof. eapply (sbi_mixin_prop_ext _ bi_entails), sbi_sbi_mixin. Qed.
(* Later *)
......
......@@ -326,7 +326,6 @@ Proof.
- intros P Q. split=> i. apply bi.sep_elim_l, _.
- intros P Q [?]. split=> i /=. by f_equiv.
- intros P. split=> i. by apply bi.persistently_idemp_2.
- intros P. split=> i /=. by setoid_rewrite bi.plainly_persistently_1.
- intros A Ψ. split=> i. by apply bi.persistently_forall_2.
- intros A Ψ. split=> i. by apply bi.persistently_exist_1.
- intros P Q. split=> i. apply bi.sep_elim_l, _.
......@@ -346,8 +345,8 @@ Context (I : biIndex) (PROP : sbi).
Lemma monPred_sbi_mixin :
SbiMixin (PROP:=monPred I PROP) monPred_ofe_mixin monPred_entails monPred_pure
monPred_and monPred_or monPred_impl monPred_forall monPred_exist
monPred_sep monPred_plainly monPred_persistently monPred_internal_eq
monPred_later.
monPred_sep monPred_wand monPred_plainly monPred_persistently
monPred_internal_eq monPred_later.
Proof.
split; unseal.
- intros n P Q HPQ. split=> i /=.
......
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