Skip to content

GitLab

Commit 30a36cf2 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Move internal_eq in the sbi interface.

parent 1addf2ac
Pipeline #6539 passed with stages
in 4 minutes and 27 seconds
Hide whitespace changes
Inline Side-by-side
Showing with 348 additions and 353 deletions
theories/base_logic/upred.v
View file @ 30a36cf2
......@@ -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.
......
theories/bi/derived_laws.v
View file @ 30a36cf2
......@@ -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.
......
theories/bi/embedding.v
View file @ 30a36cf2
......@@ -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⎤.
......
theories/bi/interface.v
View file @ 30a36cf2
......@@ -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);