Commit 2c2f36f5 by Robbert Krebbers

### Change proposition extensionality.

```As suggested by @jjourdan, and proved in the ordered RA model by @amintimany.

This should solve the paradox in #149.```
parent 1f24d020
 ... ... @@ -501,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 *) ... ... @@ -523,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 *) ... ...
 ... ... @@ -1909,10 +1909,10 @@ 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 `{!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. ... ...
 ... ... @@ -158,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 *) ... ... @@ -261,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. ... ... @@ -488,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 *) ... ...
 ... ... @@ -345,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!