From 45eb1be5f217ab6517b8191606dae62453e088d3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 13 May 2020 18:26:01 +0200
Subject: [PATCH] Use type class for internal equality.
---
_CoqProject | 1 +
tests/proofmode.v | 18 +-
tests/proofmode_monpred.v | 2 +-
theories/algebra/lib/excl_auth.v | 2 +-
theories/base_logic/bi.v | 49 +++--
theories/base_logic/lib/iprop.v | 2 +-
theories/base_logic/lib/own.v | 2 +-
theories/base_logic/lib/saved_prop.v | 2 +-
theories/base_logic/lib/wsat.v | 4 +-
theories/bi/bi.v | 4 +-
theories/bi/derived_laws_sbi.v | 158 ---------------
theories/bi/embedding.v | 130 ++++++------
theories/bi/interface.v | 118 +++--------
theories/bi/internal_eq.v | 240 +++++++++++++++++++++++
theories/bi/lib/relations.v | 18 +-
theories/bi/monpred.v | 179 +++++++++--------
theories/bi/plainly.v | 110 ++++++-----
theories/proofmode/class_instances_sbi.v | 70 ++++---
theories/proofmode/classes.v | 8 +-
theories/proofmode/coq_tactics.v | 4 +-
theories/proofmode/frame_instances.v | 5 +-
theories/proofmode/ltac_tactics.v | 2 +-
theories/proofmode/monpred.v | 6 +-
theories/si_logic/bi.v | 38 ++--
24 files changed, 615 insertions(+), 557 deletions(-)
create mode 100644 theories/bi/internal_eq.v
diff --git a/_CoqProject b/_CoqProject
index 2bb663e11..f01a9bc22 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -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
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 2df448f52..af8ebb1eb 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.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 -∗ <affine> (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) :
φ → <affine> ⌜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 : <affine> ▷ (Q ≡ P) -∗ <affine> ▷ Q -∗ <affine> ▷ P.
+Lemma test_iNext_iRewrite `{!BiInternalEq PROP} P Q :
+ <affine> ▷ (Q ≡ P) -∗ <affine> ▷ Q -∗ <affine> ▷ 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 : <affine> ▷ (Q ≡ P) -∗ <affine> ▷ Q -∗ <affine> ▷ P.
+Lemma test_iNext_affine `{!BiInternalEq PROP} P Q :
+ <affine> ▷ (Q ≡ P) -∗ <affine> ▷ Q -∗ <affine> ▷ 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 ∧
diff --git a/tests/proofmode_monpred.v b/tests/proofmode_monpred.v
index 24a606a68..b39d8ab7c 100644
--- a/tests/proofmode_monpred.v
+++ b/tests/proofmode_monpred.v
@@ -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.
diff --git a/theories/algebra/lib/excl_auth.v b/theories/algebra/lib/excl_auth.v
index 25a06edf1..5358d8dc1 100644
--- a/theories/algebra/lib/excl_auth.v
+++ b/theories/algebra/lib/excl_auth.v
@@ -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.
diff --git a/theories/base_logic/bi.v b/theories/base_logic/bi.v
index b225064ad..ebb60030c 100644
--- a/theories/base_logic/bi.v
+++ b/theories/base_logic/bi.v
@@ -1,4 +1,4 @@
-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.
diff --git a/theories/base_logic/lib/iprop.v b/theories/base_logic/lib/iprop.v
index 9566152db..214b72850 100644
--- a/theories/base_logic/lib/iprop.v
+++ b/theories/base_logic/lib/iprop.v
@@ -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.
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index f9dbb70ce..ce5889435 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -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. }
diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index d9cc45f05..ea836c510 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -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.
diff --git a/theories/base_logic/lib/wsat.v b/theories/base_logic/lib/wsat.v
index 0cc14c031..1846c8912 100644
--- a/theories/base_logic/lib/wsat.v
+++ b/theories/base_logic/lib/wsat.v
@@ -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]}.
diff --git a/theories/bi/bi.v b/theories/bi/bi.v
index 9e9de7dba..9fde00f1a 100644
--- a/theories/bi/bi.v
+++ b/theories/bi/bi.v
@@ -1,5 +1,5 @@
-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.
diff --git a/theories/bi/derived_laws_sbi.v b/theories/bi/derived_laws_sbi.v
index 16d86917b..19bafd7bf 100644
--- a/theories/bi/derived_laws_sbi.v
+++ b/theories/bi/derived_laws_sbi.v
@@ -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) : <absorb> (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) : <pers> (a ≡ b) ⊣⊢ a ≡ b.
-Proof.
- apply (anti_symm (⊢)).
- { by rewrite persistently_into_absorbingly absorbingly_internal_eq. }
- apply (internal_eq_rewrite' a b (λ b, <pers> (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.
diff --git a/theories/bi/embedding.v b/theories/bi/embedding.v
index f2bcbd6fb..176a12da7 100644
--- a/theories/bi/embedding.v
+++ b/theories/bi/embedding.v
@@ -1,4 +1,5 @@
-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.
-
- (* Not an instance, since it may cause overlap *)
- Lemma bi_embed_plainly_emp `{!BiPlainly PROP1, !BiPlainly PROP2} :
- BiEmbedEmp PROP1 PROP2 → BiEmbedPlainly PROP1 PROP2.
- Proof.
- intros. constructor=> P. rewrite !plainly_alt embed_internal_eq.
- by rewrite -embed_affinely -embed_emp embed_interal_inj.
- 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.
- Lemma embed_plainly_1 `{!BiPlainly PROP1, !BiPlainly PROP2} P : ⎡■P⎤ ⊢ ■⎡P⎤.
- Proof.
- assert (∀ P, <affine> ⎡ P ⎤ ⊣⊢ (<affine> ⎡ <affine> P ⎤ : PROP2)) as Hhelp.
- { intros P'. apply (anti_symm _).
- - by rewrite -bi.affinely_idemp (embed_affinely_2 P').
- - by rewrite (bi.affinely_elim P'). }
- assert (<affine> ⎡ emp ⎤ ⊣⊢ (emp : PROP2)) as Hemp.
- { apply (anti_symm _).
- - apply bi.affinely_elim_emp.
- - apply bi.and_intro; auto using embed_emp_2. }
- rewrite !plainly_alt embed_internal_eq. by rewrite Hhelp -Hemp -!bi.f_equiv.
- Qed.
- Lemma embed_plainly `{!BiPlainly PROP1, !BiPlainly PROP2,
- !BiEmbedPlainly PROP1 PROP2} P : ⎡■P⎤ ⊣⊢ ■⎡P⎤.
- Proof.
- apply (anti_symm _). by apply embed_plainly_1. by apply embed_plainly_2.
- Qed.
+ Global Instance embed_timeless P : Timeless P → Timeless ⎡P⎤.
+ Proof.
+ intros ?. by rewrite /Timeless -embed_except_0 -embed_later timeless.
+ Qed.
+ End later.
+
+ Section internal_eq.
+ Context `{!BiInternalEq PROP1, !BiInternalEq PROP2, !BiEmbedInternalEq PROP1 PROP2}.
- Lemma embed_plainly_if `{!BiPlainly PROP1, !BiPlainly PROP2,
- !BiEmbedPlainly PROP1 PROP2} p P : ⎡■?p P⎤ ⊣⊢ ■?p ⎡P⎤.
- Proof. destruct p; simpl; auto using embed_plainly. Qed.
- Lemma embed_plainly_if_1 `{!BiPlainly PROP1, !BiPlainly PROP2} p P :
- ⎡■?p P⎤ ⊢ ■?p ⎡P⎤.
- Proof. destruct p; simpl; auto using embed_plainly_1. Qed.
+ 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 (internal_eq_rewrite x y (λ y, ⎡x ≡ y⎤%I)); solve_proper|].
+ rewrite -(internal_eq_refl True%I) embed_pure.
+ eapply bi.impl_elim; [done|]. apply bi.True_intro.
+ Qed.
+ End internal_eq.
- Lemma embed_plain `{!BiPlainly PROP1, !BiPlainly PROP2} (P : PROP1) :
- Plain P → Plain (PROP:=PROP2) ⎡P⎤.
- Proof. intros ?. by rewrite /Plain {1}(plain P) embed_plainly_1. Qed.
+ Section plainly.
+ Context `{!BiPlainly PROP1, !BiPlainly PROP2, !BiEmbedPlainly PROP1 PROP2}.
- Global Instance embed_timeless P : Timeless P → Timeless ⎡P⎤.
- Proof.
- intros ?. by rewrite /Timeless -embed_except_0 -embed_later timeless.
- Qed.
-End sbi_embed.
+ Lemma embed_plainly_if p P : ⎡■?p P⎤ ⊣⊢ ■?p ⎡P⎤.
+ Proof. destruct p; simpl; auto using embed_plainly. Qed.
+
+ Lemma embed_plain (P : PROP1) : Plain P → Plain (PROP:=PROP2) ⎡P⎤.
+ Proof. intros ?. by rewrite /Plain {1}(plain P) embed_plainly. Qed.
+ End plainly.
+End embed.
(* Not defined using an ordinary [Instance] because the default
[class_apply @bi_embed_plainly] shelves the [BiPlainly] premise, making proof
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 0560df4d0..9c2e3d227 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -15,26 +15,23 @@ Section bi_mixin.
Context (bi_sep : PROP → PROP → PROP).
Context (bi_wand : PROP → PROP → PROP).
Context (bi_persistently : PROP → PROP).
- Context (sbi_internal_eq : ∀ A : ofeT, A → A → PROP).
- Context (sbi_later : PROP → PROP).
+ Local Bind Scope bi_scope with PROP.
Local Infix "⊢" := bi_entails.
- Local Notation "'emp'" := bi_emp.
- Local Notation "'True'" := (bi_pure True).
- Local Notation "'False'" := (bi_pure False).
- Local Notation "'⌜' φ 'âŒ'" := (bi_pure φ%type%stdpp).
- Local Infix "∧" := bi_and.
- Local Infix "∨" := bi_or.
- Local Infix "→" := bi_impl.
+ Local Notation "'emp'" := bi_emp : bi_scope.
+ Local Notation "'True'" := (bi_pure True) : bi_scope.
+ Local Notation "'False'" := (bi_pure False) : bi_scope.
+ Local Notation "'⌜' φ 'âŒ'" := (bi_pure φ%type%stdpp) : bi_scope.
+ Local Infix "∧" := bi_and : bi_scope.
+ Local Infix "∨" := bi_or : bi_scope.
+ Local Infix "→" := bi_impl : bi_scope.
Local Notation "∀ x .. y , P" :=
- (bi_forall _ (λ x, .. (bi_forall _ (λ y, P)) ..)).
+ (bi_forall _ (λ x, .. (bi_forall _ (λ y, P%I)) ..)) : bi_scope.
Local Notation "∃ x .. y , P" :=
- (bi_exist _ (λ x, .. (bi_exist _ (λ y, P)) ..)).
- Local Infix "∗" := bi_sep.
- Local Infix "-∗" := bi_wand.
- Local Notation "'<pers>' P" := (bi_persistently P).
- Local Notation "x ≡ y" := (sbi_internal_eq _ x y).
- Local Notation "â–· P" := (sbi_later P).
+ (bi_exist _ (λ x, .. (bi_exist _ (λ y, P%I)) ..)) : bi_scope.
+ Local Infix "∗" := bi_sep : bi_scope.
+ Local Infix "-∗" := bi_wand : bi_scope.
+ Local Notation "'<pers>' P" := (bi_persistently P) : bi_scope.
(** * Axioms for a general BI (logic of bunched implications) *)
@@ -49,7 +46,7 @@ Section bi_mixin.
Record BiMixin := {
bi_mixin_entails_po : PreOrder bi_entails;
- bi_mixin_equiv_spec P Q : equiv P Q ↔ (P ⊢ Q) ∧ (Q ⊢ P);
+ bi_mixin_equiv_spec P Q : (P ≡ Q) ↔ (P ⊢ Q) ∧ (Q ⊢ P);
(** Non-expansiveness *)
bi_mixin_pure_ne n : Proper (iff ==> dist n) bi_pure;
@@ -117,21 +114,11 @@ Section bi_mixin.
bi_mixin_persistently_and_sep_elim P Q : <pers> P ∧ Q ⊢ P ∗ Q;
}.
- Record SbiMixin := {
- bi_mixin_later_ne : NonExpansive sbi_later;
- bi_mixin_internal_eq_ne (A : ofeT) : NonExpansive2 (sbi_internal_eq A);
+ Context (bi_later : PROP → PROP).
+ Local Notation "â–· P" := (bi_later P) : bi_scope.
- (* Equality *)
- bi_mixin_internal_eq_refl {A : ofeT} P (a : A) : P ⊢ a ≡ a;
- bi_mixin_internal_eq_rewrite {A : ofeT} a b (Ψ : A → PROP) :
- NonExpansive Ψ → a ≡ b ⊢ Ψ a → Ψ b;
- bi_mixin_fun_ext {A} {B : A → ofeT} (f g : discrete_fun B) : (∀ x, f x ≡ g x) ⊢ f ≡ g;
- bi_mixin_sig_eq {A : ofeT} (P : A → Prop) (x y : sig P) : `x ≡ `y ⊢ x ≡ y;
- bi_mixin_discrete_eq_1 {A : ofeT} (a b : A) : Discrete a → a ≡ b ⊢ ⌜a ≡ bâŒ;
-
- (* Later *)
- bi_mixin_later_eq_1 {A : ofeT} (x y : A) : Next x ≡ Next y ⊢ ▷ (x ≡ y);
- bi_mixin_later_eq_2 {A : ofeT} (x y : A) : ▷ (x ≡ y) ⊢ Next x ≡ Next y;
+ Record BiLaterMixin := {
+ bi_mixin_later_ne : NonExpansive bi_later;
bi_mixin_later_mono P Q : (P ⊢ Q) → ▷ P ⊢ ▷ Q;
bi_mixin_later_intro P : P ⊢ ▷ P;
@@ -163,15 +150,13 @@ Structure bi := Bi {
bi_sep : bi_car → bi_car → bi_car;
bi_wand : bi_car → bi_car → bi_car;
bi_persistently : bi_car → bi_car;
- bi_internal_eq : ∀ A : ofeT, A → A → bi_car;
bi_later : bi_car → bi_car;
bi_ofe_mixin : OfeMixin bi_car;
bi_cofe : Cofe (OfeT bi_car bi_ofe_mixin);
bi_bi_mixin : BiMixin bi_entails bi_emp bi_pure bi_and bi_or bi_impl bi_forall
bi_exist bi_sep bi_wand bi_persistently;
- bi_sbi_mixin : SbiMixin bi_entails bi_pure bi_or bi_impl
- bi_forall bi_exist bi_sep
- bi_persistently bi_internal_eq bi_later;
+ bi_bi_later_mixin : BiLaterMixin bi_entails bi_pure bi_or bi_impl
+ bi_forall bi_exist bi_sep bi_persistently bi_later;
}.
Coercion bi_ofeO (PROP : bi) : ofeT := OfeT PROP (bi_ofe_mixin PROP).
@@ -191,7 +176,6 @@ Instance: Params (@bi_sep) 1 := {}.
Instance: Params (@bi_wand) 1 := {}.
Instance: Params (@bi_persistently) 1 := {}.
Instance: Params (@bi_later) 1 := {}.
-Instance: Params (@bi_internal_eq) 1 := {}.
Arguments bi_car : simpl never.
Arguments bi_dist : simpl never.
@@ -208,7 +192,6 @@ Arguments bi_sep {PROP} _%I _%I : simpl never, rename.
Arguments bi_wand {PROP} _%I _%I : simpl never, rename.
Arguments bi_persistently {PROP} _%I : simpl never, rename.
Arguments bi_later {PROP} _%I : simpl never, rename.
-Arguments bi_internal_eq {PROP _} _ _ : simpl never, rename.
Hint Extern 0 (bi_entails _ _) => reflexivity : core.
Instance bi_rewrite_relation (PROP : bi) : RewriteRelation (@bi_entails PROP) := {}.
@@ -246,13 +229,6 @@ Notation "∃ x .. y , P" :=
(bi_exist (λ x, .. (bi_exist (λ y, P)) ..)%I) : bi_scope.
Notation "'<pers>' P" := (bi_persistently P) : bi_scope.
-Infix "≡" := bi_internal_eq : bi_scope.
-Infix "≡@{ A }" := (bi_internal_eq (A := A)) (only parsing) : bi_scope.
-
-Notation "( X ≡.)" := (bi_internal_eq X) (only parsing) : bi_scope.
-Notation "(.≡ X )" := (λ Y, Y ≡ X)%I (only parsing) : bi_scope.
-Notation "(≡@{ A } )" := (bi_internal_eq (A:=A)) (only parsing) : bi_scope.
-
Notation "â–· P" := (bi_later P) : bi_scope.
Definition bi_emp_valid {PROP : bi} (P : PROP) : Prop := emp ⊢ P.
@@ -375,63 +351,31 @@ Lemma persistently_absorbing P Q : <pers> P ∗ Q ⊢ <pers> P.
Proof. eapply (bi_mixin_persistently_absorbing bi_entails), bi_bi_mixin. Qed.
Lemma persistently_and_sep_elim P Q : <pers> P ∧ Q ⊢ P ∗ Q.
Proof. eapply (bi_mixin_persistently_and_sep_elim bi_entails), bi_bi_mixin. Qed.
-End bi_laws.
-
-Section sbi_laws.
-Context {PROP : bi}.
-Implicit Types φ : Prop.
-Implicit Types P Q R : PROP.
-
-(* Equality *)
-Global Instance internal_eq_ne (A : ofeT) : NonExpansive2 (@bi_internal_eq PROP A).
-Proof. eapply bi_mixin_internal_eq_ne, bi_sbi_mixin. Qed.
-
-Lemma internal_eq_refl {A : ofeT} P (a : A) : P ⊢ a ≡ a.
-Proof. eapply bi_mixin_internal_eq_refl, bi_sbi_mixin. Qed.
-Lemma internal_eq_rewrite {A : ofeT} a b (Ψ : A → PROP) :
- NonExpansive Ψ → a ≡ b ⊢ Ψ a → Ψ b.
-Proof. eapply bi_mixin_internal_eq_rewrite, bi_sbi_mixin. Qed.
-
-Lemma fun_ext {A} {B : A → ofeT} (f g : discrete_fun B) :
- (∀ x, f x ≡ g x) ⊢@{PROP} f ≡ g.
-Proof. eapply bi_mixin_fun_ext, bi_sbi_mixin. Qed.
-Lemma sig_eq {A : ofeT} (P : A → Prop) (x y : sig P) :
- `x ≡ `y ⊢@{PROP} x ≡ y.
-Proof. eapply bi_mixin_sig_eq, bi_sbi_mixin. Qed.
-Lemma discrete_eq_1 {A : ofeT} (a b : A) :
- Discrete a → a ≡ b ⊢@{PROP} ⌜a ≡ bâŒ.
-Proof. eapply bi_mixin_discrete_eq_1, bi_sbi_mixin. Qed.
(* Later *)
Global Instance later_ne : NonExpansive (@bi_later PROP).
-Proof. eapply bi_mixin_later_ne, bi_sbi_mixin. Qed.
-
-Lemma later_eq_1 {A : ofeT} (x y : A) : Next x ≡ Next y ⊢@{PROP} ▷ (x ≡ y).
-Proof. eapply bi_mixin_later_eq_1, bi_sbi_mixin. Qed.
-Lemma later_eq_2 {A : ofeT} (x y : A) : ▷ (x ≡ y) ⊢@{PROP} Next x ≡ Next y.
-Proof. eapply bi_mixin_later_eq_2, bi_sbi_mixin. Qed.
+Proof. eapply bi_mixin_later_ne, bi_bi_later_mixin. Qed.
Lemma later_mono P Q : (P ⊢ Q) → ▷ P ⊢ ▷ Q.
-Proof. eapply bi_mixin_later_mono, bi_sbi_mixin. Qed.
+Proof. eapply bi_mixin_later_mono, bi_bi_later_mixin. Qed.
Lemma later_intro P : P ⊢ ▷ P.
-Proof. eapply bi_mixin_later_intro, bi_sbi_mixin. Qed.
+Proof. eapply bi_mixin_later_intro, bi_bi_later_mixin. Qed.
Lemma later_forall_2 {A} (Φ : A → PROP) : (∀ a, ▷ Φ a) ⊢ ▷ ∀ a, Φ a.
-Proof. eapply bi_mixin_later_forall_2, bi_sbi_mixin. Qed.
+Proof. eapply bi_mixin_later_forall_2, bi_bi_later_mixin. Qed.
Lemma later_exist_false {A} (Φ : A → PROP) :
(▷ ∃ a, Φ a) ⊢ ▷ False ∨ (∃ a, ▷ Φ a).
-Proof. eapply bi_mixin_later_exist_false, bi_sbi_mixin. Qed.
+Proof. eapply bi_mixin_later_exist_false, bi_bi_later_mixin. Qed.
Lemma later_sep_1 P Q : ▷ (P ∗ Q) ⊢ ▷ P ∗ ▷ Q.
-Proof. eapply bi_mixin_later_sep_1, bi_sbi_mixin. Qed.
+Proof. eapply bi_mixin_later_sep_1, bi_bi_later_mixin. Qed.
Lemma later_sep_2 P Q : ▷ P ∗ ▷ Q ⊢ ▷ (P ∗ Q).
-Proof. eapply bi_mixin_later_sep_2, bi_sbi_mixin. Qed.
+Proof. eapply bi_mixin_later_sep_2, bi_bi_later_mixin. Qed.
Lemma later_persistently_1 P : ▷ <pers> P ⊢ <pers> ▷ P.
-Proof. eapply (bi_mixin_later_persistently_1 bi_entails), bi_sbi_mixin. Qed.
+Proof. eapply (bi_mixin_later_persistently_1 bi_entails), bi_bi_later_mixin. Qed.
Lemma later_persistently_2 P : <pers> ▷ P ⊢ ▷ <pers> P.
-Proof. eapply (bi_mixin_later_persistently_2 bi_entails), bi_sbi_mixin. Qed.
+Proof. eapply (bi_mixin_later_persistently_2 bi_entails), bi_bi_later_mixin. Qed.
Lemma later_false_em P : ▷ P ⊢ ▷ False ∨ (▷ False → P).
-Proof. eapply bi_mixin_later_false_em, bi_sbi_mixin. Qed.
-End sbi_laws.
-
+Proof. eapply bi_mixin_later_false_em, bi_bi_later_mixin. Qed.
+End bi_laws.
End bi.
diff --git a/theories/bi/internal_eq.v b/theories/bi/internal_eq.v
new file mode 100644
index 000000000..62ce1bfd5
--- /dev/null
+++ b/theories/bi/internal_eq.v
@@ -0,0 +1,240 @@
+From iris.bi Require Import derived_laws_sbi big_op.
+Import interface.bi derived_laws_bi.bi derived_laws_sbi.bi.
+
+Class InternalEq (PROP : bi) :=
+ internal_eq : ∀ {A : ofeT}, A → A → PROP.
+Arguments internal_eq {_ _ _} _ _ : simpl never.
+Hint Mode InternalEq ! : typeclass_instances.
+Instance: Params (@internal_eq) 3 := {}.
+Infix "≡" := internal_eq : bi_scope.
+Infix "≡@{ A }" := (internal_eq (A := A)) (only parsing) : bi_scope.
+
+Notation "( X ≡.)" := (internal_eq X) (only parsing) : bi_scope.
+Notation "(.≡ X )" := (λ Y, Y ≡ X)%I (only parsing) : bi_scope.
+Notation "(≡@{ A } )" := (internal_eq (A:=A)) (only parsing) : bi_scope.
+
+(* Mixins allow us to create instances easily without having to use Program *)
+Record BiInternalEqMixin (PROP : bi) `(InternalEq PROP) := {
+ bi_internal_eq_mixin_internal_eq_ne (A : ofeT) : NonExpansive2 (@internal_eq PROP _ A);
+ bi_internal_eq_mixin_internal_eq_refl {A : ofeT} (P : PROP) (a : A) : P ⊢ a ≡ a;
+ bi_internal_eq_mixin_internal_eq_rewrite {A : ofeT} a b (Ψ : A → PROP) :
+ NonExpansive Ψ → a ≡ b ⊢ Ψ a → Ψ b;
+ bi_internal_eq_mixin_fun_extI {A} {B : A → ofeT} (f g : discrete_fun B) :
+ (∀ x, f x ≡ g x) ⊢@{PROP} f ≡ g;
+ bi_internal_eq_mixin_sig_equivI_1 {A : ofeT} (P : A → Prop) (x y : sig P) :
+ `x ≡ `y ⊢@{PROP} x ≡ y;
+ bi_internal_eq_mixin_discrete_eq_1 {A : ofeT} (a b : A) :
+ Discrete a → a ≡ b ⊢@{PROP} ⌜a ≡ bâŒ;
+ bi_internal_eq_mixin_later_equivI_1 {A : ofeT} (x y : A) :
+ Next x ≡ Next y ⊢@{PROP} ▷ (x ≡ y);
+ bi_internal_eq_mixin_later_equivI_2 {A : ofeT} (x y : A) :
+ ▷ (x ≡ y) ⊢@{PROP} Next x ≡ Next y;
+}.
+
+Class BiInternalEq (PROP : bi) := {
+ bi_internal_eq_internal_eq :> InternalEq PROP;
+ bi_internal_eq_mixin : BiInternalEqMixin PROP bi_internal_eq_internal_eq;
+}.
+Hint Mode BiInternalEq ! : typeclass_instances.
+Arguments bi_internal_eq_internal_eq : simpl never.
+
+Section internal_eq_laws.
+ Context `{BiInternalEq PROP}.
+ Implicit Types P Q : PROP.
+
+ Global Instance internal_eq_ne (A : ofeT) : NonExpansive2 (@internal_eq PROP _ A).
+ Proof. eapply bi_internal_eq_mixin_internal_eq_ne, (bi_internal_eq_mixin). Qed.
+
+ Lemma internal_eq_refl {A : ofeT} P (a : A) : P ⊢ a ≡ a.
+ Proof. eapply bi_internal_eq_mixin_internal_eq_refl, bi_internal_eq_mixin. Qed.
+ Lemma internal_eq_rewrite {A : ofeT} a b (Ψ : A → PROP) :
+ NonExpansive Ψ → a ≡ b ⊢ Ψ a → Ψ b.
+ Proof. eapply bi_internal_eq_mixin_internal_eq_rewrite, bi_internal_eq_mixin. Qed.
+
+ Lemma fun_extI {A} {B : A → ofeT} (f g : discrete_fun B) :
+ (∀ x, f x ≡ g x) ⊢@{PROP} f ≡ g.
+ Proof. eapply bi_internal_eq_mixin_fun_extI, bi_internal_eq_mixin. Qed.
+ Lemma sig_equivI_1 {A : ofeT} (P : A → Prop) (x y : sig P) :
+ `x ≡ `y ⊢@{PROP} x ≡ y.
+ Proof. eapply bi_internal_eq_mixin_sig_equivI_1, bi_internal_eq_mixin. Qed.
+ Lemma discrete_eq_1 {A : ofeT} (a b : A) :
+ Discrete a → a ≡ b ⊢@{PROP} ⌜a ≡ bâŒ.
+ Proof. eapply bi_internal_eq_mixin_discrete_eq_1, bi_internal_eq_mixin. Qed.
+
+ Lemma later_equivI_1 {A : ofeT} (x y : A) : Next x ≡ Next y ⊢@{PROP} ▷ (x ≡ y).
+ Proof. eapply bi_internal_eq_mixin_later_equivI_1, bi_internal_eq_mixin. Qed.
+ Lemma later_equivI_2 {A : ofeT} (x y : A) : ▷ (x ≡ y) ⊢@{PROP} Next x ≡ Next y.
+ Proof. eapply bi_internal_eq_mixin_later_equivI_2, bi_internal_eq_mixin. Qed.
+End internal_eq_laws.
+
+(* Derived laws *)
+Section internal_eq_derived.
+Context `{BiInternalEq PROP}.
+Implicit Types P : PROP.
+
+(* Force implicit argument PROP *)
+Notation "P ⊢ Q" := (P ⊢@{PROP} Q).
+Notation "P ⊣⊢ Q" := (P ⊣⊢@{PROP} Q).
+
+Global Instance internal_eq_proper (A : ofeT) :
+ Proper ((≡) ==> (≡) ==> (⊣⊢)) (@internal_eq PROP _ A) := ne_proper_2 _.
+
+(* Equality *)
+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.
+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_equivI {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_equivI_contractive {A B : ofeT} (f : A → B) `{Hf : !Contractive f} x y :
+ ▷ (x ≡ y) ⊢ f x ≡ f y.
+Proof.
+ rewrite later_equivI_2. move: Hf=>/contractive_alt [g [? Hfg]]. rewrite !Hfg.
+ by apply f_equivI.
+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_equivI; 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_equivI, _.
+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_equivI, _.
+Qed.
+
+Lemma sig_equivI {A : ofeT} (P : A → Prop) (x y : sig P) : `x ≡ `y ⊣⊢ x ≡ y.
+Proof. apply (anti_symm _). apply sig_equivI_1. apply f_equivI, _. 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_equivI, _.
+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_extI.
+ 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_equivI -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) : <absorb> (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) : <pers> (a ≡ b) ⊣⊢ a ≡ b.
+Proof.
+ apply (anti_symm (⊢)).
+ { by rewrite persistently_into_absorbingly absorbingly_internal_eq. }
+ apply (internal_eq_rewrite' a b (λ b, <pers> (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_equivI_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_equivI_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_equivI_1, later_equivI_2. Qed.
+Lemma later_equivI_prop_2 `{!Contractive (bi_later (PROP:=PROP))} P Q :
+ ▷ (P ≡ Q) ⊢ (▷ P) ≡ (▷ Q).
+Proof. apply (f_equivI_contractive _). 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.
+End internal_eq_derived.
diff --git a/theories/bi/lib/relations.v b/theories/bi/lib/relations.v
index 16b865e48..a42b93d8b 100644
--- a/theories/bi/lib/relations.v
+++ b/theories/bi/lib/relations.v
@@ -3,13 +3,13 @@ its reflexive transitive closure. *)
From iris.bi.lib Require Export fixpoint.
From iris.proofmode Require Import tactics.
-Definition bi_rtc_pre
- {PROP : bi} {A : ofeT} (R : A → A → PROP)
+Definition bi_rtc_pre `{!BiInternalEq PROP}
+ {A : ofeT} (R : A → A → PROP)
(x2 : A) (rec : A → PROP) (x1 : A) : PROP :=
(<affine> (x1 ≡ x2) ∨ ∃ x', R x1 x' ∗ rec x')%I.
-Instance bi_rtc_pre_mono
- {PROP : bi} {A : ofeT} (R : A → A → PROP) `{NonExpansive2 R} (x : A) :
+Instance bi_rtc_pre_mono `{!BiInternalEq PROP}
+ {A : ofeT} (R : A → A → PROP) `{NonExpansive2 R} (x : A) :
BiMonoPred (bi_rtc_pre R x).
Proof.
constructor; [|solve_proper].
@@ -20,26 +20,26 @@ Proof.
iDestruct ("H" with "Hrec") as "Hrec". eauto with iFrame.
Qed.
-Definition bi_rtc {PROP : bi} {A : ofeT} (R : A → A → PROP) (x1 x2 : A) : PROP :=
+Definition bi_rtc `{!BiInternalEq PROP}
+ {A : ofeT} (R : A → A → PROP) (x1 x2 : A) : PROP :=
bi_least_fixpoint (bi_rtc_pre R x2) x1.
Instance: Params (@bi_rtc) 3 := {}.
Typeclasses Opaque bi_rtc.
-Instance bi_rtc_ne {PROP : bi} {A : ofeT} (R : A → A → PROP) :
+Instance bi_rtc_ne `{!BiInternalEq PROP} {A : ofeT} (R : A → A → PROP) :
NonExpansive2 (bi_rtc R).
Proof.
intros n x1 x2 Hx y1 y2 Hy. rewrite /bi_rtc Hx. f_equiv=> rec z.
solve_proper.
Qed.
-Instance bi_rtc_proper
- {PROP : bi} {A : ofeT} (R : A → A → PROP)
+Instance bi_rtc_proper `{!BiInternalEq PROP} {A : ofeT} (R : A → A → PROP)
: Proper ((≡) ==> (≡) ==> (⊣⊢)) (bi_rtc R).
Proof. apply ne_proper_2. apply _. Qed.
Section bi_rtc.
- Context {PROP : bi}.
+ Context `{!BiInternalEq PROP}.
Context {A : ofeT}.
Context (R : A → A → PROP) `{NonExpansive2 R}.
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index 30252b28e..d6890ecbf 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -210,44 +210,30 @@ Next Obligation. solve_proper. Qed.
Definition monPred_in_aux : seal (@monPred_in_def). Proof. by eexists. Qed.
Definition monPred_in := monPred_in_aux.(unseal).
Definition monPred_in_eq : @monPred_in = _ := monPred_in_aux.(seal_eq).
-End Bi.
-
-Arguments monPred_objectively {_ _} _%I.
-Arguments monPred_subjectively {_ _} _%I.
-Notation "'<obj>' P" := (monPred_objectively P) : bi_scope.
-Notation "'<subj>' P" := (monPred_subjectively P) : bi_scope.
-
-Section Sbi.
-Context {I : biIndex} {PROP : bi}.
-Implicit Types i : I.
-Notation monPred := (monPred I PROP).
-Implicit Types P Q : monPred.
-
-Definition monPred_internal_eq_def (A : ofeT) (a b : A) : monPred :=
- MonPred (λ _, a ≡ b)%I _.
-Definition monPred_internal_eq_aux : seal (@monPred_internal_eq_def). Proof. by eexists. Qed.
-Definition monPred_internal_eq := monPred_internal_eq_aux.(unseal).
-Definition monPred_internal_eq_eq : @monPred_internal_eq = _ :=
- monPred_internal_eq_aux.(seal_eq).
Program Definition monPred_later_def P : monPred := MonPred (λ i, ▷ (P i))%I _.
Next Obligation. solve_proper. Qed.
Definition monPred_later_aux : seal monPred_later_def. Proof. by eexists. Qed.
Definition monPred_later := monPred_later_aux.(unseal).
Definition monPred_later_eq : monPred_later = _ := monPred_later_aux.(seal_eq).
-End Sbi.
+End Bi.
+
+Arguments monPred_objectively {_ _} _%I.
+Arguments monPred_subjectively {_ _} _%I.
+Notation "'<obj>' P" := (monPred_objectively P) : bi_scope.
+Notation "'<subj>' P" := (monPred_subjectively P) : bi_scope.
Module MonPred.
Definition unseal_eqs :=
(@monPred_and_eq, @monPred_or_eq, @monPred_impl_eq,
@monPred_forall_eq, @monPred_exist_eq, @monPred_sep_eq, @monPred_wand_eq,
- @monPred_persistently_eq, @monPred_later_eq, @monPred_internal_eq_eq, @monPred_in_eq,
+ @monPred_persistently_eq, @monPred_later_eq, @monPred_in_eq,
@monPred_embed_eq, @monPred_emp_eq, @monPred_pure_eq,
@monPred_objectively_eq, @monPred_subjectively_eq).
Ltac unseal :=
unfold bi_affinely, bi_absorbingly, bi_except_0, bi_pure, bi_emp,
monPred_upclosed, bi_and, bi_or,
- bi_impl, bi_forall, bi_exist, bi_internal_eq, bi_sep, bi_wand,
+ bi_impl, bi_forall, bi_exist, bi_sep, bi_wand,
bi_persistently, bi_affinely, bi_later;
simpl;
rewrite !unseal_eqs /=.
@@ -307,23 +293,13 @@ Proof.
- intros P Q. split=> i. by apply bi.persistently_and_sep_elim.
Qed.
-Lemma monPred_sbi_mixin :
- SbiMixin (PROP:=monPred I PROP) monPred_entails monPred_pure
- monPred_or monPred_impl monPred_forall monPred_exist
- monPred_sep monPred_persistently monPred_internal_eq monPred_later.
+Lemma monPred_bi_later_mixin :
+ BiLaterMixin (PROP:=monPred I PROP) monPred_entails monPred_pure
+ monPred_or monPred_impl monPred_forall monPred_exist
+ monPred_sep monPred_persistently monPred_later.
Proof.
split; unseal.
- by split=> ? /=; repeat f_equiv.
- - by split=> ? /=; repeat f_equiv.
- - intros A P a. split=> i. by apply bi.internal_eq_refl.
- - intros A a b Ψ ?. split=> i /=.
- setoid_rewrite bi.pure_impl_forall. do 2 apply bi.forall_intro => ?.
- erewrite (bi.internal_eq_rewrite _ _ (flip Ψ _)) => //=. solve_proper.
- - intros A1 A2 f g. split=> i. by apply bi.fun_ext.
- - intros A P x y. split=> i. by apply bi.sig_eq.
- - intros A a b ?. split=> i. by apply bi.discrete_eq_1.
- - intros A x y. split=> i. by apply bi.later_eq_1.
- - intros A x y. split=> i. by apply bi.later_eq_2.
- intros P Q [?]. split=> i. by apply bi.later_mono.
- intros P. split=> i /=. by apply bi.later_intro.
- intros A Ψ. split=> i. by apply bi.later_forall_2.
@@ -338,7 +314,7 @@ Qed.
Canonical Structure monPredI : bi :=
{| bi_ofe_mixin := monPred_ofe_mixin; bi_bi_mixin := monPred_bi_mixin;
- bi_sbi_mixin := monPred_sbi_mixin |}.
+ bi_bi_later_mixin := monPred_bi_later_mixin |}.
End canonical.
Class Objective {I : biIndex} {PROP : bi} (P : monPred I PROP) :=
@@ -460,6 +436,10 @@ Definition monPred_embedding_mixin : BiEmbedMixin PROP monPredI monPred_embed.
Proof.
split; try apply _; rewrite /bi_emp_valid; unseal; try done.
- move=> P /= [/(_ inhabitant) ?] //.
+ - intros PROP' ? P Q.
+ set (f P := monPred_at P inhabitant).
+ assert (NonExpansive f) by solve_proper.
+ apply (f_equivI f).
- intros P Q. split=> i /=.
by rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim.
- intros P Q. split=> i /=.
@@ -790,15 +770,11 @@ Proof. intros ??. by rewrite !monPred_at_bupd objective_at. Qed.
Global Instance monPred_bi_embed_bupd `{BiBUpd PROP} :
BiEmbedBUpd PROP monPredI.
-Proof. split. split=>i /=. by rewrite monPred_at_bupd !monPred_at_embed. Qed.
-End bi_facts.
+Proof. split=>i /=. by rewrite monPred_at_bupd !monPred_at_embed. Qed.
-Section sbi_facts.
-Context {I : biIndex} {PROP : bi}.
-Local Notation monPred := (monPred I PROP).
-Local Notation monPredI := (monPredI I PROP).
-Implicit Types i : I.
-Implicit Types P Q : monPred.
+(** Later *)
+Global Instance monPred_bi_embed_later : BiEmbedLater PROP monPredI.
+Proof. split; by unseal. Qed.
Global Instance monPred_at_timeless P i : Timeless P → Timeless (P i).
Proof. move => [] /(_ i). unfold Timeless. by unseal. Qed.
@@ -815,19 +791,6 @@ Proof.
by apply timeless, bi.exist_timeless.
Qed.
-Global Instance monPred_sbi_embed : SbiEmbed PROP monPredI.
-Proof.
- split; unseal=> //. intros ? P Q.
- apply (@bi.f_equiv _ _ _ (λ P, monPred_at P inhabitant)); solve_proper.
-Qed.
-
-Lemma monPred_internal_eq_unfold : @bi_internal_eq monPredI = λ A x y, ⎡ x ≡ y ⎤%I.
-Proof. by unseal. Qed.
-
-(** Unfolding lemmas *)
-Lemma monPred_at_internal_eq {A : ofeT} i (a b : A) :
- @monPred_at I PROP (a ≡ b) i ⊣⊢ a ≡ b.
-Proof. rewrite monPred_internal_eq_unfold. by apply monPred_at_embed. Qed.
Lemma monPred_at_later i P : (▷ P) i ⊣⊢ ▷ P i.
Proof. by unseal. Qed.
Lemma monPred_at_laterN n i P : (▷^n P) i ⊣⊢ ▷^n P i.
@@ -835,26 +798,64 @@ Proof. induction n; first done. rewrite /= monPred_at_later IHn //. Qed.
Lemma monPred_at_except_0 i P : (◇ P) i ⊣⊢ ◇ P i.
Proof. by unseal. Qed.
-Lemma monPred_equivI {PROP' : bi} P Q :
+Global Instance later_objective P `{!Objective P} : Objective (â–· P).
+Proof. intros ??. unseal. by rewrite objective_at. Qed.
+Global Instance laterN_objective P `{!Objective P} n : Objective (â–·^n P).
+Proof. induction n; apply _. Qed.
+Global Instance except0_objective P `{!Objective P} : Objective (â—‡ P).
+Proof. rewrite /bi_except_0. apply _. Qed.
+
+(** Internal equality *)
+Definition monPred_internal_eq_def `{!BiInternalEq PROP} (A : ofeT) (a b : A) : monPred :=
+ MonPred (λ _, a ≡ b)%I _.
+Definition monPred_internal_eq_aux `{!BiInternalEq PROP} : seal (@monPred_internal_eq_def _).
+Proof. by eexists. Qed.
+Definition monPred_internal_eq `{!BiInternalEq PROP} := monPred_internal_eq_aux.(unseal).
+Definition monPred_internal_eq_eq `{!BiInternalEq PROP} :
+ @internal_eq _ (@monPred_internal_eq _) = _ := monPred_internal_eq_aux.(seal_eq).
+
+Lemma monPred_internal_eq_mixin `{!BiInternalEq PROP} :
+ BiInternalEqMixin monPredI (@monPred_internal_eq _).
+Proof.
+ split; rewrite monPred_internal_eq_eq.
+ - split=> i /=. solve_proper.
+ - intros A P a. split=> i /=. apply internal_eq_refl.
+ - intros A a b Ψ ?. split=> i /=. unseal.
+ setoid_rewrite bi.pure_impl_forall. do 2 apply bi.forall_intro => ?.
+ erewrite (internal_eq_rewrite _ _ (flip Ψ _)) => //=. solve_proper.
+ - intros A1 A2 f g. split=> i /=. unseal. by apply fun_extI.
+ - intros A P x y. split=> i /=. by apply sig_equivI_1.
+ - intros A a b ?. split=> i /=. unseal. by apply discrete_eq_1.
+ - intros A x y. split=> i /=. unseal. by apply later_equivI_1.
+ - intros A x y. split=> i /=. unseal. by apply later_equivI_2.
+Qed.
+Global Instance monPred_bi_internal_eq `{BiInternalEq PROP} : BiInternalEq monPredI :=
+ {| bi_internal_eq_mixin := monPred_internal_eq_mixin |}.
+
+Global Instance monPred_bi_embed_internal_eq `{BiInternalEq PROP} :
+ BiEmbedInternalEq PROP monPredI.
+Proof. split=> i. rewrite monPred_internal_eq_eq. by unseal. Qed.
+
+Lemma monPred_internal_eq_unfold `{!BiInternalEq PROP} :
+ @internal_eq monPredI _ = λ A x y, ⎡ x ≡ y ⎤%I.
+Proof. rewrite monPred_internal_eq_eq. by unseal. Qed.
+
+Lemma monPred_at_internal_eq `{!BiInternalEq PROP} {A : ofeT} i (a b : A) :
+ @monPred_at (a ≡ b) i ⊣⊢ a ≡ b.
+Proof. rewrite monPred_internal_eq_unfold. by apply monPred_at_embed. Qed.
+
+Lemma monPred_equivI `{!BiInternalEq PROP'} P Q :
P ≡ Q ⊣⊢@{PROP'} ∀ i, P i ≡ Q i.
Proof.
apply bi.equiv_spec. split.
- - apply bi.forall_intro=>?. apply (bi.f_equiv (flip monPred_at _)).
+ - apply bi.forall_intro=> ?. apply (f_equivI (flip monPred_at _)).
- by rewrite -{2}(sig_monPred_sig P) -{2}(sig_monPred_sig Q)
- -bi.f_equiv -bi.sig_equivI !bi.discrete_fun_equivI.
+ -f_equivI -sig_equivI !discrete_fun_equivI.
Qed.
-(** Objective *)
-Global Instance internal_eq_objective {A : ofeT} (x y : A) :
+Global Instance internal_eq_objective `{!BiInternalEq PROP} {A : ofeT} (x y : A) :
@Objective I PROP (x ≡ y).
-Proof. intros ??. by unseal. Qed.
-
-Global Instance later_objective P `{!Objective P} : Objective (â–· P).
-Proof. intros ??. unseal. by rewrite objective_at. Qed.
-Global Instance laterN_objective P `{!Objective P} n : Objective (â–·^n P).
-Proof. induction n; apply _. Qed.
-Global Instance except0_objective P `{!Objective P} : Objective (â—‡ P).
-Proof. rewrite /bi_except_0. apply _. Qed.
+Proof. intros ??. rewrite monPred_internal_eq_unfold. by unseal. Qed.
(** FUpd *)
Program Definition monPred_fupd_def `{BiFUpd PROP} (E1 E2 : coPset)
@@ -885,7 +886,7 @@ Proof.
intros E P. split=>/= i. rewrite monPred_at_bupd monPred_fupd_eq bupd_fupd //=.
Qed.
Global Instance monPred_bi_embed_fupd `{BiFUpd PROP} : BiEmbedFUpd PROP monPredI.
-Proof. split. split=>i /=. by rewrite monPred_fupd_eq /= !monPred_at_embed. Qed.
+Proof. split=>i /=. by rewrite monPred_fupd_eq /= !monPred_at_embed. Qed.
Lemma monPred_at_fupd `{BiFUpd PROP} i E1 E2 P :
(|={E1,E2}=> P) i ⊣⊢ |={E1,E2}=> P i.
@@ -923,8 +924,6 @@ Proof.
do 3 apply bi.forall_intro => ?. f_equiv. rewrite bi.forall_elim //.
- intros P. split=> i /=. apply bi.forall_intro=>_. by apply plainly_emp_intro.
- intros P Q. split=> i. apply bi.sep_elim_l, _.
- - intros P Q. split=> i /=. rewrite (monPred_equivI P Q). f_equiv=> j.
- by rewrite prop_ext !(bi.forall_elim j) !bi.pure_True // !bi.True_impl.
- intros P. split=> i /=.
rewrite bi.later_forall. f_equiv=> j. by rewrite -later_plainly_1.
- intros P. split=> i /=.
@@ -933,29 +932,41 @@ Qed.
Global Instance monPred_bi_plainly `{BiPlainly PROP} : BiPlainly monPredI :=
{| bi_plainly_mixin := monPred_plainly_mixin |}.
-Global Instance monPred_bi_plainly_exist `{BiPlainly PROP} `{@BiIndexBottom I bot} :
+Global Instance monPred_bi_prop_ext
+ `{!BiPlainly PROP, !BiInternalEq PROP, !BiPropExt PROP} : BiPropExt monPredI.
+Proof.
+ intros P Q. split=> i /=. rewrite monPred_plainly_eq monPred_internal_eq_eq /=.
+ rewrite /bi_wand_iff monPred_equivI. f_equiv=> j. unseal.
+ by rewrite prop_ext !(bi.forall_elim j) !bi.pure_True // !bi.True_impl.
+Qed.
+
+Global Instance monPred_bi_plainly_exist `{!BiPlainly PROP} `{!BiIndexBottom bot} :
BiPlainlyExist PROP → BiPlainlyExist monPredI.
Proof.
- split=>?/=. rewrite monPred_plainly_eq /=. repeat setoid_rewrite monPred_at_exist.
+ split=> ? /=. rewrite monPred_plainly_eq /=. repeat setoid_rewrite monPred_at_exist.
rewrite (bi.forall_elim bot) plainly_exist_1. do 2 f_equiv.
apply bi.forall_intro=>?. by do 2 f_equiv.
Qed.
Global Instance monPred_bi_embed_plainly `{BiPlainly PROP} :
BiEmbedPlainly PROP monPredI.
-Proof. apply bi_embed_plainly_emp, _. Qed.
-
-Lemma monPred_plainly_unfold `{BiPlainly PROP} : plainly = λ P, ⎡ ∀ i, ■(P i) ⎤%I.
-Proof. by rewrite monPred_plainly_eq monPred_embed_eq. Qed.
-Lemma monPred_at_plainly `{BiPlainly PROP} i P : (■P) i ⊣⊢ ∀ j, ■(P j).
-Proof. by rewrite monPred_plainly_eq. Qed.
+Proof.
+ split=> i. rewrite monPred_plainly_eq; unseal. apply (anti_symm _).
+ - by apply bi.forall_intro.
+ - by rewrite (bi.forall_elim inhabitant).
+Qed.
Global Instance monPred_bi_bupd_plainly `{BiBUpdPlainly PROP} : BiBUpdPlainly monPredI.
Proof.
intros P. split=> /= i.
- rewrite monPred_at_bupd monPred_at_plainly bi.forall_elim. apply bupd_plainly.
+ rewrite monPred_at_bupd monPred_plainly_eq /= bi.forall_elim. apply bupd_plainly.
Qed.
+Lemma monPred_plainly_unfold `{BiPlainly PROP} : plainly = λ P, ⎡ ∀ i, ■(P i) ⎤%I.
+Proof. by rewrite monPred_plainly_eq monPred_embed_eq. Qed.
+Lemma monPred_at_plainly `{BiPlainly PROP} i P : (■P) i ⊣⊢ ∀ j, ■(P j).
+Proof. by rewrite monPred_plainly_eq. Qed.
+
Global Instance monPred_at_plain `{BiPlainly PROP} P i : Plain P → Plain (P i).
Proof. move => [] /(_ i). rewrite /Plain monPred_at_plainly bi.forall_elim //. Qed.
@@ -984,4 +995,4 @@ Global Instance monPred_objectively_plain `{BiPlainly PROP} P : Plain P → Plai
Proof. rewrite monPred_objectively_unfold. apply _. Qed.
Global Instance monPred_subjectively_plain `{BiPlainly PROP} P : Plain P → Plain (<subj> P).
Proof. rewrite monPred_subjectively_unfold. apply _. Qed.
-End sbi_facts.
+End bi_facts.
diff --git a/theories/bi/plainly.v b/theories/bi/plainly.v
index e501adc71..f99e4b68a 100644
--- a/theories/bi/plainly.v
+++ b/theories/bi/plainly.v
@@ -1,4 +1,4 @@
-From iris.bi Require Import derived_laws_sbi big_op.
+From iris.bi Require Import derived_laws_sbi big_op internal_eq.
From iris.algebra Require Import monoid.
Import interface.bi derived_laws_bi.bi derived_laws_sbi.bi.
@@ -29,8 +29,6 @@ Record BiPlainlyMixin (PROP : bi) `(Plainly PROP) := {
bi_plainly_mixin_plainly_emp_intro (P : PROP) : P ⊢ ■emp;
bi_plainly_mixin_plainly_absorb (P Q : PROP) : ■P ∗ Q ⊢ ■P;
- bi_plainly_mixin_prop_ext_2 (P Q : PROP) : ■((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q;
-
bi_plainly_mixin_later_plainly_1 (P : PROP) : ▷ ■P ⊢ ■▷ P;
bi_plainly_mixin_later_plainly_2 (P : PROP) : ■▷ P ⊢ ▷ ■P;
}.
@@ -50,6 +48,13 @@ Arguments BiPlainlyExist _ {_}.
Arguments plainly_exist_1 _ {_ _} _.
Hint Mode BiPlainlyExist ! - : typeclass_instances.
+Class BiPropExt `{!BiPlainly PROP, !BiInternalEq PROP} :=
+ prop_ext_2 (P Q : PROP) : ■(P ∗-∗ Q) ⊢ P ≡ Q.
+Arguments BiPropExt : clear implicits.
+Arguments BiPropExt _ {_ _}.
+Arguments prop_ext_2 _ {_ _ _} _.
+Hint Mode BiPropExt ! - - : typeclass_instances.
+
Section plainly_laws.
Context `{BiPlainly PROP}.
Implicit Types P Q : PROP.
@@ -74,9 +79,6 @@ Section plainly_laws.
Lemma plainly_emp_intro P : P ⊢ ■emp.
Proof. eapply bi_plainly_mixin_plainly_emp_intro, bi_plainly_mixin. Qed.
- Lemma prop_ext_2 P Q : ■((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q.
- Proof. eapply bi_plainly_mixin_prop_ext_2, bi_plainly_mixin. Qed.
-
Lemma later_plainly_1 P : ▷ ■P ⊢ ■(▷ P).
Proof. eapply bi_plainly_mixin_later_plainly_1, bi_plainly_mixin. Qed.
Lemma later_plainly_2 P : ■▷ P ⊢ ▷ ■P.
@@ -540,50 +542,62 @@ Global Instance big_sepMS_plain `{BiAffine PROP, Countable A} (Φ : A → PROP)
Proof. rewrite big_opMS_eq. apply _. Qed.
(* Interaction with equality *)
-Lemma plainly_internal_eq {A:ofeT} (a b : A) : ■(a ≡ b) ⊣⊢@{PROP} a ≡ b.
-Proof.
- apply (anti_symm (⊢)).
- { by rewrite plainly_elim. }
- apply (internal_eq_rewrite' a b (λ b, ■(a ≡ b))%I); [solve_proper|done|].
- rewrite -(internal_eq_refl True%I a) plainly_pure; auto.
-Qed.
+Section internal_eq.
+ Context `{!BiInternalEq PROP}.
-Lemma prop_ext P Q : P ≡ Q ⊣⊢ ■(P ∗-∗ Q).
-Proof.
- apply (anti_symm (⊢)); last exact: prop_ext_2.
- apply (internal_eq_rewrite' P Q (λ Q, ■(P ∗-∗ Q))%I);
- [ solve_proper | done | ].
- rewrite (plainly_emp_intro (P ≡ Q)%I).
- apply plainly_mono, wand_iff_refl.
-Qed.
+ Lemma plainly_internal_eq {A:ofeT} (a b : A) : ■(a ≡ b) ⊣⊢@{PROP} a ≡ b.
+ Proof.
+ apply (anti_symm (⊢)).
+ { by rewrite plainly_elim. }
+ apply (internal_eq_rewrite' a b (λ b, ■(a ≡ b))%I); [solve_proper|done|].
+ rewrite -(internal_eq_refl True%I a) plainly_pure; auto.
+ Qed.
-Lemma plainly_alt P : ■P ⊣⊢ <affine> P ≡ emp.
-Proof.
- rewrite -plainly_affinely_elim. 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 _ _ plainly).
- by rewrite -plainly_True_emp plainly_pure True_impl.
-Qed.
+ Global Instance internal_eq_plain {A : ofeT} (a b : A) :
+ Plain (PROP:=PROP) (a ≡ b).
+ Proof. by intros; rewrite /Plain plainly_internal_eq. Qed.
+End internal_eq.
-Lemma plainly_alt_absorbing P `{!Absorbing P} : ■P ⊣⊢ P ≡ True.
-Proof.
- apply (anti_symm (⊢)).
- - rewrite prop_ext. apply plainly_mono, and_intro; apply wand_intro_l; auto.
- - rewrite internal_eq_sym (internal_eq_rewrite _ _ plainly).
- by rewrite plainly_pure True_impl.
-Qed.
+Section prop_ext.
+ Context `{!BiInternalEq PROP, !BiPropExt PROP}.
-Lemma plainly_True_alt P : ■(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, ■(True -∗ Q))%I ltac:(shelve)); last solve_proper.
- by rewrite -entails_wand // -(plainly_emp_intro True%I) True_impl.
-Qed.
+ Lemma prop_ext P Q : P ≡ Q ⊣⊢ ■(P ∗-∗ Q).
+ Proof.
+ apply (anti_symm (⊢)); last exact: prop_ext_2.
+ apply (internal_eq_rewrite' P Q (λ Q, ■(P ∗-∗ Q))%I);
+ [ solve_proper | done | ].
+ rewrite (plainly_emp_intro (P ≡ Q)%I).
+ apply plainly_mono, wand_iff_refl.
+ Qed.
+
+ Lemma plainly_alt P : ■P ⊣⊢ <affine> P ≡ emp.
+ Proof.
+ rewrite -plainly_affinely_elim. 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 _ _ plainly).
+ by rewrite -plainly_True_emp plainly_pure True_impl.
+ Qed.
+
+ Lemma plainly_alt_absorbing P `{!Absorbing P} : ■P ⊣⊢ P ≡ True.
+ Proof.
+ apply (anti_symm (⊢)).
+ - rewrite prop_ext. apply plainly_mono, and_intro; apply wand_intro_l; auto.
+ - rewrite internal_eq_sym (internal_eq_rewrite _ _ plainly).
+ by rewrite plainly_pure True_impl.
+ Qed.
+
+ Lemma plainly_True_alt P : ■(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, ■(True -∗ Q))%I ltac:(shelve)); last solve_proper.
+ by rewrite -entails_wand // -(plainly_emp_intro True%I) True_impl.
+ Qed.
+End prop_ext.
(* Interaction with â–· *)
Lemma later_plainly P : ▷ ■P ⊣⊢ ■▷ P.
@@ -601,10 +615,6 @@ Proof. by rewrite /bi_except_0 -plainly_or_2 -later_plainly plainly_pure. Qed.
Lemma except_0_plainly `{!BiPlainlyExist PROP} P : ◇ ■P ⊣⊢ ■◇ P.
Proof. by rewrite /bi_except_0 plainly_or -later_plainly plainly_pure. Qed.
-Global Instance internal_eq_plain {A : ofeT} (a b : A) :
- Plain (PROP:=PROP) (a ≡ b).
-Proof. by intros; rewrite /Plain plainly_internal_eq. Qed.
-
Global Instance later_plain P : Plain P → Plain (▷ P).
Proof. intros. by rewrite /Plain -later_plainly {1}(plain P). Qed.
Global Instance laterN_plain n P : Plain P → Plain (▷^n P).
diff --git a/theories/proofmode/class_instances_sbi.v b/theories/proofmode/class_instances_sbi.v
index 1b335fc46..3e40fc8dc 100644
--- a/theories/proofmode/class_instances_sbi.v
+++ b/theories/proofmode/class_instances_sbi.v
@@ -37,7 +37,7 @@ Proof.
Qed.
(** FromPure *)
-Global Instance from_pure_internal_eq {A : ofeT} (a b : A) :
+Global Instance from_pure_internal_eq `{!BiInternalEq PROP} {A : ofeT} (a b : A) :
@FromPure PROP false (a ≡ b) (a ≡ b).
Proof. by rewrite /FromPure pure_internal_eq. Qed.
Global Instance from_pure_later a P φ : FromPure a P φ → FromPure a (▷ P) φ.
@@ -56,7 +56,7 @@ Global Instance from_pure_plainly `{BiPlainly PROP} P φ :
Proof. rewrite /FromPure=> <-. by rewrite plainly_pure. Qed.
(** IntoPure *)
-Global Instance into_pure_eq {A : ofeT} (a b : A) :
+Global Instance into_pure_eq `{!BiInternalEq PROP} {A : ofeT} (a b : A) :
Discrete a → @IntoPure PROP (a ≡ b) (a ≡ b).
Proof. intros. by rewrite /IntoPure discrete_eq. Qed.
@@ -354,7 +354,7 @@ Global Instance is_except_0_except_0 P : IsExcept0 (â—‡ P).
Proof. by rewrite /IsExcept0 except_0_idemp. Qed.
Global Instance is_except_0_later P : IsExcept0 (â–· P).
Proof. by rewrite /IsExcept0 except_0_later. Qed.
-Global Instance is_except_0_embed `{SbiEmbed PROP PROP'} P :
+Global Instance is_except_0_embed `{BiEmbedLater PROP PROP'} P :
IsExcept0 P → IsExcept0 ⎡P⎤.
Proof. by rewrite /IsExcept0 -embed_except_0=>->. Qed.
Global Instance is_except_0_bupd `{BiBUpd PROP} P : IsExcept0 P → IsExcept0 (|==> P).
@@ -373,7 +373,7 @@ Proof. by rewrite /FromModal. Qed.
Global Instance from_modal_laterN n P :
FromModal (modality_laterN n) (â–·^n P) (â–·^n P) P.
Proof. by rewrite /FromModal. Qed.
-Global Instance from_modal_Next {A : ofeT} (x y : A) :
+Global Instance from_modal_Next `{!BiInternalEq PROP} {A : ofeT} (x y : A) :
FromModal (PROP1:=PROP) (PROP2:=PROP) (modality_laterN 1)
(▷^1 (x ≡ y) : PROP)%I (Next x ≡ Next y) (x ≡ y).
Proof. by rewrite /FromModal /= later_equivI. Qed.
@@ -385,7 +385,7 @@ Global Instance from_modal_fupd E P `{BiFUpd PROP} :
FromModal modality_id (|={E}=> P) (|={E}=> P) P.
Proof. by rewrite /FromModal /= -fupd_intro. Qed.
-Global Instance from_modal_later_embed `{SbiEmbed PROP PROP'} `(sel : A) n P Q :
+Global Instance from_modal_later_embed `{BiEmbedLater PROP PROP'} `(sel : A) n P Q :
FromModal (modality_laterN n) sel P Q →
FromModal (modality_laterN n) sel ⎡P⎤ ⎡Q⎤.
Proof. rewrite /FromModal /= =><-. by rewrite embed_laterN. Qed.
@@ -394,35 +394,40 @@ Global Instance from_modal_plainly `{BiPlainly PROP} P :
FromModal modality_plainly (â– P) (â– P) P | 2.
Proof. by rewrite /FromModal. Qed.
-Global Instance from_modal_plainly_embed `{BiPlainly PROP, BiPlainly PROP',
- BiEmbedPlainly PROP PROP', !SbiEmbed PROP PROP'} `(sel : A) P Q :
+Global Instance from_modal_plainly_embed `{!BiPlainly PROP, !BiPlainly PROP',
+ !BiEmbed PROP PROP', !BiEmbedPlainly PROP PROP'} `(sel : A) P Q :
FromModal modality_plainly sel P Q →
FromModal (PROP2:=PROP') modality_plainly sel ⎡P⎤ ⎡Q⎤ | 100.
Proof. rewrite /FromModal /= =><-. by rewrite embed_plainly. Qed.
(** IntoInternalEq *)
-Global Instance into_internal_eq_internal_eq {A : ofeT} (x y : A) :
- @IntoInternalEq PROP A (x ≡ y) x y.
-Proof. by rewrite /IntoInternalEq. Qed.
-Global Instance into_internal_eq_affinely {A : ofeT} (x y : A) P :
- IntoInternalEq P x y → IntoInternalEq (<affine> P) x y.
-Proof. rewrite /IntoInternalEq=> ->. by rewrite affinely_elim. Qed.
-Global Instance into_internal_eq_intuitionistically {A : ofeT} (x y : A) P :
- IntoInternalEq P x y → IntoInternalEq (□ P) x y.
-Proof. rewrite /IntoInternalEq=> ->. by rewrite intuitionistically_elim. Qed.
-Global Instance into_internal_eq_absorbingly {A : ofeT} (x y : A) P :
- IntoInternalEq P x y → IntoInternalEq (<absorb> P) x y.
-Proof. rewrite /IntoInternalEq=> ->. by rewrite absorbingly_internal_eq. Qed.
-Global Instance into_internal_eq_plainly `{BiPlainly PROP} {A : ofeT} (x y : A) P :
- IntoInternalEq P x y → IntoInternalEq (■P) x y.
-Proof. rewrite /IntoInternalEq=> ->. by rewrite plainly_elim. Qed.
-Global Instance into_internal_eq_persistently {A : ofeT} (x y : A) P :
- IntoInternalEq P x y → IntoInternalEq (<pers> P) x y.
-Proof. rewrite /IntoInternalEq=> ->. by rewrite persistently_elim. Qed.
-Global Instance into_internal_eq_embed
- `{SbiEmbed PROP PROP'} {A : ofeT} (x y : A) P :
- IntoInternalEq P x y → IntoInternalEq ⎡P⎤ x y.
-Proof. rewrite /IntoInternalEq=> ->. by rewrite embed_internal_eq. Qed.
+Section internal_eq.
+ Context `{!BiInternalEq PROP}.
+
+ Global Instance into_internal_eq_internal_eq {A : ofeT} (x y : A) :
+ @IntoInternalEq PROP _ A (x ≡ y) x y.
+ Proof. by rewrite /IntoInternalEq. Qed.
+ Global Instance into_internal_eq_affinely {A : ofeT} (x y : A) P :
+ IntoInternalEq P x y → IntoInternalEq (<affine> P) x y.
+ Proof. rewrite /IntoInternalEq=> ->. by rewrite affinely_elim. Qed.
+ Global Instance into_internal_eq_intuitionistically {A : ofeT} (x y : A) P :
+ IntoInternalEq P x y → IntoInternalEq (□ P) x y.
+ Proof. rewrite /IntoInternalEq=> ->. by rewrite intuitionistically_elim. Qed.
+ Global Instance into_internal_eq_absorbingly {A : ofeT} (x y : A) P :
+ IntoInternalEq P x y → IntoInternalEq (<absorb> P) x y.
+ Proof. rewrite /IntoInternalEq=> ->. by rewrite absorbingly_internal_eq. Qed.
+ Global Instance into_internal_eq_plainly `{BiPlainly PROP} {A : ofeT} (x y : A) P :
+ IntoInternalEq P x y → IntoInternalEq (■P) x y.
+ Proof. rewrite /IntoInternalEq=> ->. by rewrite plainly_elim. Qed.
+ Global Instance into_internal_eq_persistently {A : ofeT} (x y : A) P :
+ IntoInternalEq P x y → IntoInternalEq (<pers> P) x y.
+ Proof. rewrite /IntoInternalEq=> ->. by rewrite persistently_elim. Qed.
+ Global Instance into_internal_eq_embed
+ `{!BiInternalEq PROP', BiEmbedInternalEq PROP PROP'}
+ {A : ofeT} (x y : A) (P : PROP) :
+ IntoInternalEq P x y → IntoInternalEq (⎡P⎤ : PROP')%I x y.
+ Proof. rewrite /IntoInternalEq=> ->. by rewrite embed_internal_eq. Qed.
+End internal_eq.
(** IntoExcept0 *)
Global Instance into_except_0_except_0 P : IntoExcept0 (â—‡ P) P.
@@ -447,7 +452,7 @@ Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_plainly. Qed.
Global Instance into_except_0_persistently P Q :
IntoExcept0 P Q → IntoExcept0 (<pers> P) (<pers> Q).
Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_persistently. Qed.
-Global Instance into_except_0_embed `{SbiEmbed PROP PROP'} P Q :
+Global Instance into_except_0_embed `{BiEmbedLater PROP PROP'} P Q :
IntoExcept0 P Q → IntoExcept0 ⎡P⎤ ⎡Q⎤.
Proof. rewrite /IntoExcept0=> ->. by rewrite embed_except_0. Qed.
@@ -572,7 +577,8 @@ Proof.
move=> Hn [_ ->|->] <-; by rewrite -!laterN_plus -Hn Nat.add_comm.
Qed.
-Global Instance into_laterN_Next {A : ofeT} only_head n n' (x y : A) :
+Global Instance into_laterN_Next `{!BiInternalEq PROP}
+ {A : ofeT} only_head n n' (x y : A) :
NatCancel n 1 n' 0 →
IntoLaterN (PROP:=PROP) only_head n (Next x ≡ Next y) (x ≡ y) | 2.
Proof.
@@ -625,7 +631,7 @@ Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_plainly. Qed
Global Instance into_later_persistently n P Q :
IntoLaterN false n P Q → IntoLaterN false n (<pers> P) (<pers> Q).
Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_persistently. Qed.
-Global Instance into_later_embed`{SbiEmbed PROP PROP'} n P Q :
+Global Instance into_later_embed`{BiEmbedLater PROP PROP'} n P Q :
IntoLaterN false n P Q → IntoLaterN false n ⎡P⎤ ⎡Q⎤.
Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite embed_laterN. Qed.
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index be5d9bfb2..01a9ae738 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -79,11 +79,11 @@ Proof. by exists φ. Qed.
Hint Extern 0 (FromPureT _ _ _) =>
notypeclasses refine (from_pureT_hint _ _ _ _) : typeclass_instances.
-Class IntoInternalEq {PROP : bi} {A : ofeT} (P : PROP) (x y : A) :=
+Class IntoInternalEq `{BiInternalEq PROP} {A : ofeT} (P : PROP) (x y : A) :=
into_internal_eq : P ⊢ x ≡ y.
-Arguments IntoInternalEq {_ _} _%I _%type_scope _%type_scope : simpl never.
-Arguments into_internal_eq {_ _} _%I _%type_scope _%type_scope {_}.
-Hint Mode IntoInternalEq + - ! - - : typeclass_instances.
+Arguments IntoInternalEq {_ _ _} _%I _%type_scope _%type_scope : simpl never.
+Arguments into_internal_eq {_ _ _} _%I _%type_scope _%type_scope {_}.
+Hint Mode IntoInternalEq + - - ! - - : typeclass_instances.
Class IntoPersistent {PROP : bi} (p : bool) (P Q : PROP) :=
into_persistent : <pers>?p P ⊢ <pers> Q.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index b41702ee9..5159c0a58 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -1022,7 +1022,7 @@ Implicit Types Δ : envs PROP.
Implicit Types P Q : PROP.
(** * Rewriting *)
-Lemma tac_rewrite Δ i p Pxy d Q :
+Lemma tac_rewrite `{!BiInternalEq PROP} Δ i p Pxy d Q :
envs_lookup i Δ = Some (p, Pxy) →
∀ {A : ofeT} (x y : A) (Φ : A → PROP),
IntoInternalEq Pxy x y →
@@ -1036,7 +1036,7 @@ Proof.
destruct d; auto using internal_eq_sym.
Qed.
-Lemma tac_rewrite_in Δ i p Pxy j q P d Q :
+Lemma tac_rewrite_in `{!BiInternalEq PROP} Δ i p Pxy j q P d Q :
envs_lookup i Δ = Some (p, Pxy) →
envs_lookup j Δ = Some (q, P) →
∀ {A : ofeT} (x y : A) (Φ : A → PROP),
diff --git a/theories/proofmode/frame_instances.v b/theories/proofmode/frame_instances.v
index 3c17872f7..3e909d0b1 100644
--- a/theories/proofmode/frame_instances.v
+++ b/theories/proofmode/frame_instances.v
@@ -292,8 +292,9 @@ Proof.
rewrite persistently_elim impl_elim_r //.
Qed.
-Global Instance frame_eq_embed `{SbiEmbed PROP PROP'} p P Q (Q' : PROP')
- {A : ofeT} (a b : A) :
+Global Instance frame_eq_embed `{!BiEmbed PROP PROP', !BiInternalEq PROP,
+ !BiInternalEq PROP', !BiEmbedInternalEq PROP PROP'}
+ p P Q (Q' : PROP') {A : ofeT} (a b : A) :
Frame p (a ≡ b) P Q → MakeEmbed Q Q' → Frame p (a ≡ b) ⎡P⎤ Q'.
Proof. rewrite /Frame /MakeEmbed -embed_internal_eq. apply (frame_embed p P Q). Qed.
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 95810df70..aabad6df9 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -3242,7 +3242,7 @@ Hint Extern 0 (envs_entails _ emp) => iEmpIntro : core.
(* TODO: look for a more principled way of adding trivial hints like those
below; see the discussion in !75 for further details. *)
Hint Extern 0 (envs_entails _ (_ ≡ _)) =>
- rewrite envs_entails_eq; apply bi.internal_eq_refl : core.
+ rewrite envs_entails_eq; apply internal_eq_refl : core.
Hint Extern 0 (envs_entails _ (big_opL _ _ _)) =>
rewrite envs_entails_eq; apply big_sepL_nil' : core.
Hint Extern 0 (envs_entails _ (big_sepL2 _ _ _)) =>
diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index feb5d5f68..97dfa462f 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -474,9 +474,8 @@ Global Instance is_except_0_monPred_at i P :
IsExcept0 P → IsExcept0 (P i).
Proof. rewrite /IsExcept0=>- [/(_ i)]. by rewrite monPred_at_except_0. Qed.
-Global Instance make_monPred_at_internal_eq {A : ofeT} (x y : A) i :
+Global Instance make_monPred_at_internal_eq `{!BiInternalEq PROP} {A : ofeT} (x y : A) i :
MakeMonPredAt i (x ≡ y) (x ≡ y).
-
Proof. by rewrite /MakeMonPredAt monPred_at_internal_eq. Qed.
Global Instance make_monPred_at_except_0 i P ð“ :
MakeMonPredAt i P ð“ → MakeMonPredAt i (â—‡ P)%I (â—‡ ð“ )%I.
@@ -491,7 +490,8 @@ Global Instance make_monPred_at_fupd `{BiFUpd PROP} i E1 E2 P ð“Ÿ :
MakeMonPredAt i P 𓟠→ MakeMonPredAt i (|={E1,E2}=> P)%I (|={E1,E2}=> ð“Ÿ)%I.
Proof. by rewrite /MakeMonPredAt monPred_at_fupd=> <-. Qed.
-Global Instance into_internal_eq_monPred_at {A : ofeT} (x y : A) P i :
+Global Instance into_internal_eq_monPred_at `{!BiInternalEq PROP}
+ {A : ofeT} (x y : A) P i :
IntoInternalEq P x y → IntoInternalEq (P i) x y.
Proof. rewrite /IntoInternalEq=> ->. by rewrite monPred_at_internal_eq. Qed.
diff --git a/theories/si_logic/bi.v b/theories/si_logic/bi.v
index 463c90cc6..a12d22cc4 100644
--- a/theories/si_logic/bi.v
+++ b/theories/si_logic/bi.v
@@ -84,21 +84,13 @@ Proof.
done.
Qed.
-Lemma siProp_sbi_mixin : SbiMixin
- siProp_entails siProp_pure siProp_or siProp_impl
- (@siProp_forall) (@siProp_exist) siProp_sep
- siProp_persistently (@siProp_internal_eq) siProp_later.
+Lemma siProp_bi_later_mixin :
+ BiLaterMixin
+ siProp_entails siProp_pure siProp_or siProp_impl
+ (@siProp_forall) (@siProp_exist) siProp_sep siProp_persistently siProp_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.
@@ -121,11 +113,26 @@ Qed.
Canonical Structure siPropI : bi :=
{| bi_ofe_mixin := ofe_mixin_of siProp;
- bi_bi_mixin := siProp_bi_mixin; bi_sbi_mixin := siProp_sbi_mixin |}.
+ bi_bi_mixin := siProp_bi_mixin; bi_bi_later_mixin := siProp_bi_later_mixin |}.
Instance siProp_later_contractive : Contractive (bi_later (PROP:=siPropI)).
Proof. apply later_contractive. Qed.
+Lemma siProp_internal_eq_mixin : BiInternalEqMixin siPropI (@siProp_internal_eq).
+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 siProp_internal_eq : BiInternalEq siPropI :=
+ {| bi_internal_eq_mixin := siProp_internal_eq_mixin |}.
+
Lemma siProp_plainly_mixin : BiPlainlyMixin siPropI siProp_plainly.
Proof.
split; try done.
@@ -134,12 +141,13 @@ Proof.
intros P. by apply pure_intro.
- (* ■P ∗ Q ⊢ ■P *)
intros P Q. apply and_elim_l.
- - (* ■((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q *)
- intros P Q. apply prop_ext_2.
Qed.
Global Instance siProp_plainlyC : BiPlainly siPropI :=
{| bi_plainly_mixin := siProp_plainly_mixin |}.
+Global Instance siProp_prop_ext : BiPropExt siPropI.
+Proof. exact: prop_ext_2. Qed.
+
(** extra BI instances *)
Global Instance siProp_affine : BiAffine siPropI | 0.
--
GitLab