Commit 128c9125 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Tweak.

parent 46ffdc4a
......@@ -37,6 +37,7 @@ Class SbiEmbedding (PROP1 PROP2 : sbi) `{BiEmbed PROP1 PROP2} := {
Section bi_embedding.
Context `{BiEmbedding PROP1 PROP2}.
Local Notation bi_embed := (bi_embed (A:=PROP1) (B:=PROP2)).
Local Notation "⎡ P ⎤" := (bi_embed P) : bi_scope.
Implicit Types P Q R : PROP1.
Global Instance bi_embed_proper : Proper (() ==> ()) bi_embed.
......@@ -49,7 +50,7 @@ Section bi_embedding.
rewrite EQ //.
Qed.
Lemma bi_embed_valid (P : PROP1) : bi_embed P P.
Lemma bi_embed_valid (P : PROP1) : P%I P.
Proof.
by rewrite /bi_valid -bi_embed_emp; split=>?; [apply (inj bi_embed)|f_equiv].
Qed.
......@@ -78,7 +79,7 @@ Section bi_embedding.
apply bi.equiv_spec; split; [|apply bi_embed_wand_2].
apply bi.wand_intro_l. by rewrite -bi_embed_sep bi.wand_elim_r.
Qed.
Lemma bi_embed_pure φ : bi_embed ⌜φ⌝ ⌜φ⌝.
Lemma bi_embed_pure φ : ⎡⌜φ⌝⎤ ⌜φ⌝.
Proof.
rewrite (@bi.pure_alt PROP1) (@bi.pure_alt PROP2) bi_embed_exist.
do 2 f_equiv. apply bi.equiv_spec. split; [apply bi.True_intro|].
......@@ -86,7 +87,7 @@ 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) : bi_embed (x y) x y.
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|].
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment