From 3f257ee4a78073008bd29c5174e83163b8a0b167 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 18 Apr 2023 18:20:16 +0200
Subject: [PATCH 1/3] Use `resolve_tc` and remove all uses of "legacy" `apply`
in Iris Proof Mode.
---
iris/program_logic/ownp.v | 4 +-
iris/proofmode/ltac_tactics.v | 104 +++++++++++++++++++---------------
iris/proofmode/reduction.v | 4 +-
3 files changed, 62 insertions(+), 50 deletions(-)
diff --git a/iris/program_logic/ownp.v b/iris/program_logic/ownp.v
index 7acca3e5f..2b9e6c4d1 100644
--- a/iris/program_logic/ownp.v
+++ b/iris/program_logic/ownp.v
@@ -69,12 +69,12 @@ Theorem ownP_invariance Σ `{!ownPGpreS Λ Σ} s e σ1 t2 σ2 φ :
φ σ2.
Proof.
intros Hwp Hsteps. eapply (wp_invariance Σ Λ s e σ1 t2 σ2 _)=> //.
- iIntros (? κs).
+ iIntros (Hinv κs).
iMod (own_alloc (●E σ1 ⋅ ◯E σ1)) as (γσ) "[Hσ Hσf]";
first by apply auth_both_valid_discrete.
iExists (λ σ κs' _, own γσ (●E σ))%I, (λ _, True%I).
iFrame "Hσ".
- iMod (Hwp (OwnPGS _ _ _ _ γσ) with "[Hσf]") as "[$ H]";
+ iMod (Hwp (OwnPGS _ _ Hinv _ γσ) with "[Hσf]") as "[$ H]";
first by rewrite /ownP; iFrame.
iIntros "!> Hσ". iExists ∅. iMod "H" as (σ2') "[Hσf %]". rewrite /ownP.
iCombine "Hσ Hσf"
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 1018168a7..3439ddebe 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -7,6 +7,9 @@ From iris.proofmode Require Export classes notation.
From iris.prelude Require Import options.
Export ident.
+(** TODO: Move to some utility file *)
+Ltac resolve_tc := ltac2:(x |- Std.resolve_tc (Option.get (Ltac1.to_constr x))).
+
(** Tactic used for solving side-conditions arising from TC resolution in [iMod]
and [iInv]. *)
Ltac iSolveSideCondition :=
@@ -92,12 +95,12 @@ Tactic Notation "iStartProof" uconstr(PROP) :=
to find the corresponding bi. *)
| |- ?φ => notypeclasses refine ((λ P : PROP, @as_emp_valid_2 φ _ P) _ _ _);
[tc_solve || fail "iStartProof: not a BI assertion"
- |apply tac_start]
+ |notypeclasses refine (tac_start _ _)]
end.
Tactic Notation "iStopProof" :=
lazymatch goal with
- | |- envs_entails _ _ => apply tac_stop; pm_reduce
+ | |- envs_entails _ _ => notypeclasses refine (tac_stop _ _ _); pm_reduce
| |- _ => fail "iStopProof: proofmode not started"
end.
@@ -130,7 +133,7 @@ Ltac iFresh :=
(** * Context manipulation *)
Tactic Notation "iRename" constr(H1) "into" constr(H2) :=
- eapply tac_rename with H1 H2 _ _; (* (i:=H1) (j:=H2) *)
+ notypeclasses refine (tac_rename _ H1 H2 _ _ _ _ _); (* (i:=H1) (j:=H2) *)
[pm_reflexivity ||
let H1 := pretty_ident H1 in
fail "iRename:" H1 "not found"
@@ -181,7 +184,7 @@ Ltac iElaborateSelPat pat :=
end.
Local Ltac iClearHyp H :=
- eapply tac_clear with H _ _; (* (i:=H) *)
+ notypeclasses refine (tac_clear _ H _ _ _ _ _ _); (* (i:=H) *)
[pm_reflexivity ||
let H := pretty_ident H in
fail "iClear:" H "not found"
@@ -209,7 +212,7 @@ Tactic Notation "iClear" "select" open_constr(pat) :=
(** ** Simplification *)
Tactic Notation "iEval" tactic3(t) :=
iStartProof;
- eapply tac_eval;
+ notypeclasses refine (tac_eval _ _ _ _ _);
[let x := fresh in intros x; t; unfold x; reflexivity
|].
@@ -218,7 +221,7 @@ Local Ltac iEval_go t Hs :=
| [] => idtac
| ESelPure :: ?Hs => fail "iEval: %: unsupported selection pattern"
| ESelIdent _ ?H :: ?Hs =>
- eapply tac_eval_in with H _ _ _;
+ notypeclasses refine (tac_eval_in _ H _ _ _ _ _ _ _);
[pm_reflexivity || let H := pretty_ident H in fail "iEval:" H "not found"
|let x := fresh in intros x; t; unfold x; reflexivity
|pm_reduce; iEval_go t Hs]
@@ -248,7 +251,7 @@ Ltac, but it may be possible in Ltac2. *)
(** * Assumptions *)
Tactic Notation "iExact" constr(H) :=
- eapply tac_assumption with H _ _; (* (i:=H) *)
+ notypeclasses refine (tac_assumption _ H _ _ _ _ _ _); (* (i:=H) *)
[pm_reflexivity ||
let H := pretty_ident H in
fail "iExact:" H "not found"
@@ -293,14 +296,14 @@ Tactic Notation "iAssumption" :=
lazymatch Γ with
| Esnoc ?Γ ?j ?P => first
[pose proof (_ : FromAssumption p P Q) as Hass;
- eapply (tac_assumption _ j p P);
+ notypeclasses refine (tac_assumption _ j p P _ _ _ _);
[pm_reflexivity
|exact Hass
|pm_reduce; tc_solve ||
fail 2 "iAssumption: remaining hypotheses not affine and the goal not absorbing"]
|assert_fails (is_evar P);
- assert (P = False%I) as Hass by reflexivity;
- apply (tac_false_destruct _ j p P);
+ assert (P = False%I) as Hass by notypeclasses refine eq_refl;
+ notypeclasses refine (tac_false_destruct _ j p P _ _ _);
[pm_reflexivity
|exact Hass]
|find p Γ Q]
@@ -316,11 +319,11 @@ Tactic Notation "iAssumption" :=
(** * False *)
Tactic Notation "iExFalso" :=
iStartProof;
- apply tac_ex_falso.
+ notypeclasses refine (tac_ex_falso _ _ _).
(** * Making hypotheses intuitionistic or pure *)
Local Tactic Notation "iIntuitionistic" constr(H) "as" constr(H') :=
- eapply tac_intuitionistic with H H' _ _ _; (* (i:=H) (j:=H') *)
+ notypeclasses refine (tac_intuitionistic _ H H' _ _ _ _ _ _ _ _); (* (i:=H) (j:=H') *)
[pm_reflexivity ||
let H := pretty_ident H in
fail "iIntuitionistic:" H "not found"
@@ -339,7 +342,7 @@ Local Tactic Notation "iIntuitionistic" constr(H) "as" constr(H') :=
end].
Local Tactic Notation "iSpatial" constr(H) "as" constr(H') :=
- eapply tac_spatial with H H' _ _ _;
+ notypeclasses refine (tac_spatial _ H H' _ _ _ _ _ _ _);
[pm_reflexivity ||
let H := pretty_ident H in
fail "iSpatial:" H "not found"
@@ -353,7 +356,7 @@ Local Tactic Notation "iSpatial" constr(H) "as" constr(H') :=
end].
Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
- eapply tac_pure with H _ _ _; (* (i:=H1) *)
+ notypeclasses refine (tac_pure _ H _ _ _ _ _ _ _ _); (* (i:=H1) *)
[pm_reflexivity ||
let H := pretty_ident H in
fail "iPure:" H "not found"
@@ -367,13 +370,13 @@ Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
Tactic Notation "iEmpIntro" :=
iStartProof;
- eapply tac_emp_intro;
+ notypeclasses refine (tac_emp_intro _ _);
[pm_reduce; tc_solve ||
fail "iEmpIntro: spatial context contains non-affine hypotheses"].
Tactic Notation "iPureIntro" :=
iStartProof;
- eapply tac_pure_intro;
+ notypeclasses refine (tac_pure_intro _ _ _ _ _ _ _);
[tc_solve ||
let P := match goal with |- FromPure _ ?P _ => P end in
fail "iPureIntro:" P "not pure"
@@ -394,13 +397,13 @@ Ltac iFrameFinish :=
Ltac iFramePure t :=
iStartProof;
let φ := type of t in
- eapply (tac_frame_pure _ _ _ _ t);
+ notypeclasses refine (tac_frame_pure _ _ _ _ t _ _);
[tc_solve || fail "iFrame: cannot frame" φ
|iFrameFinish].
Ltac iFrameHyp H :=
iStartProof;
- eapply tac_frame with H _ _ _;
+ notypeclasses refine (tac_frame _ H _ _ _ _ _ _ _);
[pm_reflexivity ||
let H := pretty_ident H in
fail "iFrame:" H "not found"
@@ -472,7 +475,7 @@ Local Tactic Notation "iIntro" "(" simple_intropattern(x) ")" :=
iStartProof;
lazymatch goal with
| |- envs_entails _ _ =>
- eapply tac_forall_intro;
+ notypeclasses refine (tac_forall_intro _ _ _ _ _ _);
[tc_solve ||
let P := match goal with |- FromForall ?P _ _ => P end in
fail "iIntro: cannot turn" P "into a universal quantifier"
@@ -489,7 +492,7 @@ Local Tactic Notation "iIntro" constr(H) :=
iStartProof;
first
[(* (?Q → _) *)
- eapply tac_impl_intro with H _ _ _; (* (i:=H) *)
+ notypeclasses refine (tac_impl_intro _ H _ _ _ _ _ _ _ _); (* (i:=H) *)
[tc_solve
|pm_reduce; tc_solve ||
let P := lazymatch goal with |- Persistent ?P => P end in
@@ -506,7 +509,7 @@ Local Tactic Notation "iIntro" constr(H) :=
| _ => idtac (* subgoal *)
end]
|(* (_ -∗ _) *)
- eapply tac_wand_intro with H _ _; (* (i:=H) *)
+ notypeclasses refine (tac_wand_intro _ H _ _ _ _ _); (* (i:=H) *)
[tc_solve
| pm_reduce;
lazymatch goal with
@@ -522,7 +525,7 @@ Local Tactic Notation "iIntro" "#" constr(H) :=
iStartProof;
first
[(* (?P → _) *)
- eapply tac_impl_intro_intuitionistic with H _ _ _; (* (i:=H) *)
+ notypeclasses refine (tac_impl_intro_intuitionistic _ H _ _ _ _ _ _ _); (* (i:=H) *)
[tc_solve
|tc_solve ||
let P := match goal with |- IntoPersistent _ ?P _ => P end in
@@ -535,7 +538,7 @@ Local Tactic Notation "iIntro" "#" constr(H) :=
| _ => idtac (* subgoal *)
end]
|(* (?P -∗ _) *)
- eapply tac_wand_intro_intuitionistic with H _ _ _; (* (i:=H) *)
+ notypeclasses refine (tac_wand_intro_intuitionistic _ H _ _ _ _ _ _ _ _); (* (i:=H) *)
[tc_solve
|tc_solve ||
let P := match goal with |- IntoPersistent _ ?P _ => P end in
@@ -562,11 +565,11 @@ Local Tactic Notation "iIntro" "_" :=
iStartProof;
first
[(* (?Q → _) *)
- eapply tac_impl_intro_drop;
+ notypeclasses refine (tac_impl_intro_drop _ _ _ _ _ _);
[tc_solve
|(* subgoal *)]
|(* (_ -∗ _) *)
- eapply tac_wand_intro_drop;
+ notypeclasses refine (tac_wand_intro_drop _ _ _ _ _ _ _);
[tc_solve
|tc_solve ||
let P := match goal with |- TCOr (Affine ?P) _ => P end in
@@ -614,25 +617,26 @@ Ltac iForallRevert x :=
lazymatch type of A with
| Prop =>
revert x; first
- [eapply tac_pure_revert;
+ [notypeclasses refine (tac_pure_revert _ _ _ _ _ _);
[tc_solve (* [MakeAffinely], should never fail *)
|]
|err x]
| _ =>
revert x; first
- [apply tac_forall_revert;
+ [notypeclasses refine (tac_forall_revert _ _ _);
(* Ensure the name [x] is preserved, see [test_iRevert_order_and_names]. *)
lazymatch goal with
| |- envs_entails ?Δ (bi_forall ?P) =>
change (envs_entails Δ (∀ x, P x)); lazy beta
end
|err x]
+ | _ => revert x; first [notypeclasses refine (tac_forall_revert _ _ _)|err x]
end.
(** The tactic [iRevertHyp H with tac] reverts the hypothesis [H] and calls
[tac] with a Boolean that is [true] iff [H] was in the intuitionistic context. *)
Tactic Notation "iRevertHyp" constr(H) "with" tactic1(tac) :=
- eapply tac_revert with H;
+ notypeclasses refine (tac_revert _ H _ _);
[lazymatch goal with
| |- match envs_lookup_delete true ?i ?Δ with _ => _ end =>
lazymatch eval pm_eval in (envs_lookup_delete true i Δ) with
@@ -1100,8 +1104,9 @@ Tactic Notation "iPoseProofCore" open_constr(lem)
| ident =>
let Htmp := iFresh in
iPoseProofCoreHyp t as Htmp; spec_tac Htmp; [..|tac Htmp]
- | _ => iPoseProofCoreLem t as (fun Htmp => spec_tac Htmp; [..|tac Htmp])
- end.
+ | _ => iPoseProofCoreLem t as (fun Htmp =>
+ spec_tac Htmp; [..|tac Htmp])
+ end; resolve_tc lem.
(** * The apply tactic *)
(** [iApply lem] takes an argument [lem : P₁ -∗ .. -∗ Pₙ -∗ Q] (after the
@@ -1123,8 +1128,9 @@ premises [n], the tactic will have the following behavior:
(* The helper [iApplyHypExact] takes care of the [n=0] case. It fails with level
0 if we should proceed to the [n > 0] case, and with level 1 if there is an
actual error. *)
+
Local Ltac iApplyHypExact H :=
- eapply tac_assumption with H _ _; (* (i:=H) *)
+ notypeclasses refine (tac_assumption _ H _ _ _ _ _ _); (* (i:=H) *)
[pm_reflexivity
|tc_solve
|pm_reduce; tc_solve ||
@@ -1132,7 +1138,7 @@ Local Ltac iApplyHypExact H :=
Local Ltac iApplyHypLoop H :=
first
- [eapply tac_apply with H _ _ _;
+ [notypeclasses refine (tac_apply _ H _ _ _ _ _ _ _);
[pm_reflexivity
|tc_solve
|pm_reduce]
@@ -1154,21 +1160,21 @@ Tactic Notation "iApply" open_constr(lem) :=
(** * Disjunction *)
Tactic Notation "iLeft" :=
iStartProof;
- eapply tac_or_l;
+ notypeclasses refine (tac_or_l _ _ _ _ _ _);
[tc_solve ||
let P := match goal with |- FromOr ?P _ _ => P end in
fail "iLeft:" P "not a disjunction"
|(* subgoal *)].
Tactic Notation "iRight" :=
iStartProof;
- eapply tac_or_r;
+ notypeclasses refine (tac_or_r _ _ _ _ _ _);
[tc_solve ||
let P := match goal with |- FromOr ?P _ _ => P end in
fail "iRight:" P "not a disjunction"
|(* subgoal *)].
Tactic Notation "iOrDestruct" constr(H) "as" constr(H1) constr(H2) :=
- eapply tac_or_destruct with H _ H1 H2 _ _ _; (* (i:=H) (j1:=H1) (j2:=H2) *)
+ notypeclasses refine (tac_or_destruct _ H _ H1 H2 _ _ _ _ _ _ _); (* (i:=H) (j1:=H1) (j2:=H2) *)
[pm_reflexivity ||
let H := pretty_ident H in
fail "iOrDestruct:" H "not found"
@@ -1187,7 +1193,7 @@ Tactic Notation "iOrDestruct" constr(H) "as" constr(H1) constr(H2) :=
(** * Conjunction and separating conjunction *)
Tactic Notation "iSplit" :=
iStartProof;
- eapply tac_and_split;
+ notypeclasses refine (tac_and_split _ _ _ _ _ _ _);
[tc_solve ||
let P := match goal with |- FromAnd ?P _ _ => P end in
fail "iSplit:" P "not a conjunction"
@@ -1199,7 +1205,7 @@ Tactic Notation "iSplitL" constr(Hs) :=
let Hs := String.words Hs in
let Hs := eval vm_compute in (INamed <$> Hs) in
let Δ := iGetCtx in
- eapply tac_sep_split with Left Hs _ _; (* (js:=Hs) *)
+ notypeclasses refine (tac_sep_split _ Left Hs _ _ _ _ _); (* (js:=Hs) *)
[tc_solve ||
let P := match goal with |- FromSep ?P _ _ => P end in
fail "iSplitL:" P "not a separating conjunction"
@@ -1215,7 +1221,7 @@ Tactic Notation "iSplitR" constr(Hs) :=
let Hs := String.words Hs in
let Hs := eval vm_compute in (INamed <$> Hs) in
let Δ := iGetCtx in
- eapply tac_sep_split with Right Hs _ _; (* (js:=Hs) *)
+ notypeclasses refine (tac_sep_split _ Right Hs _ _ _ _ _); (* (js:=Hs) *)
[tc_solve ||
let P := match goal with |- FromSep ?P _ _ => P end in
fail "iSplitR:" P "not a separating conjunction"
@@ -1230,7 +1236,8 @@ Tactic Notation "iSplitL" := iSplitR "".
Tactic Notation "iSplitR" := iSplitL "".
Local Tactic Notation "iAndDestruct" constr(H) "as" constr(H1) constr(H2) :=
- eapply tac_and_destruct with H _ H1 H2 _ _ _; (* (i:=H) (j1:=H1) (j2:=H2) *)
+ notypeclasses refine (tac_and_destruct _ H _ H1 H2 _ _ _ _ _ _ _);
+ (* (i:=H) (j1:=H1) (j2:=H2) *)
[pm_reflexivity ||
let H := pretty_ident H in
fail "iAndDestruct:" H "not found"
@@ -1251,7 +1258,7 @@ Local Tactic Notation "iAndDestruct" constr(H) "as" constr(H1) constr(H2) :=
end].
Local Tactic Notation "iAndDestructChoice" constr(H) "as" constr(d) constr(H') :=
- eapply tac_and_destruct_choice with H _ d H' _ _ _;
+ notypeclasses refine (tac_and_destruct_choice _ H _ d H' _ _ _ _ _ _ _);
[pm_reflexivity || fail "iAndDestructChoice:" H "not found"
|pm_reduce; tc_solve ||
let P := match goal with |- TCOr (IntoAnd _ ?P _ _) _ => P end in
@@ -1268,7 +1275,7 @@ Local Tactic Notation "iAndDestructChoice" constr(H) "as" constr(d) constr(H') :
Ltac _iExists x :=
iStartProof;
- eapply tac_exist;
+ notypeclasses refine (tac_exist _ _ _ _ _);
[tc_solve ||
let P := match goal with |- FromExist ?P _ => P end in
fail "iExists:" P "not an existential"
@@ -1280,7 +1287,7 @@ Tactic Notation "iExists" ne_uconstr_list_sep(xs,",") :=
Local Tactic Notation "iExistDestruct" constr(H)
"as" simple_intropattern(x) constr(Hx) :=
- eapply tac_exist_destruct with H _ Hx _ _ _; (* (i:=H) (j:=Hx) *)
+ notypeclasses refine (tac_exist_destruct _ H _ Hx _ _ _ _ _ _ _); (* (i:=H) (j:=Hx) *)
[pm_reflexivity ||
let H := pretty_ident H in
fail "iExistDestruct:" H "not found"
@@ -1335,7 +1342,7 @@ Tactic Notation "iNext" := iModIntro (▷^_ _)%I.
(** * Update modality *)
Tactic Notation "iModCore" constr(H) "as" constr(H') :=
- eapply tac_modal_elim with H H' _ _ _ _ _ _;
+ notypeclasses refine (tac_modal_elim _ H H' _ _ _ _ _ _ _ _ _ _ _);
[pm_reflexivity || fail "iMod:" H "not found"
|tc_solve ||
let P := match goal with |- ElimModal _ _ _ ?P _ _ _ => P end in
@@ -1906,7 +1913,8 @@ Tactic Notation "iAssertCore" open_constr(Q)
| _ => fail "iAssert: exactly one specialization pattern should be given"
end;
let H := iFresh in
- eapply tac_assert with H Q;
+ notypeclasses refine (tac_assert _ H Q _ _);
+ resolve_tc Q;
[pm_reduce;
iSpecializeCore H with hnil pats as p; [..|tac H]].
@@ -1945,7 +1953,7 @@ Local Ltac iRewriteFindPred :=
Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) :=
iPoseProofCore lem as true (fun Heq =>
- eapply (tac_rewrite _ Heq _ _ lr);
+ notypeclasses refine (tac_rewrite _ Heq _ _ lr _ _ _ _ _ _ _ _ _);
[pm_reflexivity ||
let Heq := pretty_ident Heq in
fail "iRewrite:" Heq "not found"
@@ -1960,7 +1968,7 @@ Tactic Notation "iRewrite" "-" open_constr(lem) := iRewriteCore Left lem.
Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) "in" constr(H) :=
iPoseProofCore lem as true (fun Heq =>
- eapply (tac_rewrite_in _ Heq _ _ H _ _ lr);
+ notypeclasses refine (tac_rewrite_in _ Heq _ _ H _ _ lr _ _ _ _ _ _ _ _ _ _);
[pm_reflexivity ||
let Heq := pretty_ident Heq in
fail "iRewrite:" Heq "not found"
@@ -2129,7 +2137,9 @@ Tactic Notation "iInv" constr(N) "as" "(" ne_simple_intropattern_list(xs) ")"
(** Miscellaneous *)
Tactic Notation "iAccu" :=
- iStartProof; eapply tac_accu; [pm_reflexivity || fail "iAccu: not an evar"].
+ iStartProof;
+ notypeclasses refine (tac_accu _ _ _);
+ [pm_reflexivity || fail "iAccu: not an evar"].
(** Automation *)
Global Hint Extern 0 (_ ⊢ _) => iStartProof : core.
diff --git a/iris/proofmode/reduction.v b/iris/proofmode/reduction.v
index be61cf47d..716117fe9 100644
--- a/iris/proofmode/reduction.v
+++ b/iris/proofmode/reduction.v
@@ -58,7 +58,9 @@ Ltac pm_reduce :=
(* Use [change_no_check] instead of [change] to avoid performing the
conversion check twice. *)
match goal with |- ?u => let v := pm_eval u in change_no_check v end.
-Ltac pm_reflexivity := pm_reduce; exact eq_refl.
+
+Ltac pm_reflexivity :=
+ pm_reduce; notypeclasses refine eq_refl.
(** Called by many tactics for redexes that are created by instantiation.
This cannot create any envs redexes so we just do the cbn part. *)
--
GitLab
From f8bc6e64f68ad92485db731c112be3b90cfc679b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 8 Oct 2024 10:59:16 +0100
Subject: [PATCH 2/3] Call `resolve_tc` in `iSpecialize`.
---
iris/proofmode/ltac_tactics.v | 11 +++++++++--
tests/proofmode.v | 4 +---
2 files changed, 10 insertions(+), 5 deletions(-)
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 3439ddebe..2c3237806 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -1078,10 +1078,17 @@ Tactic Notation "iSpecializeCore" open_constr(t) "as" constr(p) :=
end
end.
+(** To finish the user-facing [iSpecialize] tactics we call [resolve_tc] to
+solve remaining TC obligations in the given term [t]. See [test_iSpecialize_tc]
+for a test.
+
+Note that we do not call [resolve_tc] in the internal [iSpecializeCore] tactics
+above, because that would be too eager. It will only be called in the very end
+by [iPoseProofCore] below. *)
Tactic Notation "iSpecialize" open_constr(t) :=
- iSpecializeCore t as false.
+ iSpecializeCore t as false; resolve_tc t.
Tactic Notation "iSpecialize" open_constr(t) "as" "#" :=
- iSpecializeCore t as true.
+ iSpecializeCore t as true; resolve_tc t.
(** The tactic [iPoseProofCore lem as p tac] inserts the resource
described by [lem] into the context. The tactic takes a continuation [tac] as
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 4d6ba28db..a2c768b7d 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -636,9 +636,7 @@ Proof. iExists {[ 1%positive ]}, ∅. auto. Qed.
Lemma test_iSpecialize_tc P : (∀ x y z : gset positive, P) -∗ P.
Proof.
- iIntros "H".
- (* FIXME: this [unshelve] and [apply _] should not be needed. *)
- unshelve iSpecialize ("H" $! ∅ {[ 1%positive ]} ∅); try apply _. done.
+ iIntros "H". iSpecialize ("H" $! ∅ {[ 1%positive ]} ∅). done.
Qed.
Lemma test_iFrame_pure `{!BiInternalEq PROP} {A : ofe} (φ : Prop) (y z : A) :
--
GitLab
From fb81776a93091130748e169ee5c4297e6f73a1ad Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 8 Oct 2024 14:23:01 +0100
Subject: [PATCH 3/3] Use `refine` for `Frame` base cases.
---
iris/proofmode/class_instances_frame.v | 30 ++++++++++++++++----------
1 file changed, 19 insertions(+), 11 deletions(-)
diff --git a/iris/proofmode/class_instances_frame.v b/iris/proofmode/class_instances_frame.v
index 7a399e4d7..a38d418ff 100644
--- a/iris/proofmode/class_instances_frame.v
+++ b/iris/proofmode/class_instances_frame.v
@@ -4,36 +4,44 @@ From iris.prelude Require Import options.
Import bi.
(** This file defines the instances that make up the framing machinery. *)
-
-Section class_instances_frame.
-Context {PROP : bi}.
-Implicit Types P Q R : PROP.
-
(** When framing [R] against itself, we leave [True] if possible (via
[frame_here_absorbing] or [frame_affinely_here_absorbing]) since it is a weaker
goal. Otherwise we leave [emp] via [frame_here].
Only if all those options fail, we start decomposing [R], via instances like
[frame_exist]. To ensure that, all other instances must have cost > 1. *)
-Global Instance frame_here_absorbing p R :
- QuickAbsorbing R → Frame p R R True | 0.
+Lemma frame_here_absorbing {PROP : bi} p (R : PROP) :
+ QuickAbsorbing R → Frame p R R True.
Proof.
rewrite /QuickAbsorbing /Frame. intros.
by rewrite intuitionistically_if_elim sep_elim_l.
Qed.
-Global Instance frame_here p R : Frame p R R emp | 1.
+Lemma frame_here {PROP : bi} p (R : PROP) : Frame p R R emp.
Proof. intros. by rewrite /Frame intuitionistically_if_elim sep_elim_l. Qed.
-Global Instance frame_affinely_here_absorbing p R :
- QuickAbsorbing R → Frame p (<affine> R) R True | 0.
+Lemma frame_affinely_here_absorbing {PROP : bi} p (R : PROP) :
+ QuickAbsorbing R → Frame p (<affine> R) R True.
Proof.
rewrite /QuickAbsorbing /Frame. intros.
rewrite intuitionistically_if_elim affinely_elim. apply sep_elim_l, _.
Qed.
-Global Instance frame_affinely_here p R : Frame p (<affine> R) R emp | 1.
+Lemma frame_affinely_here {PROP : bi} p (R : PROP) : Frame p (<affine> R) R emp.
Proof.
intros. rewrite /Frame intuitionistically_if_elim affinely_elim.
apply sep_elim_l, _.
Qed.
+Global Hint Extern 0 (Frame _ _ _ _) =>
+ notypeclasses refine (frame_here_absorbing _ _ _) : typeclass_instances.
+Global Hint Extern 1 (Frame _ _ _ _) =>
+ notypeclasses refine (frame_here _ _) : typeclass_instances.
+Global Hint Extern 0 (Frame _ (<affine> _) _ _) =>
+ notypeclasses refine (frame_affinely_here_absorbing _ _ _) : typeclass_instances.
+Global Hint Extern 1 (Frame _ (<affine> _) _ _) =>
+ notypeclasses refine (frame_affinely_here _ _) : typeclass_instances.
+
+Section class_instances_frame.
+Context {PROP : bi}.
+Implicit Types P Q R : PROP.
+
Global Instance frame_here_pure_persistent a φ Q :
FromPure a Q φ → Frame true ⌜φ⌝ Q emp | 2.
Proof.
--
GitLab