From 30a36cf2e0949573d13cf2ef0233aa408bcf09ca Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Fri, 2 Feb 2018 15:49:05 +0100
Subject: [PATCH] Move internal_eq in the sbi interface.
---
theories/base_logic/upred.v | 57 +++---
theories/bi/derived_laws.v | 259 ++++++++++++++-------------
theories/bi/embedding.v | 16 +-
theories/bi/interface.v | 133 +++++++-------
theories/bi/monpred.v | 79 ++++----
theories/proofmode/class_instances.v | 67 +++----
theories/proofmode/classes.v | 2 +-
theories/proofmode/coq_tactics.v | 74 ++++----
theories/proofmode/monpred.v | 14 +-
9 files changed, 348 insertions(+), 353 deletions(-)
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 88e0b7aae..e89357f1e 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -349,7 +349,7 @@ Definition unseal_eqs :=
Ltac unseal := (* Coq unfold is used to circumvent bug #5699 in rewrite /foo *)
unfold bi_emp; simpl;
unfold uPred_emp, bi_pure, bi_and, bi_or, bi_impl, bi_forall, bi_exist,
- bi_internal_eq, bi_sep, bi_wand, bi_plainly, bi_persistently, sbi_later; simpl;
+ bi_sep, bi_wand, bi_plainly, bi_persistently, sbi_internal_eq, sbi_later; simpl;
unfold sbi_emp, sbi_pure, sbi_and, sbi_or, sbi_impl, sbi_forall, sbi_exist,
sbi_internal_eq, sbi_sep, sbi_wand, sbi_plainly, sbi_persistently; simpl;
rewrite !unseal_eqs /=.
@@ -358,10 +358,11 @@ Import uPred_unseal.
Local Arguments uPred_holds {_} !_ _ _ /.
-Lemma uPred_bi_mixin (M : ucmraT) : BiMixin (ofe_mixin_of (uPred M))
- uPred_entails uPred_emp uPred_pure uPred_and uPred_or uPred_impl
- (@uPred_forall M) (@uPred_exist M) (@uPred_internal_eq M)
- uPred_sep uPred_wand uPred_plainly uPred_persistently.
+Lemma uPred_bi_mixin (M : ucmraT) :
+ BiMixin
+ uPred_entails uPred_emp uPred_pure uPred_and uPred_or uPred_impl
+ (@uPred_forall M) (@uPred_exist M) uPred_sep uPred_wand uPred_plainly
+ uPred_persistently.
Proof.
split.
- (* PreOrder uPred_entails *)
@@ -403,10 +404,6 @@ Proof.
- (* NonExpansive uPred_persistently *)
intros n P1 P2 HP.
unseal; split=> n' x; split; apply HP; eauto using @cmra_core_validN.
- - (* NonExpansive2 (@uPred_internal_eq M A) *)
- intros A n x x' Hx y y' Hy; split=> n' z; unseal; split; intros; simpl in *.
- + by rewrite -(dist_le _ _ _ _ Hx) -?(dist_le _ _ _ _ Hy); auto.
- + by rewrite (dist_le _ _ _ _ Hx) ?(dist_le _ _ _ _ Hy); auto.
- (* φ → P ⊢ ⌜φ⌠*)
intros P φ ?. unseal; by split.
- (* (φ → True ⊢ P) → ⌜φ⌠⊢ P *)
@@ -438,17 +435,6 @@ Proof.
intros A Ψ a. unseal; split=> n x ??; by exists a.
- (* (∀ a, Ψ a ⊢ Q) → (∃ a, Ψ a) ⊢ Q *)
intros A Ψ Q. unseal; intros HΨ; split=> n x ? [a ?]; by apply HΨ with a.
- - (* P ⊢ a ≡ a *)
- intros A P a. unseal; by split=> n x ?? /=.
- - (* a ≡ b ⊢ Ψ a → Ψ b *)
- intros A a b Ψ Hnonexp.
- unseal; split=> n x ? Hab n' x' ??? HΨ. eapply Hnonexp with n a; auto.
- - (* (∀ x, f x ≡ g x) ⊢ f ≡ g *)
- by unseal.
- - (* `x ≡ `y ⊢ x ≡ y *)
- by unseal.
- - (* Discrete a → a ≡ b ⊣⊢ ⌜a ≡ b⌠*)
- intros A a b ?. unseal; split=> n x ?; by apply (discrete_iff n).
- (* (P ⊢ Q) → (P' ⊢ Q') → P ∗ P' ⊢ Q ∗ Q' *)
intros P P' Q Q' HQ HQ'; unseal.
split; intros n' x ? (x1&x2&?&?&?); exists x1,x2; ofe_subst x;
@@ -482,9 +468,6 @@ Proof.
unseal; split=> n x ?? //.
- (* (∀ a, bi_plainly (Ψ a)) ⊢ bi_plainly (∀ a, Ψ a) *)
by unseal.
- - (* bi_plainly ((P → Q) ∧ (Q → P)) ⊢ P ≡ Q *)
- unseal; split=> n x ? /= HPQ; split=> n' x' ? HP;
- split; eapply HPQ; eauto using @ucmra_unit_least.
- (* (bi_plainly P → bi_persistently Q) ⊢ bi_persistently (bi_plainly P → Q) *)
unseal; split=> /= n x ? HPQ n' x' ????.
eapply uPred_mono with n' (core x)=>//; [|by apply cmra_included_includedN].
@@ -518,15 +501,33 @@ Proof.
exists (core x), x; rewrite ?cmra_core_l; auto.
Qed.
-Lemma uPred_sbi_mixin (M : ucmraT) : SbiMixin
- uPred_entails uPred_pure uPred_or uPred_impl
- (@uPred_forall M) (@uPred_exist M) (@uPred_internal_eq M)
- uPred_sep uPred_plainly uPred_persistently uPred_later.
+Lemma uPred_sbi_mixin (M : ucmraT) : SbiMixin uPred_ofe_mixin
+ uPred_entails uPred_pure uPred_and uPred_or uPred_impl
+ (@uPred_forall M) (@uPred_exist M) uPred_sep uPred_plainly uPred_persistently
+ (@uPred_internal_eq M) uPred_later.
Proof.
split.
- (* Contractive sbi_later *)
unseal; intros [|n] P Q HPQ; split=> -[|n'] x ?? //=; try omega.
apply HPQ; eauto using cmra_validN_S.
+ - (* NonExpansive2 (@uPred_internal_eq M A) *)
+ intros A n x x' Hx y y' Hy; split=> n' z; unseal; split; intros; simpl in *.
+ + by rewrite -(dist_le _ _ _ _ Hx) -?(dist_le _ _ _ _ Hy); auto.
+ + by rewrite (dist_le _ _ _ _ Hx) ?(dist_le _ _ _ _ Hy); auto.
+ - (* P ⊢ a ≡ a *)
+ intros A P a. unseal; by split=> n x ?? /=.
+ - (* a ≡ b ⊢ Ψ a → Ψ b *)
+ intros A a b Ψ Hnonexp.
+ unseal; split=> n x ? Hab n' x' ??? HΨ. eapply Hnonexp with n a; auto.
+ - (* (∀ x, f x ≡ g x) ⊢ f ≡ g *)
+ by unseal.
+ - (* `x ≡ `y ⊢ x ≡ y *)
+ by unseal.
+ - (* Discrete a → a ≡ b ⊣⊢ ⌜a ≡ b⌠*)
+ intros A a b ?. unseal; split=> n x ?; by apply (discrete_iff n).
+ - (* bi_plainly ((P → Q) ∧ (Q → P)) ⊢ P ≡ Q *)
+ unseal; split=> n x ? /= HPQ; split=> n' x' ? HP;
+ split; eapply HPQ; eauto using @ucmra_unit_least.
- (* Next x ≡ Next y ⊢ ▷ (x ≡ y) *)
by unseal.
- (* ▷ (x ≡ y) ⊢ Next x ≡ Next y *)
@@ -638,7 +639,7 @@ Lemma ownM_unit : bi_valid (uPred_ownM (ε:M)).
Proof. unseal; split=> n x ??; by exists x; rewrite left_id. Qed.
Lemma later_ownM (a : M) : ▷ uPred_ownM a ⊢ ∃ b, uPred_ownM b ∧ ▷ (a ≡ b).
Proof.
- rewrite /bi_and /sbi_later /bi_exist /bi_internal_eq /=; unseal.
+ rewrite /bi_and /sbi_later /bi_exist /sbi_internal_eq /=; unseal.
split=> -[|n] x /= ? Hax; first by eauto using ucmra_unit_leastN.
destruct Hax as [y ?].
destruct (cmra_extend n x a y) as (a'&y'&Hx&?&?); auto using cmra_validN_S.
diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index f8249ff54..41c7e56d3 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -68,8 +68,6 @@ Proof.
intros Φ1 Φ2 HΦ. apply equiv_dist=> n.
apply exist_ne=> x. apply equiv_dist, HΦ.
Qed.
-Global Instance internal_eq_proper (A : ofeT) :
- Proper ((≡) ==> (≡) ==> (⊣⊢)) (@bi_internal_eq PROP A) := ne_proper_2 _.
Global Instance plainly_proper :
Proper ((⊣⊢) ==> (⊣⊢)) (@bi_plainly PROP) := ne_proper _.
Global Instance persistently_proper :
@@ -273,84 +271,6 @@ Global Instance iff_proper :
Lemma iff_refl Q P : Q ⊢ P ↔ P.
Proof. rewrite /bi_iff; apply and_intro; apply impl_intro_l; auto. Qed.
-(* Equality stuff *)
-Hint Resolve internal_eq_refl.
-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 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.
-
-Lemma ofe_fun_equivI {A} {B : A → ofeT} (f g : ofe_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_morC_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 -(ofe_fun_equivI (ofe_mor_car _ _ f) (ofe_mor_car _ _ g)).
- set (h1 (f : A -n> B) :=
- exist (λ f : A -c> B, NonExpansive (f : A → B)) f (ofe_mor_ne A B f)).
- set (h2 (f : sigC (λ f : A -c> B, NonExpansive (f : A → B))) :=
- @CofeMor 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.
(* BI Stuff *)
Hint Resolve sep_mono.
@@ -577,13 +497,6 @@ Proof.
apply wand_intro_l. rewrite (forall_elim Hφ) comm. by apply absorbing.
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.
-
(* Properties of the affinely modality *)
Global Instance affinely_ne : NonExpansive (@bi_affinely PROP).
Proof. solve_proper. Qed.
@@ -686,13 +599,6 @@ Lemma absorbingly_exist {A} (Φ : A → PROP) :
bi_absorbingly (∃ a, Φ a) ⊣⊢ ∃ a, bi_absorbingly (Φ a).
Proof. by rewrite /bi_absorbingly sep_exist_l. Qed.
-Lemma absorbingly_internal_eq {A : ofeT} (x y : A) : bi_absorbingly (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 absorbingly_sep P Q : bi_absorbingly (P ∗ Q) ⊣⊢ bi_absorbingly P ∗ bi_absorbingly Q.
Proof. by rewrite -{1}absorbingly_idemp /bi_absorbingly !assoc -!(comm _ P) !assoc. Qed.
Lemma absorbingly_True_emp : bi_absorbingly True ⊣⊢ bi_absorbingly emp.
@@ -901,15 +807,6 @@ Proof. by rewrite !(comm _ P) persistently_and_sep_l_1. Qed.
Lemma persistently_emp_intro P : P ⊢ bi_persistently emp.
Proof. by rewrite -plainly_elim_persistently -plainly_emp_intro. Qed.
-Lemma persistently_internal_eq {A : ofeT} (a b : A) :
- bi_persistently (a ≡ b) ⊣⊢ a ≡ b.
-Proof.
- apply (anti_symm (⊢)).
- { by rewrite persistently_elim_absorbingly absorbingly_internal_eq. }
- apply (internal_eq_rewrite' a b (λ b, bi_persistently (a ≡ b))%I); auto.
- rewrite -(internal_eq_refl emp%I a). apply persistently_emp_intro.
-Qed.
-
Lemma persistently_True_emp : bi_persistently True ⊣⊢ bi_persistently emp.
Proof. apply (anti_symm _); auto using persistently_emp_intro. Qed.
Lemma persistently_and_sep P Q : bi_persistently (P ∧ Q) ⊢ bi_persistently (P ∗ Q).
@@ -1107,14 +1004,6 @@ Proof. by rewrite -{1}(left_id emp%I _ Q%I) plainly_and_sep_assoc and_elim_l. Qe
Lemma plainly_and_sep_r_1 P Q : P ∧ bi_plainly Q ⊢ P ∗ bi_plainly Q.
Proof. by rewrite !(comm _ P) plainly_and_sep_l_1. Qed.
-Lemma plainly_internal_eq {A:ofeT} (a b : A) : bi_plainly (a ≡ b) ⊣⊢ a ≡ b.
-Proof.
- apply (anti_symm (⊢)).
- { by rewrite plainly_elim_absorbingly absorbingly_internal_eq. }
- apply (internal_eq_rewrite' a b (λ b, bi_plainly (a ≡ b))%I); [solve_proper|done|].
- rewrite -(internal_eq_refl True%I a) plainly_pure; auto.
-Qed.
-
Lemma plainly_True_emp : bi_plainly True ⊣⊢ bi_plainly emp.
Proof. apply (anti_symm _); auto using plainly_emp_intro. Qed.
Lemma plainly_and_sep P Q : bi_plainly (P ∧ Q) ⊢ bi_plainly (P ∗ Q).
@@ -1564,13 +1453,6 @@ Lemma plain_plainly P `{!Plain P, !Absorbing P} : bi_plainly P ⊣⊢ P.
Proof. apply (anti_symm _), plain_plainly_2, _. apply plainly_elim, _. Qed.
Lemma plainly_intro P Q `{!Plain P} : (P ⊢ Q) → P ⊢ bi_plainly Q.
Proof. by intros <-. Qed.
-Lemma plainly_alt P : bi_plainly P ⊣⊢ P ≡ True.
-Proof.
- apply (anti_symm (⊢)).
- - rewrite -prop_ext. apply plainly_mono, and_intro; apply impl_intro_r; auto.
- - rewrite internal_eq_sym (internal_eq_rewrite _ _ bi_plainly).
- by rewrite plainly_pure True_impl.
-Qed.
(* Affine instances *)
Global Instance emp_affine_l : Affine (emp%I : PROP).
@@ -1614,9 +1496,6 @@ Proof.
rewrite persistent_and_affinely_sep_l_1 absorbingly_sep_r.
by rewrite -persistent_and_affinely_sep_l impl_elim_r.
Qed.
-Global Instance internal_eq_absorbing {A : ofeT} (x y : A) :
- Absorbing (x ≡ y : PROP)%I.
-Proof. by rewrite /Absorbing absorbingly_internal_eq. Qed.
Global Instance sep_absorbing_l P Q : Absorbing P → Absorbing (P ∗ Q).
Proof. intros. by rewrite /Absorbing -absorbingly_sep_l absorbing. Qed.
@@ -1667,10 +1546,6 @@ Proof.
apply exist_mono=> x. by rewrite -!persistent.
Qed.
-Global Instance internal_eq_persistent {A : ofeT} (a b : A) :
- Persistent (a ≡ b : PROP)%I.
-Proof. by intros; rewrite /Persistent persistently_internal_eq. Qed.
-
Global Instance impl_persistent P Q :
Absorbing P → Plain P → Persistent Q → Persistent (P → Q).
Proof.
@@ -1723,10 +1598,6 @@ Proof.
intros. rewrite /Plain -plainly_exist_2. apply exist_mono=> x. by rewrite -plain.
Qed.
-Global Instance internal_eq_plain {A : ofeT} (a b : A) :
- Plain (a ≡ b : PROP)%I.
-Proof. by intros; rewrite /Plain plainly_internal_eq. Qed.
-
Global Instance impl_plain P Q :
Absorbing P → Plain P → Plain Q → Plain (P → Q).
Proof.
@@ -1888,10 +1759,140 @@ Notation "P ⊣⊢ Q" := (equiv (A:=bi_car PROP) P%I Q%I).
Hint Resolve or_elim or_intro_l' or_intro_r' True_intro False_elim.
Hint Resolve and_elim_l' and_elim_r' and_intro forall_intro.
+Global Instance internal_eq_proper (A : ofeT) :
+ Proper ((≡) ==> (≡) ==> (⊣⊢)) (@sbi_internal_eq PROP A) := ne_proper_2 _.
Global Instance later_proper :
Proper ((⊣⊢) ==> (⊣⊢)) (@sbi_later PROP) := ne_proper _.
(* Equality *)
+Hint Resolve internal_eq_refl.
+Hint Extern 100 (NonExpansive _) => solve_proper.
+
+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 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.
+
+Lemma ofe_fun_equivI {A} {B : A → ofeT} (f g : ofe_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_morC_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 -(ofe_fun_equivI (ofe_mor_car _ _ f) (ofe_mor_car _ _ g)).
+ set (h1 (f : A -n> B) :=
+ exist (λ f : A -c> B, NonExpansive (f : A → B)) f (ofe_mor_ne A B f)).
+ set (h2 (f : sigC (λ f : A -c> B, NonExpansive (f : A → B))) :=
+ @CofeMor 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) : bi_absorbingly (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) :
+ bi_persistently (a ≡ b) ⊣⊢ a ≡ b.
+Proof.
+ apply (anti_symm (⊢)).
+ { by rewrite persistently_elim_absorbingly absorbingly_internal_eq. }
+ apply (internal_eq_rewrite' a b (λ b, bi_persistently (a ≡ b))%I); auto.
+ rewrite -(internal_eq_refl emp%I a). apply persistently_emp_intro.
+Qed.
+Lemma plainly_internal_eq {A:ofeT} (a b : A) : bi_plainly (a ≡ b) ⊣⊢ a ≡ b.
+Proof.
+ apply (anti_symm (⊢)).
+ { by rewrite plainly_elim_absorbingly absorbingly_internal_eq. }
+ apply (internal_eq_rewrite' a b (λ b, bi_plainly (a ≡ b))%I); [solve_proper|done|].
+ rewrite -(internal_eq_refl True%I a) plainly_pure; auto.
+Qed.
+
+Lemma plainly_alt P : bi_plainly P ⊣⊢ P ≡ True.
+Proof.
+ apply (anti_symm (⊢)).
+ - rewrite -prop_ext. apply plainly_mono, and_intro; apply impl_intro_r; auto.
+ - rewrite internal_eq_sym (internal_eq_rewrite _ _ bi_plainly).
+ by rewrite plainly_pure True_impl.
+Qed.
+
+Global Instance internal_eq_absorbing {A : ofeT} (x y : A) :
+ Absorbing (x ≡ y : PROP)%I.
+Proof. by rewrite /Absorbing absorbingly_internal_eq. Qed.
+Global Instance internal_eq_plain {A : ofeT} (a b : A) :
+ Plain (a ≡ b : PROP)%I.
+Proof. by intros; rewrite /Plain plainly_internal_eq. Qed.
+Global Instance internal_eq_persistent {A : ofeT} (a b : A) :
+ Persistent (a ≡ b : PROP)%I.
+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.
diff --git a/theories/bi/embedding.v b/theories/bi/embedding.v
index a3cabc167..4b7d4b234 100644
--- a/theories/bi/embedding.v
+++ b/theories/bi/embedding.v
@@ -22,7 +22,6 @@ Class BiEmbedding (PROP1 PROP2 : bi) `{BiEmbed PROP1 PROP2} := {
bi_embed_impl_2 P Q : (⎡P⎤ → ⎡Q⎤) ⊢ ⎡P → Q⎤;
bi_embed_forall_2 A (Φ : A → PROP1) : (∀ x, ⎡Φ x⎤) ⊢ ⎡∀ x, Φ x⎤;
bi_embed_exist_1 A (Φ : A → PROP1) : ⎡∃ x, Φ x⎤ ⊢ ∃ x, ⎡Φ x⎤;
- bi_embed_internal_eq_1 (A : ofeT) (x y : A) : ⎡x ≡ y⎤ ⊢ x ≡ y;
bi_embed_sep P Q : ⎡P ∗ Q⎤ ⊣⊢ ⎡P⎤ ∗ ⎡Q⎤;
bi_embed_wand_2 P Q : (⎡P⎤ -∗ ⎡Q⎤) ⊢ ⎡P -∗ Q⎤;
bi_embed_plainly P : ⎡bi_plainly P⎤ ⊣⊢ bi_plainly ⎡P⎤;
@@ -31,6 +30,7 @@ Class BiEmbedding (PROP1 PROP2 : bi) `{BiEmbed PROP1 PROP2} := {
Class SbiEmbedding (PROP1 PROP2 : sbi) `{BiEmbed PROP1 PROP2} := {
sbi_embed_bi_embed :> BiEmbedding PROP1 PROP2;
+ sbi_embed_internal_eq_1 (A : ofeT) (x y : A) : ⎡x ≡ y⎤ ⊢ x ≡ y;
sbi_embed_later P : ⎡▷ P⎤ ⊣⊢ ▷ ⎡P⎤
}.
@@ -87,13 +87,6 @@ Section bi_embedding.
last apply bi.True_intro.
apply bi.impl_intro_l. by rewrite right_id.
Qed.
- Lemma bi_embed_internal_eq (A : ofeT) (x y : A) : ⎡x ≡ y⎤ ⊣⊢ x ≡ y.
- Proof.
- apply bi.equiv_spec; split; [apply bi_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) bi_embed_pure.
- eapply bi.impl_elim; [done|]. apply bi.True_intro.
- Qed.
Lemma bi_embed_iff P Q : ⎡P ↔ Q⎤ ⊣⊢ (⎡P⎤ ↔ ⎡Q⎤).
Proof. by rewrite bi_embed_and !bi_embed_impl. Qed.
Lemma bi_embed_wand_iff P Q : ⎡P ∗-∗ Q⎤ ⊣⊢ (⎡P⎤ ∗-∗ ⎡Q⎤).
@@ -162,6 +155,13 @@ Section sbi_embedding.
Context `{SbiEmbedding PROP1 PROP2}.
Implicit Types P Q R : PROP1.
+ Lemma sbi_embed_internal_eq (A : ofeT) (x y : A) : ⎡x ≡ y⎤ ⊣⊢ x ≡ y.
+ Proof.
+ apply bi.equiv_spec; split; [apply sbi_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) bi_embed_pure.
+ eapply bi.impl_elim; [done|]. apply bi.True_intro.
+ Qed.
Lemma sbi_embed_laterN n P : ⎡▷^n P⎤ ⊣⊢ ▷^n ⎡P⎤.
Proof. induction n=>//=. rewrite sbi_embed_later. by f_equiv. Qed.
Lemma sbi_embed_except_0 P : ⎡◇ P⎤ ⊣⊢ ◇ ⎡P⎤.
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 2add9f305..9ffaa5736 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -18,11 +18,11 @@ Section bi_mixin.
Context (bi_impl : PROP → PROP → PROP).
Context (bi_forall : ∀ A, (A → PROP) → PROP).
Context (bi_exist : ∀ A, (A → PROP) → PROP).
- Context (bi_internal_eq : ∀ A : ofeT, A → A → PROP).
Context (bi_sep : PROP → PROP → PROP).
Context (bi_wand : PROP → PROP → PROP).
Context (bi_plainly : PROP → PROP).
Context (bi_persistently : PROP → PROP).
+ Context (sbi_internal_eq : ∀ A : ofeT, A → A → PROP).
Context (sbi_later : PROP → PROP).
Local Infix "⊢" := bi_entails.
@@ -37,9 +37,9 @@ Section bi_mixin.
(bi_forall _ (λ x, .. (bi_forall _ (λ y, P)) ..)).
Local Notation "∃ x .. y , P" :=
(bi_exist _ (λ x, .. (bi_exist _ (λ y, P)) ..)).
- Local Notation "x ≡ y" := (bi_internal_eq _ x y).
Local Infix "∗" := bi_sep.
Local Infix "-∗" := bi_wand.
+ Local Notation "x ≡ y" := (sbi_internal_eq _ x y).
Local Notation "â–· P" := (sbi_later P).
Record BiMixin := {
@@ -59,7 +59,6 @@ Section bi_mixin.
bi_mixin_wand_ne : NonExpansive2 bi_wand;
bi_mixin_plainly_ne : NonExpansive bi_plainly;
bi_mixin_persistently_ne : NonExpansive bi_persistently;
- bi_mixin_internal_eq_ne (A : ofeT) : NonExpansive2 (bi_internal_eq A);
(* Higher-order logic *)
bi_mixin_pure_intro P (φ : Prop) : φ → P ⊢ ⌜ φ âŒ;
@@ -83,14 +82,6 @@ Section bi_mixin.
bi_mixin_exist_intro {A} {Ψ : A → PROP} a : Ψ a ⊢ ∃ a, Ψ a;
bi_mixin_exist_elim {A} (Φ : A → PROP) Q : (∀ a, Φ a ⊢ Q) → (∃ a, Φ a) ⊢ Q;
- (* 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 : ofe_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âŒ;
-
(* BI connectives *)
bi_mixin_sep_mono P P' Q Q' : (P ⊢ Q) → (P' ⊢ Q') → P ∗ P' ⊢ Q ∗ Q';
bi_mixin_emp_sep_1 P : P ⊢ emp ∗ P;
@@ -108,9 +99,6 @@ Section bi_mixin.
bi_mixin_plainly_forall_2 {A} (Ψ : A → PROP) :
(∀ a, bi_plainly (Ψ a)) ⊢ bi_plainly (∀ a, Ψ a);
- bi_mixin_prop_ext P Q : bi_plainly ((P → Q) ∧ (Q → P)) ⊢
- bi_internal_eq (OfeT PROP prop_ofe_mixin) P Q;
-
(* The following two laws are very similar, and indeed they hold
not just for â–¡ and â– , but for any modality defined as
`M P n x := ∀ y, R x y → P n y`. *)
@@ -143,7 +131,19 @@ Section bi_mixin.
Record SbiMixin := {
sbi_mixin_later_contractive : Contractive sbi_later;
+ sbi_mixin_internal_eq_ne (A : ofeT) : NonExpansive2 (sbi_internal_eq A);
+
+ (* Equality *)
+ sbi_mixin_internal_eq_refl {A : ofeT} P (a : A) : P ⊢ a ≡ a;
+ sbi_mixin_internal_eq_rewrite {A : ofeT} a b (Ψ : A → PROP) :
+ NonExpansive Ψ → a ≡ b ⊢ Ψ a → Ψ b;
+ sbi_mixin_fun_ext {A} {B : A → ofeT} (f g : ofe_fun B) : (∀ x, f x ≡ g x) ⊢ f ≡ g;
+ sbi_mixin_sig_eq {A : ofeT} (P : A → Prop) (x y : sig P) : `x ≡ `y ⊢ x ≡ y;
+ sbi_mixin_discrete_eq_1 {A : ofeT} (a b : A) : Discrete a → a ≡ b ⊢ ⌜a ≡ bâŒ;
+ sbi_mixin_prop_ext P Q : bi_plainly ((P → Q) ∧ (Q → P)) ⊢
+ sbi_internal_eq (OfeT PROP prop_ofe_mixin) P Q;
+ (* Later *)
sbi_mixin_later_eq_1 {A : ofeT} (x y : A) : Next x ≡ Next y ⊢ ▷ (x ≡ y);
sbi_mixin_later_eq_2 {A : ofeT} (x y : A) : ▷ (x ≡ y) ⊢ Next x ≡ Next y;
@@ -178,15 +178,13 @@ Structure bi := Bi {
bi_impl : bi_car → bi_car → bi_car;
bi_forall : ∀ A, (A → bi_car) → bi_car;
bi_exist : ∀ A, (A → bi_car) → bi_car;
- bi_internal_eq : ∀ A : ofeT, A → A → bi_car;
bi_sep : bi_car → bi_car → bi_car;
bi_wand : bi_car → bi_car → bi_car;
bi_plainly : bi_car → bi_car;
bi_persistently : bi_car → bi_car;
bi_ofe_mixin : OfeMixin bi_car;
- bi_bi_mixin : BiMixin bi_ofe_mixin bi_entails bi_emp bi_pure bi_and bi_or
- bi_impl bi_forall bi_exist bi_internal_eq
- bi_sep bi_wand bi_plainly bi_persistently;
+ 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_plainly bi_persistently;
}.
Coercion bi_ofeC (PROP : bi) : ofeT := OfeT PROP (bi_ofe_mixin PROP).
@@ -200,7 +198,6 @@ Instance: Params (@bi_or) 1.
Instance: Params (@bi_impl) 1.
Instance: Params (@bi_forall) 2.
Instance: Params (@bi_exist) 2.
-Instance: Params (@bi_internal_eq) 2.
Instance: Params (@bi_sep) 1.
Instance: Params (@bi_wand) 1.
Instance: Params (@bi_plainly) 1.
@@ -218,7 +215,6 @@ Arguments bi_or {PROP} _%I _%I : simpl never, rename.
Arguments bi_impl {PROP} _%I _%I : simpl never, rename.
Arguments bi_forall {PROP _} _%I : simpl never, rename.
Arguments bi_exist {PROP _} _%I : simpl never, rename.
-Arguments bi_internal_eq {PROP _} _ _ : simpl never, rename.
Arguments bi_sep {PROP} _%I _%I : simpl never, rename.
Arguments bi_wand {PROP} _%I _%I : simpl never, rename.
Arguments bi_plainly {PROP} _%I : simpl never, rename.
@@ -236,35 +232,26 @@ Structure sbi := Sbi {
sbi_impl : sbi_car → sbi_car → sbi_car;
sbi_forall : ∀ A, (A → sbi_car) → sbi_car;
sbi_exist : ∀ A, (A → sbi_car) → sbi_car;
- sbi_internal_eq : ∀ A : ofeT, A → A → sbi_car;
sbi_sep : sbi_car → sbi_car → sbi_car;
sbi_wand : sbi_car → sbi_car → sbi_car;
sbi_plainly : sbi_car → sbi_car;
sbi_persistently : sbi_car → sbi_car;
+ sbi_internal_eq : ∀ A : ofeT, A → A → sbi_car;
sbi_later : sbi_car → sbi_car;
sbi_ofe_mixin : OfeMixin sbi_car;
- sbi_bi_mixin : BiMixin sbi_ofe_mixin sbi_entails sbi_emp sbi_pure sbi_and
- sbi_or sbi_impl sbi_forall sbi_exist sbi_internal_eq
- sbi_sep sbi_wand sbi_plainly sbi_persistently;
- sbi_sbi_mixin : SbiMixin sbi_entails sbi_pure sbi_or sbi_impl
- sbi_forall sbi_exist sbi_internal_eq
- sbi_sep sbi_plainly sbi_persistently sbi_later;
+ sbi_bi_mixin : BiMixin sbi_entails sbi_emp sbi_pure sbi_and sbi_or sbi_impl
+ sbi_forall sbi_exist sbi_sep sbi_wand sbi_plainly
+ sbi_persistently;
+ sbi_sbi_mixin : SbiMixin sbi_ofe_mixin sbi_entails sbi_pure sbi_and sbi_or
+ sbi_impl sbi_forall sbi_exist sbi_sep sbi_plainly
+ sbi_persistently sbi_internal_eq sbi_later;
}.
-Arguments sbi_car : simpl never.
-Arguments sbi_entails {PROP} _%I _%I : simpl never, rename.
-Arguments bi_emp {PROP} : simpl never, rename.
-Arguments bi_pure {PROP} _%stdpp : simpl never, rename.
-Arguments bi_and {PROP} _%I _%I : simpl never, rename.
-Arguments bi_or {PROP} _%I _%I : simpl never, rename.
-Arguments bi_impl {PROP} _%I _%I : simpl never, rename.
-Arguments bi_forall {PROP _} _%I : simpl never, rename.
-Arguments bi_exist {PROP _} _%I : simpl never, rename.
-Arguments bi_internal_eq {PROP _} _ _ : simpl never, rename.
-Arguments bi_sep {PROP} _%I _%I : simpl never, rename.
-Arguments bi_wand {PROP} _%I _%I : simpl never, rename.
-Arguments bi_plainly {PROP} _%I : simpl never, rename.
-Arguments bi_persistently {PROP} _%I : simpl never, rename.
+Instance: Params (@sbi_later) 1.
+Instance: Params (@sbi_internal_eq) 1.
+
+Arguments sbi_later {PROP} _%I : simpl never, rename.
+Arguments sbi_internal_eq {PROP _} _ _ : simpl never, rename.
Coercion sbi_ofeC (PROP : sbi) : ofeT := OfeT PROP (sbi_ofe_mixin PROP).
Canonical Structure sbi_ofeC.
@@ -283,11 +270,11 @@ Arguments sbi_or {PROP} _%I _%I : simpl never, rename.
Arguments sbi_impl {PROP} _%I _%I : simpl never, rename.
Arguments sbi_forall {PROP _} _%I : simpl never, rename.
Arguments sbi_exist {PROP _} _%I : simpl never, rename.
-Arguments sbi_internal_eq {PROP _} _ _ : simpl never, rename.
Arguments sbi_sep {PROP} _%I _%I : simpl never, rename.
Arguments sbi_wand {PROP} _%I _%I : simpl never, rename.
Arguments sbi_plainly {PROP} _%I : simpl never, rename.
Arguments sbi_persistently {PROP} _%I : simpl never, rename.
+Arguments sbi_internal_eq {PROP _} _ _ : simpl never, rename.
Arguments sbi_later {PROP} _%I : simpl never, rename.
Hint Extern 0 (bi_entails _ _) => reflexivity.
@@ -320,7 +307,7 @@ Notation "∀ x .. y , P" :=
Notation "∃ x .. y , P" :=
(bi_exist (λ x, .. (bi_exist (λ y, P)) ..)%I) : bi_scope.
-Infix "≡" := bi_internal_eq : bi_scope.
+Infix "≡" := sbi_internal_eq : bi_scope.
Notation "â–· P" := (sbi_later P) : bi_scope.
Coercion bi_valid {PROP : bi} (P : PROP) : Prop := emp ⊢ P.
@@ -396,31 +383,13 @@ Proof. eapply bi_mixin_impl_elim_l', bi_bi_mixin. Qed.
Lemma forall_intro {A} P (Ψ : A → PROP) : (∀ a, P ⊢ Ψ a) → P ⊢ ∀ a, Ψ a.
Proof. eapply bi_mixin_forall_intro, bi_bi_mixin. Qed.
Lemma forall_elim {A} {Ψ : A → PROP} a : (∀ a, Ψ a) ⊢ Ψ a.
-Proof. eapply (bi_mixin_forall_elim _ bi_entails), bi_bi_mixin. Qed.
+Proof. eapply (bi_mixin_forall_elim bi_entails), bi_bi_mixin. Qed.
Lemma exist_intro {A} {Ψ : A → PROP} a : Ψ a ⊢ ∃ a, Ψ a.
Proof. eapply bi_mixin_exist_intro, bi_bi_mixin. Qed.
Lemma exist_elim {A} (Φ : A → PROP) Q : (∀ a, Φ a ⊢ Q) → (∃ a, Φ a) ⊢ Q.
Proof. eapply bi_mixin_exist_elim, bi_bi_mixin. Qed.
-(* Equality *)
-Global Instance internal_eq_ne (A : ofeT) : NonExpansive2 (@bi_internal_eq PROP A).
-Proof. eapply bi_mixin_internal_eq_ne, bi_bi_mixin. Qed.
-
-Lemma internal_eq_refl {A : ofeT} P (a : A) : P ⊢ a ≡ a.
-Proof. eapply bi_mixin_internal_eq_refl, bi_bi_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_bi_mixin. Qed.
-
-Lemma fun_ext {A} {B : A → ofeT} (f g : ofe_fun B) : (∀ x, f x ≡ g x) ⊢ (f ≡ g : PROP).
-Proof. eapply bi_mixin_fun_ext, bi_bi_mixin. Qed.
-Lemma sig_eq {A : ofeT} (P : A → Prop) (x y : sig P) : `x ≡ `y ⊢ (x ≡ y : PROP).
-Proof. eapply bi_mixin_sig_eq, bi_bi_mixin. Qed.
-Lemma discrete_eq_1 {A : ofeT} (a b : A) :
- Discrete a → a ≡ b ⊢ (⌜a ≡ b⌠: PROP).
-Proof. eapply bi_mixin_discrete_eq_1, bi_bi_mixin. Qed.
-
(* BI connectives *)
Lemma sep_mono P P' Q Q' : (P ⊢ Q) → (P' ⊢ Q') → P ∗ P' ⊢ Q ∗ Q'.
Proof. eapply bi_mixin_sep_mono, bi_bi_mixin. Qed.
@@ -429,7 +398,7 @@ Proof. eapply bi_mixin_emp_sep_1, bi_bi_mixin. Qed.
Lemma emp_sep_2 P : emp ∗ P ⊢ P.
Proof. eapply bi_mixin_emp_sep_2, bi_bi_mixin. Qed.
Lemma sep_comm' P Q : P ∗ Q ⊢ Q ∗ P.
-Proof. eapply (bi_mixin_sep_comm' _ bi_entails), bi_bi_mixin. Qed.
+Proof. eapply (bi_mixin_sep_comm' bi_entails), bi_bi_mixin. Qed.
Lemma sep_assoc' P Q R : (P ∗ Q) ∗ R ⊢ P ∗ (Q ∗ R).
Proof. eapply bi_mixin_sep_assoc', bi_bi_mixin. Qed.
Lemma wand_intro_r P Q R : (P ∗ Q ⊢ R) → P ⊢ Q -∗ R.
@@ -447,8 +416,6 @@ Proof. eapply bi_mixin_plainly_idemp_2, bi_bi_mixin. Qed.
Lemma plainly_forall_2 {A} (Ψ : A → PROP) :
(∀ a, bi_plainly (Ψ a)) ⊢ bi_plainly (∀ a, Ψ a).
Proof. eapply bi_mixin_plainly_forall_2, bi_bi_mixin. Qed.
-Lemma prop_ext P Q : bi_plainly ((P → Q) ∧ (Q → P)) ⊢ P ≡ Q.
-Proof. eapply (bi_mixin_prop_ext _ bi_entails), bi_bi_mixin. Qed.
Lemma persistently_impl_plainly P Q :
(bi_plainly P → bi_persistently Q) ⊢ bi_persistently (bi_plainly P → Q).
Proof. eapply bi_mixin_persistently_impl_plainly, bi_bi_mixin. Qed.
@@ -456,7 +423,7 @@ Lemma plainly_impl_plainly P Q :
(bi_plainly P → bi_plainly Q) ⊢ bi_plainly (bi_plainly P → Q).
Proof. eapply bi_mixin_plainly_impl_plainly, bi_bi_mixin. Qed.
Lemma plainly_absorbing P Q : bi_plainly P ∗ Q ⊢ bi_plainly P.
-Proof. eapply (bi_mixin_plainly_absorbing _ bi_entails), bi_bi_mixin. Qed.
+Proof. eapply (bi_mixin_plainly_absorbing bi_entails), bi_bi_mixin. Qed.
Lemma plainly_emp_intro P : P ⊢ bi_plainly emp.
Proof. eapply bi_mixin_plainly_emp_intro, bi_bi_mixin. Qed.
@@ -468,7 +435,7 @@ Lemma persistently_idemp_2 P :
Proof. eapply bi_mixin_persistently_idemp_2, bi_bi_mixin. Qed.
Lemma plainly_persistently_1 P :
bi_plainly (bi_persistently P) ⊢ bi_plainly P.
-Proof. eapply (bi_mixin_plainly_persistently_1 _ bi_entails), bi_bi_mixin. Qed.
+Proof. eapply (bi_mixin_plainly_persistently_1 bi_entails), bi_bi_mixin. Qed.
Lemma persistently_forall_2 {A} (Ψ : A → PROP) :
(∀ a, bi_persistently (Ψ a)) ⊢ bi_persistently (∀ a, Ψ a).
@@ -478,7 +445,7 @@ Lemma persistently_exist_1 {A} (Ψ : A → PROP) :
Proof. eapply bi_mixin_persistently_exist_1, bi_bi_mixin. Qed.
Lemma persistently_absorbing P Q : bi_persistently P ∗ Q ⊢ bi_persistently P.
-Proof. eapply (bi_mixin_persistently_absorbing _ bi_entails), bi_bi_mixin. Qed.
+Proof. eapply (bi_mixin_persistently_absorbing bi_entails), bi_bi_mixin. Qed.
Lemma persistently_and_sep_elim P Q : bi_persistently P ∧ Q ⊢ (emp ∧ P) ∗ Q.
Proof. eapply bi_mixin_persistently_and_sep_elim, bi_bi_mixin. Qed.
End bi_laws.
@@ -488,6 +455,28 @@ Context {PROP : sbi}.
Implicit Types φ : Prop.
Implicit Types P Q R : PROP.
+(* Equality *)
+Global Instance internal_eq_ne (A : ofeT) : NonExpansive2 (@sbi_internal_eq PROP A).
+Proof. eapply sbi_mixin_internal_eq_ne, sbi_sbi_mixin. Qed.
+
+Lemma internal_eq_refl {A : ofeT} P (a : A) : P ⊢ a ≡ a.
+Proof. eapply sbi_mixin_internal_eq_refl, sbi_sbi_mixin. Qed.
+Lemma internal_eq_rewrite {A : ofeT} a b (Ψ : A → PROP) :
+ NonExpansive Ψ → a ≡ b ⊢ Ψ a → Ψ b.
+Proof. eapply sbi_mixin_internal_eq_rewrite, sbi_sbi_mixin. Qed.
+
+Lemma fun_ext {A} {B : A → ofeT} (f g : ofe_fun B) : (∀ x, f x ≡ g x) ⊢ (f ≡ g : PROP).
+Proof. eapply sbi_mixin_fun_ext, sbi_sbi_mixin. Qed.
+Lemma sig_eq {A : ofeT} (P : A → Prop) (x y : sig P) : `x ≡ `y ⊢ (x ≡ y : PROP).
+Proof. eapply sbi_mixin_sig_eq, sbi_sbi_mixin. Qed.
+Lemma discrete_eq_1 {A : ofeT} (a b : A) :
+ Discrete a → a ≡ b ⊢ (⌜a ≡ b⌠: PROP).
+Proof. eapply sbi_mixin_discrete_eq_1, sbi_sbi_mixin. Qed.
+
+Lemma prop_ext P Q : bi_plainly ((P → Q) ∧ (Q → P)) ⊢ P ≡ Q.
+Proof. eapply (sbi_mixin_prop_ext _ bi_entails), sbi_sbi_mixin. Qed.
+
+(* Later *)
Global Instance later_contractive : Contractive (@sbi_later PROP).
Proof. eapply sbi_mixin_later_contractive, sbi_sbi_mixin. Qed.
@@ -511,13 +500,13 @@ Proof. eapply sbi_mixin_later_sep_1, sbi_sbi_mixin. Qed.
Lemma later_sep_2 P Q : ▷ P ∗ ▷ Q ⊢ ▷ (P ∗ Q).
Proof. eapply sbi_mixin_later_sep_2, sbi_sbi_mixin. Qed.
Lemma later_plainly_1 P : ▷ bi_plainly P ⊢ bi_plainly (▷ P).
-Proof. eapply (sbi_mixin_later_plainly_1 bi_entails), sbi_sbi_mixin. Qed.
+Proof. eapply (sbi_mixin_later_plainly_1 _ bi_entails), sbi_sbi_mixin. Qed.
Lemma later_plainly_2 P : bi_plainly (▷ P) ⊢ ▷ bi_plainly P.
-Proof. eapply (sbi_mixin_later_plainly_2 bi_entails), sbi_sbi_mixin. Qed.
+Proof. eapply (sbi_mixin_later_plainly_2 _ bi_entails), sbi_sbi_mixin. Qed.
Lemma later_persistently_1 P : ▷ bi_persistently P ⊢ bi_persistently (▷ P).
-Proof. eapply (sbi_mixin_later_persistently_1 bi_entails), sbi_sbi_mixin. Qed.
+Proof. eapply (sbi_mixin_later_persistently_1 _ bi_entails), sbi_sbi_mixin. Qed.
Lemma later_persistently_2 P : bi_persistently (▷ P) ⊢ ▷ bi_persistently P.
-Proof. eapply (sbi_mixin_later_persistently_2 bi_entails), sbi_sbi_mixin. Qed.
+Proof. eapply (sbi_mixin_later_persistently_2 _ bi_entails), sbi_sbi_mixin. Qed.
Lemma later_false_em P : ▷ P ⊢ ▷ False ∨ (▷ False → P).
Proof. eapply sbi_mixin_later_false_em, sbi_sbi_mixin. Qed.
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index c839b5556..3cf4df992 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -131,7 +131,6 @@ Definition monPred_embed_eq : bi_embed (A:=PROP) = _ := seal_eq _.
Definition monPred_pure (φ : Prop) : monPred := tc_opaque ⎡⌜φâŒâŽ¤%I.
Definition monPred_emp : monPred := tc_opaque ⎡emp⎤%I.
-Definition monPred_internal_eq (A : ofeT) (a b : A) : monPred := tc_opaque ⎡a ≡ b⎤%I.
Definition monPred_plainly P : monPred := tc_opaque ⎡∀ i, bi_plainly (P i)⎤%I.
Definition monPred_all (P : monPred) : monPred := tc_opaque ⎡∀ i, P i⎤%I.
Definition monPred_ex (P : monPred) : monPred := tc_opaque ⎡∃ i, P i⎤%I.
@@ -216,6 +215,8 @@ Implicit Types i : I.
Notation monPred := (monPred I PROP).
Implicit Types P Q : monPred.
+Definition monPred_internal_eq (A : ofeT) (a b : A) : monPred := tc_opaque ⎡a ≡ b⎤%I.
+
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. by eexists. Qed.
@@ -243,7 +244,7 @@ Definition unseal_eqs :=
Ltac unseal :=
unfold bi_affinely, bi_absorbingly, sbi_except_0, bi_pure, bi_emp,
monPred_all, monPred_ex, 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, sbi_internal_eq, bi_sep, bi_wand,
bi_persistently, bi_affinely, sbi_later;
simpl;
unfold sbi_emp, sbi_pure, sbi_and, sbi_or, sbi_impl, sbi_forall, sbi_exist,
@@ -257,13 +258,12 @@ Import MonPred.
Section canonical_bi.
Context (I : biIndex) (PROP : bi).
-Lemma monPred_bi_mixin : BiMixin (@monPred_ofe_mixin I PROP)
+Lemma monPred_bi_mixin : BiMixin (PROP:=monPred I PROP)
monPred_entails monPred_emp monPred_pure monPred_and monPred_or
- monPred_impl monPred_forall monPred_exist monPred_internal_eq
- monPred_sep monPred_wand monPred_plainly monPred_persistently.
+ monPred_impl monPred_forall monPred_exist monPred_sep monPred_wand
+ monPred_plainly monPred_persistently.
Proof.
- split; try unseal;
- try by (repeat intro; split=> ? /=; repeat f_equiv).
+ split; try unseal; try by (split=> ? /=; repeat f_equiv).
- split.
+ intros P. by split.
+ intros P Q R [H1] [H2]. split => ?. by rewrite H1 H2.
@@ -289,13 +289,6 @@ Proof.
- intros A Ψ. split=> i. by apply: bi.forall_elim.
- intros A Ψ a. split=> i. by rewrite /= -bi.exist_intro.
- intros A Ψ Q HΨ. split=> i. apply bi.exist_elim => a. by apply HΨ.
- - 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 P P' Q Q' [?] [?]. split=> i. by apply bi.sep_mono.
- intros P. split=> i. by apply bi.emp_sep_1.
- intros P. split=> i. by apply bi.emp_sep_2.
@@ -313,11 +306,6 @@ Proof.
- intros A Ψ. split=> i /=. apply bi.forall_intro=> j.
rewrite bi.plainly_forall. apply bi.forall_intro=> a.
by rewrite !bi.forall_elim.
- - intros P Q. split=> i /=.
- rewrite <-(sig_monPred_sig P), <-(sig_monPred_sig Q), <-(bi.f_equiv _).
- rewrite -bi.sig_equivI /= -bi.fun_ext. f_equiv=> j.
- rewrite -bi.prop_ext !(bi.forall_elim j) !bi.pure_impl_forall
- !bi.forall_elim //.
- intros P Q. split=> i /=. repeat setoid_rewrite bi.pure_impl_forall.
repeat setoid_rewrite <-bi.plainly_forall.
repeat setoid_rewrite bi.persistently_forall. do 4 f_equiv.
@@ -341,21 +329,35 @@ Qed.
Canonical Structure monPredI : bi :=
Bi (monPred I PROP) monPred_dist monPred_equiv monPred_entails monPred_emp
monPred_pure monPred_and monPred_or monPred_impl monPred_forall
- monPred_exist monPred_internal_eq monPred_sep monPred_wand monPred_plainly
- monPred_persistently monPred_ofe_mixin monPred_bi_mixin.
+ monPred_exist monPred_sep monPred_wand monPred_plainly monPred_persistently
+ monPred_ofe_mixin monPred_bi_mixin.
End canonical_bi.
Section canonical_sbi.
Context (I : biIndex) (PROP : sbi).
Lemma monPred_sbi_mixin :
- SbiMixin (PROP:=monPred I PROP) monPred_entails monPred_pure monPred_or
- monPred_impl monPred_forall monPred_exist monPred_internal_eq
- monPred_sep monPred_plainly monPred_persistently monPred_later.
+ SbiMixin (PROP:=monPred I PROP) monPred_ofe_mixin monPred_entails monPred_pure
+ monPred_and monPred_or monPred_impl monPred_forall monPred_exist
+ monPred_sep monPred_plainly monPred_persistently monPred_internal_eq
+ monPred_later.
Proof.
split; unseal.
- intros n P Q HPQ. split=> i /=.
apply bi.later_contractive. destruct n as [|n]=> //. by apply HPQ.
+ - 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 P Q. split=> i /=.
+ rewrite <-(sig_monPred_sig P), <-(sig_monPred_sig Q), <-(bi.f_equiv _).
+ rewrite -bi.sig_equivI /= -bi.fun_ext. f_equiv=> j.
+ rewrite -bi.prop_ext !(bi.forall_elim j) !bi.pure_impl_forall
+ !bi.forall_elim //.
- 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.
@@ -378,8 +380,8 @@ Qed.
Canonical Structure monPredSI : sbi :=
Sbi (monPred I PROP) monPred_dist monPred_equiv monPred_entails monPred_emp
monPred_pure monPred_and monPred_or monPred_impl monPred_forall
- monPred_exist monPred_internal_eq monPred_sep monPred_wand monPred_plainly
- monPred_persistently monPred_later monPred_ofe_mixin
+ monPred_exist monPred_sep monPred_wand monPred_plainly
+ monPred_persistently monPred_internal_eq monPred_later monPred_ofe_mixin
(bi_bi_mixin _) monPred_sbi_mixin.
End canonical_sbi.
@@ -523,8 +525,6 @@ Lemma monPred_at_pure i (φ : Prop) : monPred_at ⌜φ⌠i ⊣⊢ ⌜φâŒ.
Proof. by apply monPred_at_embed. Qed.
Lemma monPred_at_emp i : monPred_at emp i ⊣⊢ emp.
Proof. by apply monPred_at_embed. Qed.
-Lemma monPred_at_internal_eq {A : ofeT} i (a b : A) : monPred_at (a ≡ b) i ⊣⊢ a ≡ b.
-Proof. by apply monPred_at_embed. Qed.
Lemma monPred_at_plainly i P : bi_plainly P i ⊣⊢ ∀ j, bi_plainly (P j).
Proof. by apply monPred_at_embed. Qed.
Lemma monPred_at_and i P Q : (P ∧ Q) i ⊣⊢ P i ∧ Q i.
@@ -620,15 +620,6 @@ Proof.
eapply bi.pure_elim; [apply bi.and_elim_l|]=>?. rewrite bi.and_elim_r. by f_equiv.
Qed.
-Lemma monPred_equivI {PROP' : bi} P Q :
- bi_internal_eq (PROP:=PROP') P Q ⊣⊢ ∀ i, P i ≡ Q i.
-Proof.
- apply bi.equiv_spec. split.
- - apply bi.forall_intro=>?. apply (bi.f_equiv (flip monPred_at _)).
- - by rewrite -{2}(sig_monPred_sig P) -{2}(sig_monPred_sig Q)
- -bi.f_equiv -bi.sig_equivI !bi.ofe_fun_equivI.
-Qed.
-
Lemma monPred_bupd_embed `{BUpdFacts PROP} (P : PROP) :
⎡|==> P⎤ ⊣⊢ bupd (PROP:=monPredI) ⎡P⎤.
Proof.
@@ -734,7 +725,7 @@ Proof.
Qed.
Global Instance monPred_sbi_embedding : SbiEmbedding PROP monPredSI.
-Proof. split; try apply _. by unseal. Qed.
+Proof. split; try apply _; by unseal. Qed.
Global Instance monPred_fupd_facts `{FUpdFacts PROP} : FUpdFacts monPredSI.
Proof.
@@ -766,6 +757,9 @@ Qed.
(** Unfolding lemmas *)
+Lemma monPred_at_internal_eq {A : ofeT} i (a b : A) :
+ @monPred_at I PROP (a ≡ b) i ⊣⊢ a ≡ b.
+Proof. by apply monPred_at_embed. Qed.
Lemma monPred_at_later i P : (▷ P) i ⊣⊢ ▷ P i.
Proof. by unseal. Qed.
Lemma monPred_at_fupd `{FUpdFacts PROP} i E1 E2 P :
@@ -785,4 +779,13 @@ Proof.
- by do 2 apply bi.forall_intro=>?.
- rewrite !bi.forall_elim //.
Qed.
+
+Lemma monPred_equivI {PROP' : sbi} P Q :
+ sbi_internal_eq (PROP:=PROP') P Q ⊣⊢ ∀ i, P i ≡ Q i.
+Proof.
+ apply bi.equiv_spec. split.
+ - apply bi.forall_intro=>?. apply (bi.f_equiv (flip monPred_at _)).
+ - by rewrite -{2}(sig_monPred_sig P) -{2}(sig_monPred_sig Q)
+ -bi.f_equiv -bi.sig_equivI !bi.ofe_fun_equivI.
+Qed.
End sbi_facts.
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index fb9522f0d..b810e6d4b 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -81,10 +81,6 @@ Proof. rewrite /FromAssumption=>->. apply bupd_intro. Qed.
Global Instance into_pure_pure φ : @IntoPure PROP ⌜φ⌠φ.
Proof. by rewrite /IntoPure. Qed.
-Global Instance into_pure_eq {A : ofeT} (a b : A) :
- Discrete a → @IntoPure M (a ≡ b) (a ≡ b).
-Proof. intros. by rewrite /IntoPure discrete_eq. Qed.
-
Global Instance into_pure_pure_and (φ1 φ2 : Prop) P1 P2 :
IntoPure P1 φ1 → IntoPure P2 φ2 → IntoPure (P1 ∧ P2) (φ1 ∧ φ2).
Proof. rewrite /IntoPure pure_and. by intros -> ->. Qed.
@@ -126,10 +122,6 @@ Proof. rewrite /IntoPure=> ->. by rewrite bi_embed_pure. Qed.
(* FromPure *)
Global Instance from_pure_pure φ : @FromPure PROP ⌜φ⌠φ.
Proof. by rewrite /FromPure. Qed.
-Global Instance from_pure_internal_eq {A : ofeT} (a b : A) :
- @FromPure PROP (a ≡ b) (a ≡ b).
-Proof. by rewrite /FromPure pure_internal_eq. Qed.
-
Global Instance from_pure_pure_and (φ1 φ2 : Prop) P1 P2 :
FromPure P1 φ1 → FromPure P2 φ2 → FromPure (P1 ∧ P2) (φ1 ∧ φ2).
Proof. rewrite /FromPure pure_and. by intros -> ->. Qed.
@@ -176,27 +168,6 @@ Global Instance from_pure_bupd `{BUpdFacts PROP} P φ :
FromPure P φ → FromPure (|==> P) φ.
Proof. rewrite /FromPure=> ->. apply bupd_intro. 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 (bi_affinely P) x y.
-Proof. rewrite /IntoInternalEq=> ->. by rewrite affinely_elim. Qed.
-Global Instance into_internal_eq_absorbingly {A : ofeT} (x y : A) P :
- IntoInternalEq P x y → IntoInternalEq (bi_absorbingly P) x y.
-Proof. rewrite /IntoInternalEq=> ->. by rewrite absorbingly_internal_eq. Qed.
-Global Instance into_internal_eq_plainly {A : ofeT} (x y : A) P :
- IntoInternalEq P x y → IntoInternalEq (bi_plainly 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 (bi_persistently P) x y.
-Proof. rewrite /IntoInternalEq=> ->. by rewrite persistently_elim. Qed.
-Global Instance into_internal_eq_embed
- `{BiEmbedding PROP PROP'} {A : ofeT} (x y : A) P :
- IntoInternalEq P x y → IntoInternalEq ⎡P⎤ x y.
-Proof. rewrite /IntoInternalEq=> ->. by rewrite bi_embed_internal_eq. Qed.
-
(* IntoPersistent *)
Global Instance into_persistent_persistently p P Q :
IntoPersistent true P Q → IntoPersistent p (bi_persistently P) Q | 0.
@@ -841,10 +812,6 @@ Qed.
Global Instance frame_pure_embed `{BiEmbedding PROP PROP'} p P Q (Q' : PROP') φ :
Frame p ⌜φ⌠P Q → MakeEmbed Q Q' → Frame p ⌜φ⌠⎡P⎤ Q'.
Proof. rewrite /Frame /MakeEmbed -bi_embed_pure. apply (frame_embed p P Q). Qed.
-Global Instance frame_eq_embed `{BiEmbedding 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 -bi_embed_internal_eq. apply (frame_embed p P Q). Qed.
Class MakeSep (P Q PQ : PROP) := make_sep : P ∗ Q ⊣⊢ PQ.
Arguments MakeSep _%I _%I _%I.
@@ -1087,6 +1054,9 @@ Global Instance from_assumption_fupd `{FUpdFacts PROP} E p P Q :
Proof. rewrite /FromAssumption=>->. apply bupd_fupd. Qed.
(* FromPure *)
+Global Instance from_pure_internal_eq {A : ofeT} (a b : A) :
+ @FromPure PROP (a ≡ b) (a ≡ b).
+Proof. by rewrite /FromPure pure_internal_eq. Qed.
Global Instance from_pure_later P φ : FromPure P φ → FromPure (▷ P) φ.
Proof. rewrite /FromPure=> ->. apply later_intro. Qed.
Global Instance from_pure_laterN n P φ : FromPure P φ → FromPure (▷^n P) φ.
@@ -1097,6 +1067,11 @@ Global Instance from_pure_fupd `{FUpdFacts PROP} E P φ :
FromPure P φ → FromPure (|={E}=> P) φ.
Proof. rewrite /FromPure. intros <-. apply fupd_intro. Qed.
+(* IntoPure *)
+Global Instance into_pure_eq {A : ofeT} (a b : A) :
+ Discrete a → @IntoPure PROP (a ≡ b) (a ≡ b).
+Proof. intros. by rewrite /IntoPure discrete_eq. Qed.
+
(* IntoWand *)
Global Instance into_wand_later p q R P Q :
IntoWand p q R P Q → IntoWand p q (▷ R) (▷ P) (▷ Q).
@@ -1331,6 +1306,27 @@ Proof. apply except_0_intro. Qed.
Global Instance from_modal_fupd E P `{FUpdFacts PROP} : FromModal (|={E}=> P) P.
Proof. rewrite /FromModal. apply fupd_intro. 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 (bi_affinely P) x y.
+Proof. rewrite /IntoInternalEq=> ->. by rewrite affinely_elim. Qed.
+Global Instance into_internal_eq_absorbingly {A : ofeT} (x y : A) P :
+ IntoInternalEq P x y → IntoInternalEq (bi_absorbingly P) x y.
+Proof. rewrite /IntoInternalEq=> ->. by rewrite absorbingly_internal_eq. Qed.
+Global Instance into_internal_eq_plainly {A : ofeT} (x y : A) P :
+ IntoInternalEq P x y → IntoInternalEq (bi_plainly 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 (bi_persistently P) x y.
+Proof. rewrite /IntoInternalEq=> ->. by rewrite persistently_elim. Qed.
+Global Instance into_internal_eq_embed
+ `{SbiEmbedding PROP PROP'} {A : ofeT} (x y : A) P :
+ IntoInternalEq P x y → IntoInternalEq ⎡P⎤ x y.
+Proof. rewrite /IntoInternalEq=> ->. by rewrite sbi_embed_internal_eq. Qed.
+
(* IntoExcept0 *)
Global Instance into_except_0_except_0 P : IntoExcept0 (â—‡ P) P.
Proof. by rewrite /IntoExcept0. Qed.
@@ -1400,6 +1396,11 @@ Global Instance add_modal_fupd `{FUpdFacts PROP} E1 E2 P Q :
Proof. by rewrite /AddModal fupd_frame_r wand_elim_r fupd_trans. Qed.
(* Frame *)
+Global Instance frame_eq_embed `{SbiEmbedding 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 -sbi_embed_internal_eq. apply (frame_embed p P Q). Qed.
+
Class MakeLater (P lP : PROP) := make_later : ▷ P ⊣⊢ lP.
Arguments MakeLater _%I _%I.
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 97302e81f..0fc192266 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -56,7 +56,7 @@ 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 {PROP : sbi} {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 {_}.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index f5edbdb2f..7515e956b 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -914,43 +914,6 @@ Proof.
by rewrite into_wand /= HP1 wand_elim_l.
Qed.
-(** * Rewriting *)
-Lemma tac_rewrite Δ i p Pxy d Q :
- envs_lookup i Δ = Some (p, Pxy) →
- ∀ {A : ofeT} (x y : A) (Φ : A → PROP),
- IntoInternalEq Pxy x y →
- (Q ⊣⊢ Φ (if d is Left then y else x)) →
- NonExpansive Φ →
- envs_entails Δ (Φ (if d is Left then x else y)) → envs_entails Δ Q.
-Proof.
- intros ? A x y ? HPxy -> ?; apply internal_eq_rewrite'; auto.
- rewrite {1}envs_lookup_sound //.
- rewrite HPxy affinely_persistently_if_elim sep_elim_l.
- destruct d; auto using internal_eq_sym.
-Qed.
-
-Lemma tac_rewrite_in Δ 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),
- IntoInternalEq Pxy x y →
- (P ⊣⊢ Φ (if d is Left then y else x)) →
- NonExpansive Φ →
- envs_simple_replace j q (Esnoc Enil j (Φ (if d is Left then x else y))) Δ = Some Δ' →
- envs_entails Δ' Q →
- envs_entails Δ Q.
-Proof.
- rewrite /envs_entails => ?? A Δ' x y Φ HPxy HP ?? <-.
- rewrite -(idemp bi_and (of_envs Δ)) {2}(envs_lookup_sound _ i) //.
- rewrite (envs_simple_replace_singleton_sound _ _ j) //=.
- rewrite HP HPxy (affinely_persistently_if_elim _ (_ ≡ _)%I) sep_elim_l.
- rewrite persistent_and_affinely_sep_r -assoc. apply wand_elim_r'.
- rewrite -persistent_and_affinely_sep_r. apply impl_elim_r'. destruct d.
- - apply (internal_eq_rewrite x y (λ y, □?q Φ y -∗ of_envs Δ')%I). solve_proper.
- - rewrite internal_eq_sym.
- eapply (internal_eq_rewrite y x (λ y, □?q Φ y -∗ of_envs Δ')%I). solve_proper.
-Qed.
-
(** * Conjunction splitting *)
Lemma tac_and_split Δ P Q1 Q2 :
FromAnd P Q1 Q2 → envs_entails Δ Q1 → envs_entails Δ Q2 → envs_entails Δ P.
@@ -1140,6 +1103,43 @@ Implicit Types Γ : env PROP.
Implicit Types Δ : envs PROP.
Implicit Types P Q : PROP.
+(** * Rewriting *)
+Lemma tac_rewrite Δ i p Pxy d Q :
+ envs_lookup i Δ = Some (p, Pxy) →
+ ∀ {A : ofeT} (x y : A) (Φ : A → PROP),
+ IntoInternalEq Pxy x y →
+ (Q ⊣⊢ Φ (if d is Left then y else x)) →
+ NonExpansive Φ →
+ envs_entails Δ (Φ (if d is Left then x else y)) → envs_entails Δ Q.
+Proof.
+ intros ? A x y ? HPxy -> ?; apply internal_eq_rewrite'; auto.
+ rewrite {1}envs_lookup_sound //.
+ rewrite (into_internal_eq Pxy x y) affinely_persistently_if_elim sep_elim_l.
+ destruct d; auto using internal_eq_sym.
+Qed.
+
+Lemma tac_rewrite_in Δ 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),
+ IntoInternalEq Pxy x y →
+ (P ⊣⊢ Φ (if d is Left then y else x)) →
+ NonExpansive Φ →
+ envs_simple_replace j q (Esnoc Enil j (Φ (if d is Left then x else y))) Δ = Some Δ' →
+ envs_entails Δ' Q →
+ envs_entails Δ Q.
+Proof.
+ rewrite /envs_entails /IntoInternalEq => ?? A Δ' x y Φ HPxy HP ?? <-.
+ rewrite -(idemp bi_and (of_envs Δ)) {2}(envs_lookup_sound _ i) //.
+ rewrite (envs_simple_replace_singleton_sound _ _ j) //=.
+ rewrite HP HPxy (affinely_persistently_if_elim _ (_ ≡ _)%I) sep_elim_l.
+ rewrite persistent_and_affinely_sep_r -assoc. apply wand_elim_r'.
+ rewrite -persistent_and_affinely_sep_r. apply impl_elim_r'. destruct d.
+ - apply (internal_eq_rewrite x y (λ y, □?q Φ y -∗ of_envs Δ')%I). solve_proper.
+ - rewrite internal_eq_sym.
+ eapply (internal_eq_rewrite y x (λ y, □?q Φ y -∗ of_envs Δ')%I). solve_proper.
+Qed.
+
(** * Later *)
Class IntoLaterNEnv (n : nat) (Γ1 Γ2 : env PROP) :=
into_laterN_env : env_Forall2 (IntoLaterN n) Γ1 Γ2.
diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index 588e30942..863602c68 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -25,9 +25,6 @@ Implicit Types i j : I.
Global Instance make_monPred_at_pure φ i : MakeMonPredAt i ⌜φ⌠⌜φâŒ.
Proof. by rewrite /MakeMonPredAt monPred_at_pure. Qed.
-Global Instance make_monPred_at_internal_eq {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_emp i : MakeMonPredAt i emp emp.
Proof. by rewrite /MakeMonPredAt monPred_at_emp. Qed.
Global Instance make_monPred_at_sep i P ð“Ÿ Q ð“ :
@@ -133,10 +130,6 @@ Proof. by rewrite /IntoPure monPred_at_in. Qed.
Global Instance from_pure_monPred_in i j : @FromPure PROP (monPred_in i j) (i ⊑ j).
Proof. by rewrite /FromPure monPred_at_in. Qed.
-Global Instance into_internal_eq_monPred_at {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.
-
Global Instance into_persistent_monPred_at p P Q ð“ i :
IntoPersistent p P Q → MakeMonPredAt i Q ð“ → IntoPersistent p (P i) ð“ | 0.
Proof.
@@ -391,6 +384,9 @@ 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 :
+ @MakeMonPredAt I PROP 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.
Proof. by rewrite /MakeMonPredAt monPred_at_except_0=><-. Qed.
@@ -404,6 +400,10 @@ Global Instance make_monPred_at_fupd `{FUpdFacts 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 :
+ IntoInternalEq P x y → IntoInternalEq (P i) x y.
+Proof. rewrite /IntoInternalEq=> ->. by rewrite monPred_at_internal_eq. Qed.
+
Global Instance into_except_0_monPred_at_fwd i P Q ð“ :
IntoExcept0 P Q → MakeMonPredAt i Q ð“ → IntoExcept0 (P i) ð“ .
Proof. rewrite /IntoExcept0 /MakeMonPredAt=> -> <-. by rewrite monPred_at_except_0. Qed.
--
GitLab