Commit 45eb1be5 by Robbert Krebbers

### Use type class for internal equality.

parent abbe9f56
 ... ... @@ -47,6 +47,7 @@ theories/bi/derived_connectives.v theories/bi/derived_laws_bi.v theories/bi/derived_laws_sbi.v theories/bi/plainly.v theories/bi/internal_eq.v theories/bi/big_op.v theories/bi/updates.v theories/bi/ascii.v ... ...
 ... ... @@ -68,11 +68,11 @@ Check "test_iStopProof". Lemma test_iStopProof Q : emp -∗ Q -∗ Q. Proof. iIntros "#H1 H2". Show. iStopProof. Show. by rewrite bi.sep_elim_r. Qed. Lemma test_iRewrite {A : ofeT} (x y : A) P : Lemma test_iRewrite `{!BiInternalEq PROP} {A : ofeT} (x y : A) P : □ (∀ z, P -∗ (z ≡ y)) -∗ (P -∗ P ∧ (x,x) ≡ (y,x)). Proof. iIntros "#H1 H2". iRewrite (bi.internal_eq_sym x x with "[# //]"). iRewrite (internal_eq_sym x x with "[# //]"). iRewrite -("H1" \$! _ with "[- //]"). auto. Qed. ... ... @@ -127,7 +127,7 @@ Qed. Lemma test_iIntros_pure_not : ⊢@{PROP} ⌜ ¬False ⌝. Proof. by iIntros (?). Qed. Lemma test_fast_iIntros P Q : Lemma test_fast_iIntros `{!BiInternalEq PROP} P Q : ⊢ ∀ x y z : nat, ⌜x = plus 0 x⌝ → ⌜y = 0⌝ → ⌜z = 0⌝ → P → □ Q → foo (x ≡ x). Proof. ... ... @@ -298,7 +298,7 @@ Proof. unshelve iSpecialize ("H" \$! ∅ {[ 1%positive ]} ∅); try apply _. done. Qed. Lemma test_iFrame_pure {A : ofeT} (φ : Prop) (y z : A) : Lemma test_iFrame_pure `{!BiInternalEq PROP} {A : ofeT} (φ : Prop) (y z : A) : φ → ⌜y ≡ z⌝ -∗ (⌜ φ ⌝ ∧ ⌜ φ ⌝ ∧ y ≡ z : PROP). Proof. iIntros (Hv) "#Hxy". iFrame (Hv) "Hxy". Qed. ... ... @@ -390,7 +390,7 @@ Lemma test_iNext_quantifier {A} (Φ : A → A → PROP) : (∀ y, ∃ x, ▷ Φ x y) -∗ ▷ (∀ y, ∃ x, Φ x y). Proof. iIntros "H". iNext. done. Qed. Lemma text_iNext_Next {A B : ofeT} (f : A -n> A) x y : Lemma text_iNext_Next `{!BiInternalEq PROP} {A B : ofeT} (f : A -n> A) x y : Next x ≡ Next y -∗ (Next (f x) ≡ Next (f y) : PROP). Proof. iIntros "H". iNext. by iRewrite "H". Qed. ... ... @@ -458,7 +458,8 @@ Lemma test_iIntros_let P : ∀ Q, let R := emp%I in P -∗ R -∗ Q -∗ P ∗ Q. Proof. iIntros (Q R) "\$ _ \$". Qed. Lemma test_iNext_iRewrite P Q : ▷ (Q ≡ P) -∗ ▷ Q -∗ ▷ P. Lemma test_iNext_iRewrite `{!BiInternalEq PROP} P Q : ▷ (Q ≡ P) -∗ ▷ Q -∗ ▷ P. Proof. iIntros "#HPQ HQ !>". iNext. by iRewrite "HPQ" in "HQ". Qed. ... ... @@ -475,7 +476,8 @@ Lemma test_iIntros_rewrite P (x1 x2 x3 x4 : nat) : x1 = x2 → (⌜ x2 = x3 ⌝ ∗ ⌜ x3 ≡ x4 ⌝ ∗ P) -∗ ⌜ x1 = x4 ⌝ ∗ P. Proof. iIntros (?) "(-> & -> & \$)"; auto. Qed. Lemma test_iNext_affine P Q : ▷ (Q ≡ P) -∗ ▷ Q -∗ ▷ P. Lemma test_iNext_affine `{!BiInternalEq PROP} P Q : ▷ (Q ≡ P) -∗ ▷ Q -∗ ▷ P. Proof. iIntros "#HPQ HQ !>". iNext. by iRewrite "HPQ" in "HQ". Qed. Lemma test_iAlways P Q R : ... ... @@ -860,7 +862,7 @@ Lemma test_entails_annot_sections_space_close P : (P ⊣⊢@{PROP} P ) ∧ (⊣⊢@{PROP} ) P P ∧ (.⊣⊢ P ) P. Proof. naive_solver. Qed. Lemma test_bi_internal_eq_annot_sections P : Lemma test_bi_internal_eq_annot_sections `{!BiInternalEq PROP} P : ⊢@{PROP} P ≡@{PROP} P ∧ (≡@{PROP}) P P ∧ (P ≡.) P ∧ (.≡ P) P ∧ ((P ≡@{PROP} P)) ∧ ((≡@{PROP})) P P ∧ ((P ≡.)) P ∧ ((.≡ P)) P ∧ ... ...
 ... ... @@ -25,7 +25,7 @@ Section tests. Proof. iStartProof PROP. iIntros (i) "\$". Qed. Lemma test_iStartProof_6 P : P ⊣⊢ P. Proof. iStartProof PROP. iIntros (i). iSplit; iIntros "\$". Qed. Lemma test_iStartProof_7 P : ⊢@{monPredI} P ≡ P. Lemma test_iStartProof_7 `{!BiInternalEq PROP} P : ⊢@{monPredI} P ≡ P. Proof. iStartProof PROP. done. Qed. Lemma test_intowand_1 P Q : (P -∗ Q) -∗ P -∗ Q. ... ...
 ... ... @@ -59,7 +59,7 @@ Section excl_auth. Proof. rewrite auth_both_validI bi.and_elim_r bi.and_elim_l. apply bi.exist_elim=> -[[c|]|]; by rewrite bi.option_equivI /= excl_equivI //= bi.False_elim. by rewrite option_equivI /= excl_equivI //= bi.False_elim. Qed. Lemma excl_auth_frag_validN_op_1_l n a b : ✓{n} (◯E a ⋅ ◯E b) → False. ... ...
 From iris.bi Require Export derived_connectives updates plainly. From iris.bi Require Export derived_connectives updates internal_eq plainly. From iris.base_logic Require Export upred. Import uPred_primitive. ... ... @@ -66,21 +66,13 @@ Proof. - exact: persistently_and_sep_l_1. Qed. Lemma uPred_sbi_mixin (M : ucmraT) : SbiMixin uPred_entails uPred_pure uPred_or uPred_impl (@uPred_forall M) (@uPred_exist M) uPred_sep uPred_persistently (@uPred_internal_eq M) uPred_later. Lemma uPred_bi_later_mixin (M : ucmraT) : BiLaterMixin uPred_entails uPred_pure uPred_or uPred_impl (@uPred_forall M) (@uPred_exist M) uPred_sep uPred_persistently uPred_later. Proof. split. - apply contractive_ne, later_contractive. - exact: internal_eq_ne. - exact: @internal_eq_refl. - exact: @internal_eq_rewrite. - exact: @fun_ext. - exact: @sig_eq. - exact: @discrete_eq_1. - exact: @later_eq_1. - exact: @later_eq_2. - exact: later_mono. - exact: later_intro. - exact: @later_forall_2. ... ... @@ -94,11 +86,27 @@ Qed. Canonical Structure uPredI (M : ucmraT) : bi := {| bi_ofe_mixin := ofe_mixin_of (uPred M); bi_bi_mixin := uPred_bi_mixin M; bi_sbi_mixin := uPred_sbi_mixin M |}. bi_bi_mixin := uPred_bi_mixin M; bi_bi_later_mixin := uPred_bi_later_mixin M |}. Instance uPred_later_contractive {M} : Contractive (bi_later (PROP:=uPredI M)). Proof. apply later_contractive. Qed. Lemma uPred_internal_eq_mixin M : BiInternalEqMixin (uPredI M) (@uPred_internal_eq M). Proof. split. - exact: internal_eq_ne. - exact: @internal_eq_refl. - exact: @internal_eq_rewrite. - exact: @fun_ext. - exact: @sig_eq. - exact: @discrete_eq_1. - exact: @later_eq_1. - exact: @later_eq_2. Qed. Global Instance uPred_internal_eq M : BiInternalEq (uPredI M) := {| bi_internal_eq_mixin := uPred_internal_eq_mixin M |}. Lemma uPred_plainly_mixin M : BiPlainlyMixin (uPredI M) uPred_plainly. Proof. split. ... ... @@ -120,13 +128,15 @@ Proof. etrans; first exact: sep_comm'. apply sep_mono; last done. exact: pure_intro. - exact: prop_ext_2. - exact: later_plainly_1. - exact: later_plainly_2. Qed. Global Instance uPred_plainlyC M : BiPlainly (uPredI M) := Global Instance uPred_plainly M : BiPlainly (uPredI M) := {| bi_plainly_mixin := uPred_plainly_mixin M |}. Global Instance uPred_prop_ext M : BiPropExt (uPredI M). Proof. exact: prop_ext_2. Qed. Lemma uPred_bupd_mixin M : BiBUpdMixin (uPredI M) uPred_bupd. Proof. split. ... ... @@ -223,9 +233,10 @@ End restate. Ltac unseal := (* Coq unfold is used to circumvent bug #5699 in rewrite /foo *) unfold bi_emp; simpl; unfold uPred_emp, bupd, bi_bupd_bupd, bi_pure, bi_and, bi_or, bi_impl, bi_forall, bi_exist, bi_sep, bi_wand, bi_persistently, bi_internal_eq, bi_later; simpl; unfold plainly, bi_plainly_plainly; simpl; bi_and, bi_or, bi_impl, bi_forall, bi_exist, bi_sep, bi_wand, bi_persistently, bi_later; simpl; unfold internal_eq, bi_internal_eq_internal_eq, plainly, bi_plainly_plainly; simpl; uPred_primitive.unseal. End uPred.
 ... ... @@ -162,5 +162,5 @@ End iProp_solution. Lemma iProp_unfold_equivI {Σ} (P Q : iProp Σ) : iProp_unfold P ≡ iProp_unfold Q ⊢@{iPropI Σ} P ≡ Q. Proof. rewrite -{2}(iProp_fold_unfold P) -{2}(iProp_fold_unfold Q). apply: bi.f_equiv. rewrite -{2}(iProp_fold_unfold P) -{2}(iProp_fold_unfold Q). apply: f_equivI. Qed.
 ... ... @@ -119,7 +119,7 @@ Proof. rewrite own_eq /own_def later_ownM. apply exist_elim=> r. assert (NonExpansive (λ r : iResUR Σ, r (inG_id Hin) !! γ)). { intros n r1 r2 Hr. f_equiv. by specialize (Hr (inG_id Hin)). } rewrite (f_equiv (λ r : iResUR Σ, r (inG_id Hin) !! γ) _ r). rewrite (f_equivI (λ r : iResUR Σ, r (inG_id Hin) !! γ) _ r). rewrite {1}/iRes_singleton discrete_fun_lookup_singleton lookup_singleton. rewrite option_equivI. case Hb: (r (inG_id _) !! γ)=> [b|]; last first. { by rewrite and_elim_r /bi_except_0 -or_intro_l. } ... ...
 ... ... @@ -62,7 +62,7 @@ Section saved_anything. assert (∀ z, G2 (G1 z) ≡ z) as help. { intros z. rewrite /G1 /G2 -oFunctor_map_compose -{2}[z]oFunctor_map_id. apply (ne_proper (oFunctor_map F)); split=>?; apply iProp_fold_unfold. } rewrite -{2}[x]help -{2}[y]help. by iApply f_equiv. rewrite -{2}[x]help -{2}[y]help. by iApply f_equivI. Qed. End saved_anything. ... ...
 ... ... @@ -113,7 +113,7 @@ Proof. rewrite -own_op own_valid auth_both_validI /=. iIntros "[_ [#HI #HvI]]". iDestruct "HI" as (I') "HI". rewrite gmap_equivI gmap_validI. iSpecialize ("HI" \$! i). iSpecialize ("HvI" \$! i). rewrite lookup_fmap lookup_op lookup_singleton bi.option_equivI. rewrite lookup_fmap lookup_op lookup_singleton option_equivI. case: (I !! i)=> [Q|] /=; [|case: (I' !! i)=> [Q'|] /=; by iExFalso]. iExists Q; iSplit; first done. iAssert (invariant_unfold Q ≡ invariant_unfold P)%I as "?". ... ... @@ -121,7 +121,7 @@ Proof. iRewrite "HI" in "HvI". rewrite uPred.option_validI agree_validI. iRewrite -"HvI" in "HI". by rewrite agree_idemp. } rewrite /invariant_unfold. by rewrite agree_equivI bi.later_equivI iProp_unfold_equivI. by rewrite agree_equivI later_equivI iProp_unfold_equivI. Qed. Lemma ownI_open i P : wsat ∗ ownI i P ∗ ownE {[i]} ⊢ wsat ∗ ▷ P ∗ ownD {[i]}. ... ...
 From iris.bi Require Export derived_laws_bi derived_laws_sbi big_op updates plainly embedding. From iris.bi Require Export derived_laws_bi derived_laws_sbi big_op. From iris.bi Require Export updates internal_eq plainly embedding. Set Default Proof Using "Type". Module Import bi. ... ...
 ... ... @@ -18,164 +18,9 @@ Notation "P ⊣⊢ Q" := (P ⊣⊢@{PROP} Q). Hint Resolve or_elim or_intro_l' or_intro_r' True_intro False_elim : core. Hint Resolve and_elim_l' and_elim_r' and_intro forall_intro : core. Global Instance internal_eq_proper (A : ofeT) : Proper ((≡) ==> (≡) ==> (⊣⊢)) (@bi_internal_eq PROP A) := ne_proper_2 _. Global Instance later_proper : Proper ((⊣⊢) ==> (⊣⊢)) (@bi_later PROP) := ne_proper _. (* Equality *) Hint Resolve internal_eq_refl : core. Hint Extern 100 (NonExpansive _) => solve_proper : core. Lemma equiv_internal_eq {A : ofeT} P (a b : A) : a ≡ b → P ⊢ a ≡ b. Proof. intros ->. auto. Qed. Lemma internal_eq_rewrite' {A : ofeT} a b (Ψ : A → PROP) P {HΨ : NonExpansive Ψ} : (P ⊢ a ≡ b) → (P ⊢ Ψ a) → P ⊢ Ψ b. Proof. intros Heq HΨa. rewrite -(idemp bi_and P) {1}Heq HΨa. apply impl_elim_l'. by apply internal_eq_rewrite. Qed. Lemma internal_eq_sym {A : ofeT} (a b : A) : a ≡ b ⊢ b ≡ a. Proof. apply (internal_eq_rewrite' a b (λ b, b ≡ a)%I); auto. Qed. Lemma internal_eq_iff P Q : P ≡ Q ⊢ P ↔ Q. Proof. apply (internal_eq_rewrite' P Q (λ Q, P ↔ Q))%I; auto using iff_refl. Qed. Lemma f_equiv {A B : ofeT} (f : A → B) `{!NonExpansive f} x y : x ≡ y ⊢ f x ≡ f y. Proof. apply (internal_eq_rewrite' x y (λ y, f x ≡ f y)%I); auto. Qed. Lemma f_equiv_contractive {A B : ofeT} (f : A → B) `{Hf : !Contractive f} x y : ▷ (x ≡ y) ⊢ f x ≡ f y. Proof. rewrite later_eq_2. move: Hf=>/contractive_alt [g [? Hfg]]. rewrite !Hfg. by apply f_equiv. Qed. Lemma prod_equivI {A B : ofeT} (x y : A * B) : x ≡ y ⊣⊢ x.1 ≡ y.1 ∧ x.2 ≡ y.2. Proof. apply (anti_symm _). - apply and_intro; apply f_equiv; apply _. - rewrite {3}(surjective_pairing x) {3}(surjective_pairing y). apply (internal_eq_rewrite' (x.1) (y.1) (λ a, (x.1,x.2) ≡ (a,y.2))%I); auto. apply (internal_eq_rewrite' (x.2) (y.2) (λ b, (x.1,x.2) ≡ (x.1,b))%I); auto. Qed. Lemma sum_equivI {A B : ofeT} (x y : A + B) : x ≡ y ⊣⊢ match x, y with | inl a, inl a' => a ≡ a' | inr b, inr b' => b ≡ b' | _, _ => False end. Proof. apply (anti_symm _). - apply (internal_eq_rewrite' x y (λ y, match x, y with | inl a, inl a' => a ≡ a' | inr b, inr b' => b ≡ b' | _, _ => False end)%I); auto. destruct x; auto. - destruct x as [a|b], y as [a'|b']; auto; apply f_equiv, _. Qed. Lemma option_equivI {A : ofeT} (x y : option A) : x ≡ y ⊣⊢ match x, y with | Some a, Some a' => a ≡ a' | None, None => True | _, _ => False end. Proof. apply (anti_symm _). - apply (internal_eq_rewrite' x y (λ y, match x, y with | Some a, Some a' => a ≡ a' | None, None => True | _, _ => False end)%I); auto. destruct x; auto. - destruct x as [a|], y as [a'|]; auto. apply f_equiv, _. Qed. Lemma sig_equivI {A : ofeT} (P : A → Prop) (x y : sig P) : `x ≡ `y ⊣⊢ x ≡ y. Proof. apply (anti_symm _). apply sig_eq. apply f_equiv, _. Qed. Section sigT_equivI. Import EqNotations. Lemma sigT_equivI {A : Type} {P : A → ofeT} (x y : sigT P) : x ≡ y ⊣⊢ ∃ eq : projT1 x = projT1 y, rew eq in projT2 x ≡ projT2 y. Proof. apply (anti_symm _). - apply (internal_eq_rewrite' x y (λ y, ∃ eq : projT1 x = projT1 y, rew eq in projT2 x ≡ projT2 y))%I; [| done | exact: (exist_intro' _ _ eq_refl) ]. move => n [a pa] [b pb] [/=]; intros -> => /= Hab. apply exist_ne => ?. by rewrite Hab. - apply exist_elim. move: x y => [a pa] [b pb] /=. intros ->; simpl. apply f_equiv, _. Qed. End sigT_equivI. Lemma discrete_fun_equivI {A} {B : A → ofeT} (f g : discrete_fun B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x. Proof. apply (anti_symm _); auto using fun_ext. apply (internal_eq_rewrite' f g (λ g, ∀ x : A, f x ≡ g x)%I); auto. intros n h h' Hh; apply forall_ne=> x; apply internal_eq_ne; auto. Qed. Lemma ofe_morO_equivI {A B : ofeT} (f g : A -n> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x. Proof. apply (anti_symm _). - apply (internal_eq_rewrite' f g (λ g, ∀ x : A, f x ≡ g x)%I); auto. - rewrite -(discrete_fun_equivI (ofe_mor_car _ _ f) (ofe_mor_car _ _ g)). set (h1 (f : A -n> B) := exist (λ f : A -d> B, NonExpansive (f : A → B)) f (ofe_mor_ne A B f)). set (h2 (f : sigO (λ f : A -d> B, NonExpansive (f : A → B))) := @OfeMor A B (`f) (proj2_sig f)). assert (∀ f, h2 (h1 f) = f) as Hh by (by intros []). assert (NonExpansive h2) by (intros ??? EQ; apply EQ). by rewrite -{2}[f]Hh -{2}[g]Hh -f_equiv -sig_equivI. Qed. Lemma pure_internal_eq {A : ofeT} (x y : A) : ⌜x ≡ y⌝ ⊢ x ≡ y. Proof. apply pure_elim'=> ->. apply internal_eq_refl. Qed. Lemma discrete_eq {A : ofeT} (a b : A) : Discrete a → a ≡ b ⊣⊢ ⌜a ≡ b⌝. Proof. intros. apply (anti_symm _); auto using discrete_eq_1, pure_internal_eq. Qed. Lemma absorbingly_internal_eq {A : ofeT} (x y : A) : (x ≡ y) ⊣⊢ x ≡ y. Proof. apply (anti_symm _), absorbingly_intro. apply wand_elim_r', (internal_eq_rewrite' x y (λ y, True -∗ x ≡ y)%I); auto. apply wand_intro_l, internal_eq_refl. Qed. Lemma persistently_internal_eq {A : ofeT} (a b : A) : (a ≡ b) ⊣⊢ a ≡ b. Proof. apply (anti_symm (⊢)). { by rewrite persistently_into_absorbingly absorbingly_internal_eq. } apply (internal_eq_rewrite' a b (λ b, (a ≡ b))%I); auto. rewrite -(internal_eq_refl emp%I a). apply persistently_emp_intro. Qed. Global Instance internal_eq_absorbing {A : ofeT} (x y : A) : Absorbing (PROP:=PROP) (x ≡ y). Proof. by rewrite /Absorbing absorbingly_internal_eq. Qed. Global Instance internal_eq_persistent {A : ofeT} (a b : A) : Persistent (PROP:=PROP) (a ≡ b). Proof. by intros; rewrite /Persistent persistently_internal_eq. Qed. (* Equality under a later. *) Lemma internal_eq_rewrite_contractive {A : ofeT} a b (Ψ : A → PROP) {HΨ : Contractive Ψ} : ▷ (a ≡ b) ⊢ Ψ a → Ψ b. Proof. rewrite f_equiv_contractive. apply (internal_eq_rewrite (Ψ a) (Ψ b) id _). Qed. Lemma internal_eq_rewrite_contractive' {A : ofeT} a b (Ψ : A → PROP) P {HΨ : Contractive Ψ} : (P ⊢ ▷ (a ≡ b)) → (P ⊢ Ψ a) → P ⊢ Ψ b. Proof. rewrite later_eq_2. move: HΨ=>/contractive_alt [g [? HΨ]]. rewrite !HΨ. by apply internal_eq_rewrite'. Qed. Lemma later_equivI {A : ofeT} (x y : A) : Next x ≡ Next y ⊣⊢ ▷ (x ≡ y). Proof. apply (anti_symm _); auto using later_eq_1, later_eq_2. Qed. Lemma later_equivI_prop_2 `{!Contractive (bi_later (PROP:=PROP))} P Q : ▷ (P ≡ Q) ⊢ (▷ P) ≡ (▷ Q). Proof. apply (f_equiv_contractive _). Qed. (* Later derived *) Hint Resolve later_mono : core. Global Instance later_mono' : Proper ((⊢) ==> (⊢)) (@bi_later PROP). ... ... @@ -489,9 +334,6 @@ Global Instance intuitionistically_timeless P : Timeless (PROP:=PROP) emp → Timeless P → Timeless (□ P). Proof. rewrite /bi_intuitionistically; apply _. Qed. Global Instance eq_timeless {A : ofeT} (a b : A) : Discrete a → Timeless (PROP:=PROP) (a ≡ b). Proof. intros. rewrite /Discrete !discrete_eq. apply (timeless _). Qed. Global Instance from_option_timeless {A} P (Ψ : A → PROP) (mx : option A) : (∀ x, Timeless (Ψ x)) → Timeless P → Timeless (from_option Ψ P mx). Proof. destruct mx; apply _. Qed. ... ...
 From iris.bi Require Import interface derived_laws_sbi big_op plainly updates. From iris.bi Require Import interface derived_laws_sbi big_op. From iris.bi Require Import plainly updates internal_eq. From iris.algebra Require Import monoid. Class Embed (A B : Type) := embed : A → B. ... ... @@ -16,6 +17,8 @@ Record BiEmbedMixin (PROP1 PROP2 : bi) `(Embed PROP1 PROP2) := { bi_embed_mixin_mono : Proper ((⊢) ==> (⊢)) (embed (A:=PROP1) (B:=PROP2)); bi_embed_mixin_emp_valid_inj (P : PROP1) : (⊢@{PROP2} ⎡P⎤) → ⊢ P; bi_embed_mixin_interal_inj `{BiInternalEq PROP'} (P Q : PROP1) : ⎡P⎤ ≡ ⎡Q⎤ ⊢@{PROP'} (P ≡ Q); bi_embed_mixin_emp_2 : emp ⊢@{PROP2} ⎡emp⎤; bi_embed_mixin_impl_2 (P Q : PROP1) : (⎡P⎤ → ⎡Q⎤) ⊢@{PROP2} ⎡P → Q⎤; ... ... @@ -39,38 +42,37 @@ Hint Mode BiEmbed ! - : typeclass_instances. Hint Mode BiEmbed - ! : typeclass_instances. Arguments bi_embed_embed : simpl never. Class BiEmbedEmp (PROP1 PROP2 : bi) `{BiEmbed PROP1 PROP2} := { embed_emp_1 : ⎡ emp : PROP1 ⎤ ⊢ emp; }. Class BiEmbedEmp (PROP1 PROP2 : bi) `{!BiEmbed PROP1 PROP2} := embed_emp_1 : ⎡ emp : PROP1 ⎤ ⊢ emp. Hint Mode BiEmbedEmp ! - - : typeclass_instances. Hint Mode BiEmbedEmp - ! - : typeclass_instances. Class SbiEmbed (PROP1 PROP2 : bi) `{BiEmbed PROP1 PROP2} := { embed_internal_eq_1 (A : ofeT) (x y : A) : ⎡x ≡ y⎤ ⊢@{PROP2} x ≡ y; embed_later P : ⎡▷ P⎤ ⊣⊢@{PROP2} ▷ ⎡P⎤; embed_interal_inj (PROP' : bi) (P Q : PROP1) : ⎡P⎤ ≡ ⎡Q⎤ ⊢@{PROP'} (P ≡ Q); }. Hint Mode SbiEmbed ! - - : typeclass_instances. Hint Mode SbiEmbed - ! - : typeclass_instances. Class BiEmbedLater (PROP1 PROP2 : bi) `{!BiEmbed PROP1 PROP2} := embed_later P : ⎡▷ P⎤ ⊣⊢@{PROP2} ▷ ⎡P⎤. Hint Mode BiEmbedLater ! - - : typeclass_instances. Hint Mode BiEmbedLater - ! - : typeclass_instances. Class BiEmbedInternalEq (PROP1 PROP2 : bi) `{!BiEmbed PROP1 PROP2, !BiInternalEq PROP1, !BiInternalEq PROP2} := embed_internal_eq_1 (A : ofeT) (x y : A) : ⎡x ≡ y⎤ ⊢@{PROP2} x ≡ y. Hint Mode BiEmbedInternalEq ! - - - - : typeclass_instances. Hint Mode BiEmbedInternalEq - ! - - - : typeclass_instances. Class BiEmbedBUpd (PROP1 PROP2 : bi) `{BiEmbed PROP1 PROP2, BiBUpd PROP1, BiBUpd PROP2} := { embed_bupd P : ⎡|==> P⎤ ⊣⊢@{PROP2} |==> ⎡P⎤ }. `{!BiEmbed PROP1 PROP2, !BiBUpd PROP1, !BiBUpd PROP2} := embed_bupd P : ⎡|==> P⎤ ⊣⊢@{PROP2} |==> ⎡P⎤. Hint Mode BiEmbedBUpd - ! - - - : typeclass_instances. Hint Mode BiEmbedBUpd ! - - - - : typeclass_instances. Class BiEmbedFUpd (PROP1 PROP2 : bi) `{BiEmbed PROP1 PROP2, BiFUpd PROP1, BiFUpd PROP2} := { embed_fupd E1 E2 P : ⎡|={E1,E2}=> P⎤ ⊣⊢@{PROP2} |={E1,E2}=> ⎡P⎤ }. `{!BiEmbed PROP1 PROP2, !BiFUpd PROP1, !BiFUpd PROP2} := embed_fupd E1 E2 P : ⎡|={E1,E2}=> P⎤ ⊣⊢@{PROP2} |={E1,E2}=> ⎡P⎤. Hint Mode BiEmbedFUpd - ! - - - : typeclass_instances. Hint Mode BiEmbedFUpd ! - - - - : typeclass_instances. Class BiEmbedPlainly (PROP1 PROP2 : bi) `{BiEmbed PROP1 PROP2, BiPlainly PROP1, BiPlainly PROP2} := { embed_plainly_2 (P : PROP1) : ■ ⎡P⎤ ⊢ (⎡■ P⎤ : PROP2) }. `{!BiEmbed PROP1 PROP2, !BiPlainly PROP1, !BiPlainly PROP2} := embed_plainly (P : PROP1) : ⎡■ P⎤ ⊣⊢@{PROP2} ■ ⎡P⎤. Hint Mode BiEmbedPlainly - ! - - - : typeclass_instances. Hint Mode BiEmbedPlainly ! - - - - : typeclass_instances. ... ... @@ -86,6 +88,9 @@ Section embed_laws. Proof. eapply bi_embed_mixin_mono, bi_embed_mixin. Qed. Lemma embed_emp_valid_inj P : (⊢@{PROP2} ⎡P⎤) → ⊢ P. Proof. eapply bi_embed_mixin_emp_valid_inj, bi_embed_mixin. Qed. Lemma embed_interal_inj `{!BiInternalEq PROP'} (P Q : PROP1) : ⎡P⎤ ≡ ⎡Q⎤ ⊢@{PROP'} (P ≡ Q). Proof. eapply bi_embed_mixin_interal_inj, bi_embed_mixin. Qed. Lemma embed_emp_2 : emp ⊢ ⎡emp⎤. Proof. eapply bi_embed_mixin_emp_2, bi_embed_mixin. Qed. Lemma embed_impl_2 P Q : (⎡P⎤ → ⎡Q⎤) ⊢ ⎡P → Q⎤. ... ... @@ -259,66 +264,43 @@ Section embed. ⎡[∗ mset] y ∈ X, Φ y⎤ ⊣⊢ [∗ mset] y ∈ X, ⎡Φ y⎤. Proof. apply (big_opMS_commute _). Qed. End big_ops_emp. End embed. Section sbi_embed. Context `{SbiEmbed PROP1 PROP2}. Implicit Types P Q R : PROP1. Section later. Context `{!BiEmbedLater PROP1 PROP2}. Lemma embed_internal_eq (A : ofeT) (x y : A) : ⎡x ≡ y⎤ ⊣⊢@{PROP2} x ≡ y. Proof. apply bi.equiv_spec; split; [apply embed_internal_eq_1|]. etrans; [apply (bi.internal_eq_rewrite x y (λ y, ⎡x ≡ y⎤%I)); solve_proper|]. rewrite -(bi.internal_eq_refl True%I) embed_pure. eapply bi.impl_elim; [done|]. apply bi.True_intro. Qed. Lemma embed_laterN n P : ⎡▷^n P⎤ ⊣⊢ ▷^n ⎡P⎤. Proof. induction n=>//=. rewrite embed_later. by f_equiv. Qed. Lemma embed_except_0 P : ⎡◇ P⎤ ⊣⊢ ◇ ⎡P⎤. Proof. by rewrite embed_or embed_later embed_pure. Qed.