Commit 78ba9509 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Make FromPure depend on an affinity parameter.

parent f30188af
......@@ -31,10 +31,10 @@ Global Instance into_pure_cmra_valid `{CmraDiscrete A} (a : A) :
@IntoPure (uPredI M) ( a) ( a).
Proof. by rewrite /IntoPure discrete_valid. Qed.
Global Instance from_pure_cmra_valid {A : cmraT} (a : A) :
@FromPure (uPredI M) ( a) ( a).
Global Instance from_pure_cmra_valid {A : cmraT} af (a : A) :
@FromPure (uPredI M) af ( a) ( a).
Proof.
rewrite /FromPure. eapply bi.pure_elim; [done|]=> ?.
rewrite /FromPure. eapply bi.pure_elim; [by apply affinely_if_elim|]=> ?.
rewrite -cmra_valid_intro //. by apply pure_intro.
Qed.
......
This diff is collapsed.
......@@ -43,18 +43,19 @@ Proof. by exists φ. Qed.
Hint Extern 0 (IntoPureT _ _) =>
notypeclasses refine (into_pureT_hint _ _ _) : typeclass_instances.
Class FromPure {PROP : bi} (P : PROP) (φ : Prop) :=
from_pure : ⌜φ⌝ P.
Arguments FromPure {_} _%I _%type_scope : simpl never.
Arguments from_pure {_} _%I _%type_scope {_}.
Hint Mode FromPure + ! - : typeclass_instances.
Class FromPureT {PROP : bi} (P : PROP) (φ : Type) :=
from_pureT : ψ : Prop, φ = ψ FromPure P ψ.
Lemma from_pureT_hint {PROP : bi} (P : PROP) (φ : Prop) : FromPure P φ FromPureT P φ.
Class FromPure {PROP : bi} (a : bool) (P : PROP) (φ : Prop) :=
from_pure : bi_affinely_if a ⌜φ⌝ P.
Arguments FromPure {_} _ _%I _%type_scope : simpl never.
Arguments from_pure {_} _ _%I _%type_scope {_}.
Hint Mode FromPure + + ! - : typeclass_instances.
Class FromPureT {PROP : bi} (a : bool) (P : PROP) (φ : Type) :=
from_pureT : ψ : Prop, φ = ψ FromPure a P ψ.
Lemma from_pureT_hint {PROP : bi} (a : bool) (P : PROP) (φ : Prop) :
FromPure a P φ FromPureT a P φ.
Proof. by exists φ. Qed.
Hint Extern 0 (FromPureT _ _) =>
notypeclasses refine (from_pureT_hint _ _ _) : typeclass_instances.
Hint Extern 0 (FromPureT _ _ _) =>
notypeclasses refine (from_pureT_hint _ _ _ _) : typeclass_instances.
Class IntoInternalEq {PROP : sbi} {A : ofeT} (P : PROP) (x y : A) :=
into_internal_eq : P x y.
......@@ -448,8 +449,8 @@ with the exception of:
*)
Instance into_pure_tc_opaque {PROP : bi} (P : PROP) φ :
IntoPure P φ IntoPure (tc_opaque P) φ := id.
Instance from_pure_tc_opaque {PROP : bi} (P : PROP) φ :
FromPure P φ FromPure (tc_opaque P) φ := id.
Instance from_pure_tc_opaque {PROP : bi} (a : bool) (P : PROP) φ :
FromPure a P φ FromPure a (tc_opaque P) φ := id.
Instance from_laterN_tc_opaque {PROP : sbi} n (P Q : PROP) :
FromLaterN n P Q FromLaterN n (tc_opaque P) Q := id.
Instance from_wand_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
......
......@@ -520,8 +520,8 @@ Proof.
Qed.
(** * Pure *)
Lemma tac_pure_intro Δ Q φ : FromPure Q φ φ envs_entails Δ Q.
Proof. intros ??. rewrite /envs_entails -(from_pure Q). by apply pure_intro. Qed.
Lemma tac_pure_intro Δ Q φ : FromPure false Q φ φ envs_entails Δ Q.
Proof. intros ??. rewrite /envs_entails -(from_pure _ Q). by apply pure_intro. Qed.
Lemma tac_pure Δ Δ' i p P φ Q :
envs_lookup_delete i Δ = Some (p, P, Δ')
......@@ -821,13 +821,14 @@ Qed.
Lemma tac_specialize_assert_pure Δ Δ' j q R P1 P2 φ Q :
envs_lookup j Δ = Some (q, R)
IntoWand q true R P1 P2
FromPure P1 φ
FromPure true P1 φ
envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ'
φ envs_entails Δ' Q envs_entails Δ Q.
Proof.
rewrite /envs_entails=> ????? <-. rewrite envs_simple_replace_singleton_sound //=.
rewrite -affinely_persistently_if_idemp into_wand /= -(from_pure P1).
rewrite pure_True // persistently_pure affinely_True_emp affinely_emp.
rewrite -affinely_persistently_if_idemp into_wand /= -(from_pure _ P1).
rewrite pure_True //= persistently_affinely persistently_pure
affinely_True_emp affinely_emp.
by rewrite emp_wand wand_elim_r.
Qed.
......@@ -926,14 +927,14 @@ Proof.
Qed.
Lemma tac_assert_pure Δ Δ' j P P' φ Q :
FromPure P φ
FromPure true P φ
FromAffinely P' P
envs_app false (Esnoc Enil j P') Δ = Some Δ'
φ envs_entails Δ' Q envs_entails Δ Q.
Proof.
rewrite /envs_entails => ???? <-. rewrite envs_app_singleton_sound //=.
rewrite -(from_affinely P') -(from_pure P) pure_True //.
by rewrite affinely_True_emp affinely_emp emp_wand.
rewrite -(from_affinely P') -(from_pure _ P) pure_True //.
by rewrite affinely_idemp affinely_True_emp affinely_emp emp_wand.
Qed.
Lemma tac_pose_proof Δ Δ' j P Q :
......
......@@ -157,12 +157,12 @@ Qed.
Global Instance into_pure_monPred_at P φ i : IntoPure P φ IntoPure (P i) φ.
Proof. rewrite /IntoPure=>->. by rewrite monPred_at_pure. Qed.
Global Instance from_pure_monPred_at P φ i : FromPure P φ FromPure (P i) φ.
Proof. rewrite /FromPure=><-. by rewrite monPred_at_pure. Qed.
Global Instance from_pure_monPred_at a P φ i : FromPure a P φ FromPure a (P i) φ.
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).
Proof. by rewrite /IntoPure monPred_at_in. Qed.
Global Instance from_pure_monPred_in i j : @FromPure PROP (monPred_in i j) (i j).
Proof. by rewrite /FromPure monPred_at_in. Qed.
Global Instance from_pure_monPred_in i j af : @FromPure PROP af (monPred_in i j) (i j).
Proof. by rewrite /FromPure monPred_at_in bi.affinely_if_elim. Qed.
Global Instance into_persistent_monPred_at p P Q 𝓠 i :
IntoPersistent p P Q MakeMonPredAt i Q 𝓠 IntoPersistent p (P i) 𝓠 | 0.
......
......@@ -230,7 +230,7 @@ Tactic Notation "iPureIntro" :=
iStartProof;
eapply tac_pure_intro;
[apply _ ||
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"
|].
......@@ -494,7 +494,7 @@ Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
[env_reflexivity || fail "iSpecialize:" H1 "not found"
|solve_to_wand H1
|apply _ ||
let Q := match goal with |- FromPure ?Q _ => Q end in
let Q := match goal with |- FromPure _ ?Q _ => Q end in
fail "iSpecialize:" Q "not pure"
|env_reflexivity
|done_if d (*goal*)
......@@ -1663,10 +1663,10 @@ Tactic Notation "iAssertCore" open_constr(Q)
let Hs := spec_pat.parse Hs in
lazymatch Hs with
| [SPureGoal ?d] =>
eapply tac_assert_pure with _ H Q _;
[env_reflexivity
|apply _ || fail "iAssert:" Q "not pure"
eapply tac_assert_pure with _ H Q _ _;
[apply _ || fail "iAssert:" Q "not pure"
|apply _
|env_reflexivity
|done_if d (*goal*)
|tac H]
| [SGoal (SpecGoal GPersistent _ ?Hs_frame [] ?d)] =>
......
......@@ -300,4 +300,18 @@ Lemma test_iNext_later_laterN P n : ▷^n ▷ P ⊢ ▷ ▷^n P.
Proof. iIntros "H". iNext. by iNext. Qed.
Lemma test_iNext_laterN_laterN P n1 n2 : ^n1 ^n2 P ^n1 ^n2 P.
Proof. iIntros "H". iNext. iNext. by iNext. Qed.
Lemma test_specialize_affine_pure (φ : Prop) P :
φ (bi_affinely ⌜φ⌝ - P) P.
Proof.
iIntros (Hφ) "H". by iSpecialize ("H" with "[% //]").
Qed.
Lemma test_assert_affine_pure (φ : Prop) P :
φ P P bi_affinely ⌜φ⌝.
Proof. iIntros (Hφ). iAssert (bi_affinely ⌜φ⌝) with "[%]" as "$"; auto. Qed.
Lemma test_assert_pure (φ : Prop) P :
φ P P ⌜φ⌝.
Proof. iIntros (Hφ). iAssert ⌜φ⌝%I with "[%]" as "$"; auto. Qed.
End tests.
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