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

Add more upred_si_embed properties

parent 1cdaee2b
......@@ -911,17 +911,77 @@ Local Ltac unseal_embed :=
/bi_sep /= /siProp_sep ?siProp_and_eq /=
/bi_wand /= /siProp_wand ?siProp_impl_eq /=
/bi_persistently /= /siProp_persistently
; unseal.
; try unseal.
Lemma si_embed_si_emp_valid (P : siProp) : @uPred_si_emp_valid M (uPred_si_embed P) P.
Proof. unseal. by constructor. Qed.
Lemma si_embed_emp_valid_inj (P : siProp) : (True P ) @{siPropI} P.
(** internal_eq properties between uPred_si_embed and uPred_si_emp_valid *)
Lemma si_embed_si_emp_valid (P : siProp) :
@uPred_si_emp_valid M (uPred_si_embed P) P.
Proof. by unseal. Qed.
Lemma si_embed_plainly (P : siProp) :
uPred_plainly (@uPred_si_embed M P) uPred_si_embed P.
Proof. by unseal. Qed.
Lemma si_embed_plainly_equiv (P : siProp) :
uPred_plainly (@uPred_si_embed M P) uPred_si_embed P.
Proof. by unseal. Qed.
Lemma si_emp_valid_si_embed P :
@uPred_si_embed M (uPred_si_emp_valid P) uPred_plainly P.
Proof. by unseal. Qed.
Lemma si_emp_valid_si_embed_equiv P :
@uPred_si_embed M (uPred_si_emp_valid P) uPred_plainly P.
Proof. by unseal. Qed.
(** Connections between siProp entails and uPred_entails *)
Lemma si_emp_valid_plainly_1 P Q :
(uPred_si_emp_valid P @{siPropI} uPred_si_emp_valid Q) P Q.
Proof.
unseal. intros [HPQ]. constructor => ???. intros HQ%HPQ.
apply (uPred_mono _ _ _ _ ε _ HQ); [apply ucmra_unit_leastN|done].
Qed.
Lemma si_emp_valid_plainly_2 P Q :
( P Q) (uPred_si_emp_valid P @{siPropI} uPred_si_emp_valid Q).
Proof.
unseal. intros [HPQ]. constructor => ?. apply (HPQ _ ε), ucmra_unit_validN.
Qed.
Local Existing Instance entails_po.
Lemma plainly_entails_si_embed_1 P (Q : siProp) :
(uPred_si_emp_valid P @{siPropI} Q) P Q .
Proof. intros. apply si_emp_valid_plainly_1. by rewrite si_embed_si_emp_valid. Qed.
Lemma plainly_entails_si_embed_2 P (Q : siProp) :
( P Q ) (uPred_si_emp_valid P @{siPropI} Q).
Proof.
intros HPQ. rewrite -(si_embed_si_emp_valid Q). apply si_emp_valid_plainly_2.
(* This should be done easily with si_embed_plainly if we have rewriting here. *)
etrans; [exact HPQ|]. apply equiv_entails, si_embed_plainly_equiv.
Qed.
Lemma plainly_entails_si_embed P (Q : siProp) :
( P Q ) (uPred_si_emp_valid P @{siPropI} Q).
Proof. split; [apply plainly_entails_si_embed_2|apply plainly_entails_si_embed_1]. Qed.
Lemma si_embed_entails_si_emp_valid (P : siProp) Q :
(P @{siPropI} uPred_si_emp_valid Q) P Q.
Proof.
rewrite -{1}(si_embed_si_emp_valid P). intros HPQ%si_emp_valid_plainly_1.
etrans; [|exact HPQ]. apply equiv_entails, si_embed_plainly_equiv.
Qed.
Lemma si_emp_valid_emp_valid_inj P :
(True P) (@{siPropI} uPred_si_emp_valid P).
Proof.
unseal. intros [EP]. constructor => ??.
apply (EP _ ε); [apply ucmra_unit_validN|done].
Qed.
Lemma emp_valid_entails_si_embed P (Q : siProp) : (@{siPropI} Q) P Q .
Proof. unseal. intros [HQ]. constructor => ????. apply HQ. by unseal_embed. Qed.
(** Embedding's properties *)
Lemma si_embed_emp_valid_inj (P : siProp) : (True P ) @{siPropI} P.
Proof.
rewrite -{2}(si_embed_si_emp_valid P). by apply si_emp_valid_emp_valid_inj.
Qed.
Lemma si_embed_emp : True emp .
Proof. by unseal_embed. Qed.
Proof. by apply emp_valid_entails_si_embed. Qed.
Lemma si_embed_impl (P Q : siProp) : ( P Q ) bi_impl P Q .
Proof.
unseal_embed.
......
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