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

Add more proofmode instances for subjectively and objectively

parent 96b5f919
......@@ -187,6 +187,26 @@ Proof. by rewrite /FromOr monPred_objectively_or => ->. Qed.
FromOr P Q1 Q2 FromOr (<obj> P) (<obj> Q1) (<obj> Q2).
Proof. by rewrite /FromOr monPred_objectively_or => <-. Qed.
#[global] Instance into_pure_objectively (φ : Prop) P :
IntoPure P φ IntoPure (<obj> P) φ.
Proof. rewrite /IntoPure => ->. by rewrite monPred_objectively_pure. Qed.
#[global] Instance from_pure_objectively a P φ :
FromPure a P φ FromPure a (<obj> P) φ.
Proof.
rewrite /FromPure -embed_pure -embed_affinely_if => <-.
apply objective_objectively, _.
Qed.
#[global] Instance into_pure_subjectively (φ : Prop) P :
IntoPure P φ IntoPure (<subj> P) φ.
Proof. rewrite /IntoPure=> ->. apply objective_subjectively, _. Qed.
#[global] Instance from_pure_subjectively a P φ :
FromPure a P φ FromPure a (<subj> P) φ.
Proof.
rewrite /FromPure -embed_pure -embed_affinely_if => <-.
apply monPred_subjectively_intro.
Qed.
#[global] Instance into_sep_subjectively P Q1 Q2 :
IntoSep P Q1 Q2 IntoSep (<subj> P) (<subj> Q1) (<subj> Q2).
Proof. by rewrite /IntoSep -monPred_subjectively_sep => ->. Qed.
......@@ -194,7 +214,7 @@ Proof. by rewrite /IntoSep -monPred_subjectively_sep => ->. Qed.
#[global] Instance into_exist_subjectively {A}
P (Φ : A monPred) name :
IntoExist P Φ name IntoExist (<subj> P) (λ a, (<subj> Φ a)%I) name.
Proof. by rewrite /IntoExist -monPred_subjectively_exist => ->. Qed.
Proof. by rewrite /IntoExist -monPred_subjectively_exist => ->. Qed.
#[global] Instance from_exist_subjectively {A} P (Φ : A monPred) :
FromExist P Φ FromExist (<subj> P) (λ a, (<subj> Φ a)%I).
Proof. by rewrite /FromExist -monPred_subjectively_exist => ->. Qed.
......
......@@ -169,11 +169,8 @@ Section na_props.
<subj> l {q1} v1 - <subj> l {q2} v2 - v1 = v2.
Proof.
rewrite own_loc_na_eq /own_loc_na_def.
(* TODO more proofmode instances *)
iDestruct 1 as (t m) "(H1 & Hrel1 & _)".
iDestruct 1 as (t' m') "(H2 & Hrel2 & _)".
rewrite 2!objective_subjectively.
iDestruct "Hrel1" as %Hrel1. iDestruct "Hrel2" as %Hrel2.
iDestruct 1 as (t m) "(H1 & %Hrel1 & _)".
iDestruct 1 as (t' m') "(H2 & %Hrel2 & _)".
iDestruct (own_loc_prim_agree_subjectively with "H1 H2") as %Eq.
apply (f_equal (lookup t)) in Eq. rewrite lookup_singleton in Eq.
destruct (decide (t = t')) as [<-|]; last by rewrite lookup_singleton_ne in Eq.
......
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