Commit 01b35b6d authored by Robbert's avatar Robbert

Merge branch 'robbert/iPureIntro_affine' into 'master'

Generalize `iPureIntro` to support non-empty spatial contexts with just affine hypotheses.

See merge request iris/iris!241
parents 2eeebf09 4c341601
...@@ -133,10 +133,21 @@ Lemma test_iSpecialize_Coq_entailment P Q R : ...@@ -133,10 +133,21 @@ Lemma test_iSpecialize_Coq_entailment P Q R :
P (P - Q) Q. P (P - Q) Q.
Proof. iIntros (HP HPQ). iDestruct (HPQ $! HP) as "?". done. Qed. Proof. iIntros (HP HPQ). iDestruct (HPQ $! HP) as "?". done. Qed.
Lemma test_iPure_intro_emp R `{!Affine R} :
R - emp.
Proof. iIntros "HR". by iPureIntro. Qed.
Lemma test_iEmp_intro P Q R `{!Affine P, !Persistent Q, !Affine R} : Lemma test_iEmp_intro P Q R `{!Affine P, !Persistent Q, !Affine R} :
P - Q R - emp. P - Q R - emp.
Proof. iIntros "HP #HQ HR". iEmpIntro. Qed. Proof. iIntros "HP #HQ HR". iEmpIntro. Qed.
Lemma test_iPure_intro (φ : nat Prop) P Q R `{!Affine P, !Persistent Q, !Affine R} :
φ 0 P - Q R - x : nat, <affine> φ x φ x .
Proof. iIntros (?) "HP #HQ HR". iPureIntro; eauto. Qed.
Lemma test_iPure_intro_2 (φ : nat Prop) P Q R `{!Persistent Q} :
φ 0 P - Q R - x : nat, <affine> φ x φ x .
Proof. iIntros (?) "HP #HQ HR". iPureIntro; eauto. Qed.
Lemma test_fresh P Q: Lemma test_fresh P Q:
(P Q) - (P Q). (P Q) - (P Q).
Proof. Proof.
......
...@@ -12,10 +12,10 @@ Global Instance into_pure_cmra_valid `{!CmraDiscrete A} (a : A) : ...@@ -12,10 +12,10 @@ Global Instance into_pure_cmra_valid `{!CmraDiscrete A} (a : A) :
@IntoPure (uPredI M) ( a) ( a). @IntoPure (uPredI M) ( a) ( a).
Proof. by rewrite /IntoPure discrete_valid. Qed. Proof. by rewrite /IntoPure discrete_valid. Qed.
Global Instance from_pure_cmra_valid {A : cmraT} af (a : A) : Global Instance from_pure_cmra_valid {A : cmraT} (a : A) :
@FromPure (uPredI M) af ( a) ( a). @FromPure (uPredI M) false ( a) ( a).
Proof. Proof.
rewrite /FromPure. eapply bi.pure_elim; [by apply bi.affinely_if_elim|]=> ?. rewrite /FromPure /=. eapply bi.pure_elim=> // ?.
rewrite -uPred.cmra_valid_intro //. rewrite -uPred.cmra_valid_intro //.
Qed. Qed.
......
...@@ -153,13 +153,12 @@ Proof. rewrite /IntoPure=>Hx. rewrite -pure_forall_2. by setoid_rewrite Hx. Qed. ...@@ -153,13 +153,12 @@ Proof. rewrite /IntoPure=>Hx. rewrite -pure_forall_2. by setoid_rewrite Hx. Qed.
Global Instance into_pure_pure_sep (φ1 φ2 : Prop) P1 P2 : Global Instance into_pure_pure_sep (φ1 φ2 : Prop) P1 P2 :
IntoPure P1 φ1 IntoPure P2 φ2 IntoPure (P1 P2) (φ1 φ2). IntoPure P1 φ1 IntoPure P2 φ2 IntoPure (P1 P2) (φ1 φ2).
Proof. rewrite /IntoPure=> -> ->. by rewrite sep_and pure_and. Qed. Proof. rewrite /IntoPure=> -> ->. by rewrite sep_and pure_and. Qed.
Global Instance into_pure_pure_wand (φ1 φ2 : Prop) P1 P2 : Global Instance into_pure_pure_wand a (φ1 φ2 : Prop) P1 P2 :
FromPure true P1 φ1 IntoPure P2 φ2 IntoPure (P1 - P2) (φ1 φ2). FromPure a P1 φ1 IntoPure P2 φ2 IntoPure (P1 - P2) (φ1 φ2).
Proof. Proof.
rewrite /FromPure /IntoPure=> <- -> /=. rewrite /FromPure /IntoPure=> <- -> /=. rewrite pure_impl.
rewrite pure_impl -impl_wand_2. apply bi.wand_intro_l. apply impl_intro_l, pure_elim_l=> ?. rewrite (pure_True φ1) //.
rewrite -{1}(persistent_absorbingly_affinely ⌜φ1%I) absorbingly_sep_l by rewrite -affinely_affinely_if affinely_True_emp affinely_emp left_id.
bi.wand_elim_r absorbing //.
Qed. Qed.
Global Instance into_pure_affinely P φ : IntoPure P φ IntoPure (<affine> P) φ. Global Instance into_pure_affinely P φ : IntoPure P φ IntoPure (<affine> P) φ.
...@@ -177,14 +176,24 @@ Global Instance into_pure_embed `{BiEmbed PROP PROP'} P φ : ...@@ -177,14 +176,24 @@ Global Instance into_pure_embed `{BiEmbed PROP PROP'} P φ :
Proof. rewrite /IntoPure=> ->. by rewrite embed_pure. Qed. Proof. rewrite /IntoPure=> ->. by rewrite embed_pure. Qed.
(** FromPure *) (** FromPure *)
Global Instance from_pure_pure a φ : @FromPure PROP a ⌜φ⌝ φ. Global Instance from_pure_emp : @FromPure PROP true emp True.
Proof. rewrite /FromPure. apply affinely_if_elim. Qed. Proof. rewrite /FromPure /=. apply (affine _). Qed.
Global Instance from_pure_pure_and a (φ1 φ2 : Prop) P1 P2 : Global Instance from_pure_pure φ : @FromPure PROP false ⌜φ⌝ φ.
FromPure a P1 φ1 FromPure a P2 φ2 FromPure a (P1 P2) (φ1 φ2). Proof. by rewrite /FromPure /=. Qed.
Proof. rewrite /FromPure pure_and=> <- <- /=. by rewrite affinely_if_and. Qed. Global Instance from_pure_pure_and a1 a2 (φ1 φ2 : Prop) P1 P2 :
Global Instance from_pure_pure_or a (φ1 φ2 : Prop) P1 P2 : FromPure a1 P1 φ1 FromPure a2 P2 φ2
FromPure a P1 φ1 FromPure a P2 φ2 FromPure a (P1 P2) (φ1 φ2). FromPure (if a1 then true else a2) (P1 P2) (φ1 φ2).
Proof. by rewrite /FromPure pure_or affinely_if_or=><- <-. Qed. Proof.
rewrite /FromPure pure_and=> <- <- /=. rewrite affinely_if_and.
f_equiv; apply affinely_if_flag_mono; destruct a1; naive_solver.
Qed.
Global Instance from_pure_pure_or a1 a2 (φ1 φ2 : Prop) P1 P2 :
FromPure a1 P1 φ1 FromPure a2 P2 φ2
FromPure (if a1 then true else a2) (P1 P2) (φ1 φ2).
Proof.
rewrite /FromPure pure_or=> <- <- /=. rewrite affinely_if_or.
f_equiv; apply affinely_if_flag_mono; destruct a1; naive_solver.
Qed.
Global Instance from_pure_pure_impl a (φ1 φ2 : Prop) P1 P2 : Global Instance from_pure_pure_impl a (φ1 φ2 : Prop) P1 P2 :
IntoPure P1 φ1 FromPure a P2 φ2 FromPure a (P1 P2) (φ1 φ2). IntoPure P1 φ1 FromPure a P2 φ2 FromPure a (P1 P2) (φ1 φ2).
Proof. Proof.
...@@ -205,27 +214,25 @@ Proof. ...@@ -205,27 +214,25 @@ Proof.
destruct a=>//=. apply affinely_forall. destruct a=>//=. apply affinely_forall.
Qed. Qed.
Global Instance from_pure_pure_sep_true (φ1 φ2 : Prop) P1 P2 : Global Instance from_pure_pure_sep_true a1 a2 (φ1 φ2 : Prop) P1 P2 :
FromPure true P1 φ1 FromPure true P2 φ2 FromPure true (P1 P2) (φ1 φ2). FromPure a1 P1 φ1 FromPure a2 P2 φ2
Proof. FromPure (if a1 then a2 else false) (P1 P2) (φ1 φ2).
rewrite /FromPure=> <- <- /=.
by rewrite -persistent_and_affinely_sep_l affinely_and_r pure_and.
Qed.
Global Instance from_pure_pure_sep_false_l (φ1 φ2 : Prop) P1 P2 :
FromPure false P1 φ1 FromPure true P2 φ2 FromPure false (P1 P2) (φ1 φ2).
Proof.
rewrite /FromPure=> <- <- /=. by rewrite -persistent_and_affinely_sep_r pure_and.
Qed.
Global Instance from_pure_pure_sep_false_r (φ1 φ2 : Prop) P1 P2 :
FromPure true P1 φ1 FromPure false P2 φ2 FromPure false (P1 P2) (φ1 φ2).
Proof. Proof.
rewrite /FromPure=> <- <- /=. by rewrite -persistent_and_affinely_sep_l pure_and. rewrite /FromPure=> <- <-. destruct a1; simpl.
- by rewrite pure_and -persistent_and_affinely_sep_l affinely_if_and_r.
- by rewrite pure_and -affinely_affinely_if -persistent_and_affinely_sep_r_1.
Qed. Qed.
Global Instance from_pure_pure_wand (φ1 φ2 : Prop) a P1 P2 : Global Instance from_pure_pure_wand a (φ1 φ2 : Prop) P1 P2 :
IntoPure P1 φ1 FromPure false P2 φ2 FromPure a (P1 - P2) (φ1 φ2). IntoPure P1 φ1 FromPure a P2 φ2
TCOr (TCEq a false) (Affine P1)
FromPure a (P1 - P2) (φ1 φ2).
Proof. Proof.
rewrite /FromPure /IntoPure=> -> <- /=. rewrite /FromPure /IntoPure=> HP1 <- Ha /=. apply wand_intro_l.
by rewrite bi.affinely_if_elim pure_wand_forall pure_impl pure_impl_forall. destruct a; simpl.
- destruct Ha as [Ha|?]; first inversion Ha.
rewrite -persistent_and_affinely_sep_r -(affine_affinely P1) HP1.
by rewrite affinely_and_l pure_impl impl_elim_r.
- by rewrite HP1 sep_and pure_impl impl_elim_r.
Qed. Qed.
Global Instance from_pure_persistently P a φ : Global Instance from_pure_persistently P a φ :
...@@ -234,24 +241,21 @@ Proof. ...@@ -234,24 +241,21 @@ Proof.
rewrite /FromPure=> <- /=. rewrite /FromPure=> <- /=.
by rewrite persistently_affinely_elim affinely_if_elim persistently_pure. by rewrite persistently_affinely_elim affinely_if_elim persistently_pure.
Qed. Qed.
Global Instance from_pure_affinely_true P φ : Global Instance from_pure_affinely_true a P φ :
FromPure true P φ FromPure true (<affine> P) φ. FromPure a P φ FromPure true (<affine> P) φ.
Proof. rewrite /FromPure=><- /=. by rewrite affinely_idemp. Qed. Proof. rewrite /FromPure=><- /=. by rewrite -affinely_affinely_if affinely_idemp. Qed.
Global Instance from_pure_affinely_false P φ `{!Affine P} : Global Instance from_pure_intuitionistically_true a P φ :
FromPure false P φ FromPure false (<affine> P) φ. FromPure a P φ FromPure true ( P) φ.
Proof. rewrite /FromPure /= affine_affinely //. Qed.
Global Instance from_pure_intuitionistically_true P φ :
FromPure true P φ FromPure true ( P) φ.
Proof. Proof.
rewrite /FromPure=><- /=. rewrite intuitionistically_affinely_elim. rewrite /FromPure=><- /=.
rewrite {1}(persistent ⌜φ⌝%I) //. rewrite -intuitionistically_affinely_elim -affinely_affinely_if affinely_idemp.
by rewrite intuitionistic_intuitionistically.
Qed. Qed.
Global Instance from_pure_absorbingly a P φ :
Global Instance from_pure_absorbingly P φ p : FromPure a P φ FromPure false (<absorb> P) φ.
FromPure true P φ FromPure p (<absorb> P) φ.
Proof. Proof.
rewrite /FromPure=> <- /=. rewrite /FromPure=> <- /=. rewrite -affinely_affinely_if.
rewrite persistent_absorbingly_affinely affinely_if_elim //. by rewrite -persistent_absorbingly_affinely_2.
Qed. Qed.
Global Instance from_pure_embed `{BiEmbed PROP PROP'} a P φ : Global Instance from_pure_embed `{BiEmbed PROP PROP'} a P φ :
FromPure a P φ FromPure a P φ. FromPure a P φ FromPure a P φ.
...@@ -946,17 +950,20 @@ Global Instance into_forall_embed `{BiEmbed PROP PROP'} {A} P (Φ : A → PROP) ...@@ -946,17 +950,20 @@ Global Instance into_forall_embed `{BiEmbed PROP PROP'} {A} P (Φ : A → PROP)
IntoForall P Φ IntoForall P (λ a, ⎡Φ a%I). IntoForall P Φ IntoForall P (λ a, ⎡Φ a%I).
Proof. by rewrite /IntoForall -embed_forall => <-. Qed. Proof. by rewrite /IntoForall -embed_forall => <-. Qed.
Global Instance into_forall_impl_pure φ P Q : Global Instance into_forall_impl_pure a φ P Q :
FromPureT false P φ IntoForall (P Q) (λ _ : φ, Q). FromPureT a P φ
TCOr (TCEq a false) (BiAffine PROP)
IntoForall (P Q) (λ _ : φ, Q).
Proof. Proof.
rewrite /FromPureT /FromPure /IntoForall=> -[φ' [-> <-]]. rewrite /FromPureT /FromPure /IntoForall=> -[φ' [-> <-]] [->|?] /=.
by rewrite pure_impl_forall. - by rewrite pure_impl_forall.
- by rewrite -affinely_affinely_if affine_affinely pure_impl_forall.
Qed. Qed.
Global Instance into_forall_wand_pure φ P Q : Global Instance into_forall_wand_pure a φ P Q :
FromPureT true P φ IntoForall (P - Q) (λ _ : φ, Q). FromPureT a P φ IntoForall (P - Q) (λ _ : φ, Q).
Proof. Proof.
rewrite /FromPureT /FromPure /IntoForall=> -[φ' [-> <-]] /=. rewrite /FromPureT /FromPure /IntoForall=> -[φ' [-> <-]] /=.
apply forall_intro=>? /=. apply forall_intro=>? /=. rewrite -affinely_affinely_if.
by rewrite -(pure_intro _ True%I) // /bi_affinely right_id emp_wand. by rewrite -(pure_intro _ True%I) // /bi_affinely right_id emp_wand.
Qed. Qed.
......
...@@ -37,9 +37,9 @@ Proof. ...@@ -37,9 +37,9 @@ Proof.
Qed. Qed.
(** FromPure *) (** FromPure *)
Global Instance from_pure_internal_eq af {A : ofeT} (a b : A) : Global Instance from_pure_internal_eq {A : ofeT} (a b : A) :
@FromPure PROP af (a b) (a b). @FromPure PROP false (a b) (a b).
Proof. by rewrite /FromPure pure_internal_eq affinely_if_elim. Qed. Proof. by rewrite /FromPure pure_internal_eq. Qed.
Global Instance from_pure_later a P φ : FromPure a P φ FromPure a ( P) φ. Global Instance from_pure_later a P φ : FromPure a P φ FromPure a ( P) φ.
Proof. rewrite /FromPure=> ->. apply later_intro. Qed. Proof. rewrite /FromPure=> ->. apply later_intro. Qed.
Global Instance from_pure_laterN a n P φ : FromPure a P φ FromPure a (^n P) φ. Global Instance from_pure_laterN a n P φ : FromPure a P φ FromPure a (^n P) φ.
......
...@@ -56,24 +56,20 @@ Proof. by exists φ. Qed. ...@@ -56,24 +56,20 @@ Proof. by exists φ. Qed.
Hint Extern 0 (IntoPureT _ _) => Hint Extern 0 (IntoPureT _ _) =>
notypeclasses refine (into_pureT_hint _ _ _) : typeclass_instances. notypeclasses refine (into_pureT_hint _ _ _) : typeclass_instances.
(** [FromPure] is used when introducing a pure assertion. It is used (** [FromPure a P φ] is used when introducing a pure assertion. It is used by
by iPure, the "[%]" specialization pattern, and the [with "[%]"] [iPureIntro] and the [[%]] specialization pattern.
pattern when using [iAssert].
The Boolean [a] specifies whether introduction of [P] needs [emp] in addition
The [a] Boolean asserts whether we introduce the pure assertion in to [φ]. Concretely, for the [iPureIntro] tactic, this means it specifies whether
an affine way or in an absorbing way. When [FromPure true P φ] is the spatial context should be empty or not.
derived, then [FromPure false P φ] can always be derived too. We
use [true] for specialization patterns and [false] for the Note that the Boolean [a] is not needed for the (dual) [IntoPure] class, because
[iPureIntro] tactic. there we can just ask that [P] is [Affine]. *)
This Boolean is not needed for [IntoPure], because in the case of
[IntoPure], we can have the same behavior by asking that [P] be
[Affine]. *)
Class FromPure {PROP : bi} (a : bool) (P : PROP) (φ : Prop) := Class FromPure {PROP : bi} (a : bool) (P : PROP) (φ : Prop) :=
from_pure : <affine>?a ⌜φ⌝ P. from_pure : <affine>?a ⌜φ⌝ P.
Arguments FromPure {_} _ _%I _%type_scope : simpl never. Arguments FromPure {_} _ _%I _%type_scope : simpl never.
Arguments from_pure {_} _ _%I _%type_scope {_}. Arguments from_pure {_} _ _%I _%type_scope {_}.
Hint Mode FromPure + + ! - : typeclass_instances. Hint Mode FromPure + - ! - : typeclass_instances.
Class FromPureT {PROP : bi} (a : bool) (P : PROP) (φ : Type) := Class FromPureT {PROP : bi} (a : bool) (P : PROP) (φ : Type) :=
from_pureT : ψ : Prop, φ = ψ FromPure a P ψ. from_pureT : ψ : Prop, φ = ψ FromPure a P ψ.
......
...@@ -104,14 +104,14 @@ Proof. ...@@ -104,14 +104,14 @@ Proof.
Qed. Qed.
(** * Pure *) (** * Pure *)
(* This relies on the invariant that [FromPure false] implies Lemma tac_pure_intro Δ Q φ a :
[FromPure true] *) FromPure a Q φ
Lemma tac_pure_intro Δ Q φ af : (if a then AffineEnv (env_spatial Δ) else TCTrue)
env_spatial_is_nil Δ = af FromPure af Q φ φ envs_entails Δ Q. φ
Proof. envs_entails Δ Q.
intros ???. rewrite envs_entails_eq -(from_pure af Q). destruct af. Proof.
- rewrite env_spatial_is_nil_intuitionistically //= /bi_intuitionistically. intros ???. rewrite envs_entails_eq -(from_pure a Q). destruct a; simpl.
f_equiv. by apply pure_intro. - by rewrite (affine (of_envs Δ)) pure_True // affinely_True_emp affinely_emp.
- by apply pure_intro. - by apply pure_intro.
Qed. Qed.
...@@ -276,19 +276,18 @@ Proof. ...@@ -276,19 +276,18 @@ Proof.
apply wand_intro_l. by rewrite assoc !wand_elim_r. apply wand_intro_l. by rewrite assoc !wand_elim_r.
Qed. Qed.
Lemma tac_specialize_assert_pure Δ Δ' j q R P1 P2 φ Q : Lemma tac_specialize_assert_pure Δ Δ' j q a R P1 P2 φ Q :
envs_lookup j Δ = Some (q, R) envs_lookup j Δ = Some (q, R)
IntoWand q true R P1 P2 IntoWand q true R P1 P2
FromPure true P1 φ FromPure a P1 φ
envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ' envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ'
φ envs_entails Δ' Q envs_entails Δ Q. φ envs_entails Δ' Q envs_entails Δ Q.
Proof. Proof.
rewrite envs_entails_eq=> ????? <-. rewrite envs_simple_replace_singleton_sound //=. rewrite envs_entails_eq=> ????? <-. rewrite envs_simple_replace_singleton_sound //=.
rewrite -intuitionistically_if_idemp (into_wand q true) /=. rewrite -intuitionistically_if_idemp (into_wand q true) /=.
rewrite -(from_pure true P1) /bi_intuitionistically. rewrite -(from_pure a P1) pure_True //.
rewrite pure_True //= persistently_affinely_elim persistently_pure rewrite -affinely_affinely_if affinely_True_emp affinely_emp.
affinely_True_emp affinely_emp. by rewrite intuitionistically_emp left_id wand_elim_r.
by rewrite emp_wand wand_elim_r.
Qed. Qed.
Lemma tac_specialize_assert_intuitionistic Δ Δ' Δ'' j q P1 P1' P2 R Q : Lemma tac_specialize_assert_intuitionistic Δ Δ' Δ'' j q P1 P1' P2 R Q :
......
...@@ -26,10 +26,20 @@ Proof. ...@@ -26,10 +26,20 @@ Proof.
apply sep_elim_l, _. apply sep_elim_l, _.
Qed. Qed.
Global Instance frame_here_pure p φ Q : FromPure false Q φ Frame p ⌜φ⌝ Q True. Global Instance frame_here_pure_persistent a φ Q :
FromPure a Q φ Frame true ⌜φ⌝ Q emp.
Proof. Proof.
rewrite /FromPure /Frame=> <-. rewrite /FromPure /Frame /= => <-. rewrite right_id.
by rewrite intuitionistically_if_elim sep_elim_l. by rewrite -affinely_affinely_if intuitionistically_affinely.
Qed.
Global Instance frame_here_pure a φ Q :
FromPure a Q φ
TCOr (TCEq a false) (BiAffine PROP)
Frame false ⌜φ⌝ Q emp.
Proof.
rewrite /FromPure /Frame => <- [->|?] /=.
- by rewrite right_id.
- by rewrite right_id -affinely_affinely_if affine_affinely.
Qed. Qed.
Global Instance make_embed_pure `{BiEmbed PROP PROP'} φ : Global Instance make_embed_pure `{BiEmbed PROP PROP'} φ :
......
...@@ -300,10 +300,11 @@ Tactic Notation "iEmpIntro" := ...@@ -300,10 +300,11 @@ Tactic Notation "iEmpIntro" :=
Tactic Notation "iPureIntro" := Tactic Notation "iPureIntro" :=
iStartProof; iStartProof;
eapply tac_pure_intro; eapply tac_pure_intro;
[pm_reflexivity [iSolveTC ||
|iSolveTC ||
let P := match goal with |- FromPure _ ?P _ => P end in let P := match goal with |- FromPure _ ?P _ => P end in
fail "iPureIntro:" P "not pure" fail "iPureIntro:" P "not pure"
|pm_reduce; iSolveTC ||
fail "iPureIntro: spatial context contains non-affine hypotheses"
|]. |].
(** Framing *) (** Framing *)
...@@ -780,7 +781,7 @@ Ltac iSpecializePat_go H1 pats := ...@@ -780,7 +781,7 @@ Ltac iSpecializePat_go H1 pats :=
fail "iSpecialize: cannot instantiate" P "with" Q fail "iSpecialize: cannot instantiate" P "with" Q
|pm_reflexivity|iSpecializePat_go H1 pats]] |pm_reflexivity|iSpecializePat_go H1 pats]]
| SPureGoal ?d :: ?pats => | SPureGoal ?d :: ?pats =>
notypeclasses refine (tac_specialize_assert_pure _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _); notypeclasses refine (tac_specialize_assert_pure _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _ _);
[pm_reflexivity || [pm_reflexivity ||
let H1 := pretty_ident H1 in let H1 := pretty_ident H1 in
fail "iSpecialize:" H1 "not found" fail "iSpecialize:" H1 "not found"
......
...@@ -202,8 +202,8 @@ Global Instance from_pure_monPred_at a P φ i : FromPure a P φ → FromPure a ( ...@@ -202,8 +202,8 @@ Global Instance from_pure_monPred_at a P φ i : FromPure a P φ → FromPure a (
Proof. rewrite /FromPure=><-. by rewrite monPred_at_affinely_if monPred_at_pure. Qed. Proof. rewrite /FromPure=><-. by rewrite monPred_at_affinely_if monPred_at_pure. Qed.
Global Instance into_pure_monPred_in i j : @IntoPure PROP (monPred_in i j) (i j). Global Instance into_pure_monPred_in i j : @IntoPure PROP (monPred_in i j) (i j).
Proof. by rewrite /IntoPure monPred_at_in. Qed. Proof. by rewrite /IntoPure monPred_at_in. Qed.
Global Instance from_pure_monPred_in i j af : @FromPure PROP af (monPred_in i j) (i j). Global Instance from_pure_monPred_in i j : @FromPure PROP false (monPred_in i j) (i j).
Proof. by rewrite /FromPure monPred_at_in bi.affinely_if_elim. Qed. Proof. by rewrite /FromPure monPred_at_in. Qed.
Global Instance into_persistent_monPred_at p P Q 𝓠 i : Global Instance into_persistent_monPred_at p P Q 𝓠 i :
IntoPersistent p P Q MakeMonPredAt i Q 𝓠 IntoPersistent p (P i) 𝓠 | 0. IntoPersistent p P Q MakeMonPredAt i Q 𝓠 IntoPersistent p (P i) 𝓠 | 0.
......
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