Commit f25bdcf3 authored by Hai Dang's avatar Hai Dang
Browse files

Initial experiment with internal_eq for bi with siProp embedding

parent 1346ccb3
...@@ -83,6 +83,7 @@ iris/bi/lib/relations.v ...@@ -83,6 +83,7 @@ iris/bi/lib/relations.v
iris/base_logic/upred.v iris/base_logic/upred.v
iris/base_logic/upred_derived.v iris/base_logic/upred_derived.v
iris/base_logic/cmra_valid.v iris/base_logic/cmra_valid.v
iris/base_logic/internal_eq.v
iris/base_logic/bi.v iris/base_logic/bi.v
iris/base_logic/derived.v iris/base_logic/derived.v
iris/base_logic/proofmode.v iris/base_logic/proofmode.v
......
From iris.si_logic Require Import siprop.
From iris.si_logic Require Export bi.
From iris.prelude Require Import options.
Definition bi_internal_eq_def
{PROP : bi} `{BiEmbed siPropI PROP} {A : ofe} (a b : A) : PROP :=
a b .
Definition bi_internal_eq_aux : seal (@bi_internal_eq_def). Proof. by eexists. Qed.
Definition bi_internal_eq := bi_internal_eq_aux.(unseal).
Global Arguments bi_internal_eq {PROP _ A}.
Definition bi_internal_eq_eq :
@bi_internal_eq = @bi_internal_eq_def := bi_internal_eq_aux.(seal_eq).
Module bi_internal_eq.
Ltac unseal :=
rewrite !bi_internal_eq_eq /bi_internal_eq_def /=.
End bi_internal_eq.
Section internal_eq_props.
Context {PROP : bi} `{BiEmbed siPropI PROP}.
Implicit Types (P : PROP).
Local Definition unseal_eqs :=
(@embed_emp, @embed_pure,
@embed_and, @embed_or, @embed_impl, @embed_forall, @embed_exist,
@embed_sep, @embed_wand,
@embed_later).
Local Ltac unseal_embed :=
bi_internal_eq.unseal;
rewrite -?unseal_eqs;
first [apply embed_ne | apply embed_proper | apply embed_mono | idtac ].
Lemma internal_eq_ne (A : ofe) :
NonExpansive2 (@bi_internal_eq PROP _ A).
Proof.
intros n x x' Hx y y' Hy. unseal_embed. exact: siProp_primitive.internal_eq_ne.
Qed.
(* Lemma prop_ext_2 P Q : ■ ((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q.
Proof.
unseal. apply embed_mono. etrans; [apply emp_valid_and_2|apply emp_valid_siProp_internal_eq].
Qed. *)
Lemma internal_eq_refl {A : ofe} P (a : A) : P bi_internal_eq a a.
Proof.
etrans; first apply bi.persistently_emp_intro.
rewrite embed_emp_2 -embed_persistently.
unseal_embed. exact: siProp_primitive.internal_eq_refl.
Qed.
Lemma internal_eq_rewrite {A : ofe} a b (Ψ : A PROP) :
NonExpansive Ψ bi_internal_eq a b Ψ a Ψ b.
Proof.
Abort.
Lemma fun_ext {A} {B : A ofe} (g1 g2 : discrete_fun B) :
( i, bi_internal_eq (g1 i) (g2 i)) bi_internal_eq g1 g2.
Proof. unseal_embed. exact: siProp_primitive.fun_ext. Qed.
Lemma sig_eq {A : ofe} (P : A Prop) (x y : sigO P) :
bi_internal_eq (proj1_sig x) (proj1_sig y) bi_internal_eq x y.
Proof. unseal_embed. exact: siProp_primitive.sig_eq. Qed.
Lemma later_eq_1 `{BiEmbedLater siPropI PROP} {A : ofe} (x y : A) :
bi_internal_eq (Next x) (Next y) (bi_internal_eq x y).
Proof. unseal_embed. exact: siProp_primitive.later_eq_1. Qed.
Lemma later_eq_2 `{BiEmbedLater siPropI PROP} {A : ofe} (x y : A) :
(bi_internal_eq x y) bi_internal_eq (Next x) (Next y).
Proof. unseal_embed. exact: siProp_primitive.later_eq_2. Qed.
Lemma discrete_eq_1 {A : ofe} (a b : A) : Discrete a bi_internal_eq a b a b.
Proof. intros. unseal_embed. exact: siProp_primitive.discrete_eq_1. Qed.
Lemma internal_eq_entails {A B : ofe} (a1 a2 : A) (b1 b2 : B) :
(a1 a2 @{siPropI} b1 b2) bi_internal_eq a1 a2 bi_internal_eq b1 b2.
Proof. intros. by unseal_embed. Qed.
Lemma internal_eq_soundness {A : ofe} (x y : A) : ( bi_internal_eq x y) x y.
Proof. unseal_embed. intros ?%embed_emp_valid_inj. exact: siProp_primitive.internal_eq_soundness. Qed.
End internal_eq_props.
Supports Markdown
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