Commit 51dbb411 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

rename : affinely_persistently -> intuitionistically. Add lemma about...

rename : affinely_persistently -> intuitionistically. Add lemma about monpred_at and intuitionistically.
parent 00b874ce
......@@ -17,7 +17,7 @@ Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
(* Own and valid derived *)
Lemma persistently_cmra_valid_1 {A : cmraT} (a : A) : a <pers> ( a : uPred M).
Proof. by rewrite {1}plainly_cmra_valid_1 plainly_elim_persistently. Qed.
Lemma affinely_persistently_ownM (a : M) : CoreId a uPred_ownM a uPred_ownM a.
Lemma intuitionistically_ownM (a : M) : CoreId a uPred_ownM a uPred_ownM a.
Proof.
rewrite /bi_intuitionistically affine_affinely=>?; apply (anti_symm _);
[by rewrite persistently_elim|].
......@@ -31,7 +31,7 @@ Lemma ownM_unit' : uPred_ownM ε ⊣⊢ True.
Proof. apply (anti_symm _); first by apply pure_intro. apply ownM_unit. Qed.
Lemma plainly_cmra_valid {A : cmraT} (a : A) : a a.
Proof. apply (anti_symm _), plainly_cmra_valid_1. apply plainly_elim, _. Qed.
Lemma affinely_persistently_cmra_valid {A : cmraT} (a : A) : a a.
Lemma intuitionistically_cmra_valid {A : cmraT} (a : A) : a a.
Proof.
rewrite /bi_intuitionistically affine_affinely. intros; apply (anti_symm _);
first by rewrite persistently_elim.
......
......@@ -503,6 +503,11 @@ Lemma monPred_at_affinely i P : (<affine> P) i ⊣⊢ <affine> (P i).
Proof. by rewrite /bi_affinely monPred_at_and monPred_at_emp. Qed.
Lemma monPred_at_affinely_if i p P : (<affine>?p P) i <affine>?p (P i).
Proof. destruct p=>//=. apply monPred_at_affinely. Qed.
Lemma monPred_at_intuitionistically i P : ( P) i (P i).
Proof. by rewrite /bi_intuitionistically monPred_at_affinely monPred_at_persistently. Qed.
Lemma monPred_at_intuitionistically_if i p P : (?p P) i ?p (P i).
Proof. destruct p=>//=. apply monPred_at_intuitionistically. Qed.
Lemma monPred_at_absorbingly i P : (<absorb> P) i <absorb> (P i).
Proof. by rewrite /bi_absorbingly monPred_at_sep monPred_at_pure. Qed.
......
......@@ -61,7 +61,7 @@ Global Instance from_modal_persistently_monPred_at `(sel : A) P Q 𝓠 i :
Proof.
rewrite /FromModal /MakeMonPredAt /==> <- <-. by rewrite monPred_at_persistently.
Qed.
Global Instance from_modal_affinely_persistently_monPred_at `(sel : A) P Q 𝓠 i :
Global Instance from_modal_intuitionistically_monPred_at `(sel : A) P Q 𝓠 i :
FromModal modality_intuitionistically sel P Q MakeMonPredAt i Q 𝓠
FromModal modality_intuitionistically sel (P i) 𝓠 | 0.
Proof.
......@@ -101,6 +101,9 @@ Proof. by rewrite /MakeMonPredAt monPred_at_persistently=><-. Qed.
Global Instance make_monPred_at_affinely i P 𝓟 :
MakeMonPredAt i P 𝓟 MakeMonPredAt i (<affine> P) (<affine> 𝓟).
Proof. by rewrite /MakeMonPredAt monPred_at_affinely=><-. Qed.
Global Instance make_monPred_at_intuitionistically i P 𝓟 :
MakeMonPredAt i P 𝓟 MakeMonPredAt i ( P) ( 𝓟).
Proof. by rewrite /MakeMonPredAt monPred_at_intuitionistically=><-. Qed.
Global Instance make_monPred_at_absorbingly i P 𝓟 :
MakeMonPredAt i P 𝓟 MakeMonPredAt i (<absorb> P) (<absorb> 𝓟).
Proof. by rewrite /MakeMonPredAt monPred_at_absorbingly=><-. Qed.
......@@ -112,6 +115,10 @@ Global Instance make_monPred_at_affinely_if i P 𝓟 p :
MakeMonPredAt i P 𝓟
MakeMonPredAt i (<affine>?p P) (<affine>?p 𝓟).
Proof. destruct p; simpl; apply _. Qed.
Global Instance make_monPred_at_intuitionistically_if i P 𝓟 p :
MakeMonPredAt i P 𝓟
MakeMonPredAt i (?p P) (?p 𝓟).
Proof. destruct p; simpl; apply _. Qed.
Global Instance make_monPred_at_embed i 𝓟 : MakeMonPredAt i ⎡𝓟⎤ 𝓟.
Proof. by rewrite /MakeMonPredAt monPred_at_embed. Qed.
Global Instance make_monPred_at_in i j : MakeMonPredAt j (monPred_in i) i j.
......
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