From 953c27ac4665607e352d1cffd07e3f3744dce020 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 25 Dec 2018 09:17:41 +0100
Subject: [PATCH] Refactor `iPoseProof`.
Split it up into more logical parts.
---
tests/proofmode.ref | 24 +++++----------
theories/proofmode/ltac_tactics.v | 50 +++++++++++++++++--------------
2 files changed, 35 insertions(+), 39 deletions(-)
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 3ad30a0bc..85296f026 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -467,12 +467,14 @@ Tactic failure: iStartProof: not a BI assertion.
The command has indeed failed with message:
In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
"iPoseProofCore (open_constr) as (constr) (constr) (tactic)",
-"<iris.proofmode.ltac_tactics.iPoseProofCore_go>" and
+"iPoseProofCoreLem (constr) as (constr) before_tc (tactic)" and
"<iris.proofmode.ltac_tactics.iIntoEmpValid>", last call failed.
Tactic failure: iPoseProof: not a BI assertion.
The command has indeed failed with message:
In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
-"iPoseProofCore (open_constr) as (constr) (constr) (tactic)",
+"iPoseProofCore (open_constr) as (constr) (constr) (tactic)",
+"iPoseProofCoreLem (constr) as (constr) before_tc (tactic)",
+"tac" (bound to spec_tac ltac:(()); [ .. | tac Htmp ]),
"tac" (bound to fun H => iDestructHyp H as pat),
"iDestructHyp (constr) as (constr)",
"<iris.proofmode.ltac_tactics.iDestructHypFindPat>",
@@ -513,11 +515,7 @@ invalid.
: string
The command has indeed failed with message:
In nested Ltac calls to "iApply (open_constr)",
-"iPoseProofCore (open_constr) as (constr) (constr) (tactic)",
-"<iris.proofmode.ltac_tactics.iPoseProofCore_go>",
-"<iris.proofmode.ltac_tactics.iPoseProofCore_go>",
-"<iris.proofmode.ltac_tactics.iPoseProofCore_go>",
-"goal_tac" (bound to fun _ => spec_tac ltac:(()); [ .. | tac Htmp ]),
+"iPoseProofCore (open_constr) as (constr) (constr) (tactic)",
"tac" (bound to fun H => iApplyHyp H) and "iApplyHyp (constr)", last call
failed.
Tactic failure: iApply: cannot apply P.
@@ -525,11 +523,7 @@ Tactic failure: iApply: cannot apply P.
: string
The command has indeed failed with message:
In nested Ltac calls to "iApply (open_constr)",
-"iPoseProofCore (open_constr) as (constr) (constr) (tactic)",
-"<iris.proofmode.ltac_tactics.iPoseProofCore_go>",
-"<iris.proofmode.ltac_tactics.iPoseProofCore_go>",
-"<iris.proofmode.ltac_tactics.iPoseProofCore_go>",
-"goal_tac" (bound to fun _ => spec_tac ltac:(()); [ .. | tac Htmp ]),
+"iPoseProofCore (open_constr) as (constr) (constr) (tactic)",
"tac" (bound to fun H => iApplyHyp H) and "iApplyHyp (constr)", last call
failed.
Tactic failure: iApply: Q
@@ -538,11 +532,7 @@ not absorbing and the remaining hypotheses not affine.
: string
The command has indeed failed with message:
In nested Ltac calls to "iApply (open_constr)",
-"iPoseProofCore (open_constr) as (constr) (constr) (tactic)",
-"<iris.proofmode.ltac_tactics.iPoseProofCore_go>",
-"<iris.proofmode.ltac_tactics.iPoseProofCore_go>",
-"<iris.proofmode.ltac_tactics.iPoseProofCore_go>",
-"goal_tac" (bound to fun _ => spec_tac ltac:(()); [ .. | tac Htmp ]),
+"iPoseProofCore (open_constr) as (constr) (constr) (tactic)",
"tac" (bound to fun H => iApplyHyp H) and "iApplyHyp (constr)", last call
failed.
Tactic failure: iApply: Q
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index d9022ec2c..98800febb 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -847,25 +847,25 @@ Local Ltac iIntoEmpValid t :=
[iSolveTC || fail 1 "iPoseProof: not a BI assertion"
|exact t]].
-Local Ltac iPoseProofCore_go Htmp t goal_tac :=
- lazymatch type of t with
- | ident =>
- eapply tac_pose_proof_hyp with _ _ t _ Htmp _;
+Tactic Notation "iPoseProofCoreHyp" constr(H) "as" constr(Hnew) :=
+ eapply tac_pose_proof_hyp with _ _ H _ Hnew _;
[pm_reflexivity ||
- let t := pretty_ident t in
- fail "iPoseProof:" t "not found"
+ let H := pretty_ident H in
+ fail "iPoseProof:" H "not found"
|pm_reflexivity ||
- let Htmp := pretty_ident Htmp in
- fail "iPoseProof:" Htmp "not fresh"
- |goal_tac ()]
- | _ =>
- eapply tac_pose_proof with _ Htmp _; (* (j:=H) *)
- [iIntoEmpValid t
+ let Htmp := pretty_ident Hnew in
+ fail "iPoseProof:" Hnew "not fresh"
+ |].
+
+Tactic Notation "iPoseProofCoreLem"
+ constr(lem) "as" constr(Hnew) "before_tc" tactic(tac) :=
+ eapply tac_pose_proof with _ Hnew _; (* (j:=H) *)
+ [iIntoEmpValid lem
|pm_reflexivity ||
- let Htmp := pretty_ident Htmp in
- fail "iPoseProof:" Htmp "not fresh"
- |goal_tac ()]
- end;
+ let Htmp := pretty_ident Hnew in
+ fail "iPoseProof:" Hnew "not fresh"
+ |tac];
+ (* Solve all remaining TC premises generated by [iIntoEmpValid] *)
try iSolveTC.
(** The tactic [iPoseProofCore lem as p lazy_tc tac] inserts the resource
@@ -878,8 +878,8 @@ There are a couple of additional arguments:
- The argument [p] is like that of [iSpecialize]. It is a Boolean that denotes
whether the conclusion of the specialized term [lem] is persistent.
- The argument [lazy_tc] denotes whether type class inference on the premises
- of [lem] should be performed before (if [lazy_tc = false]) or after, i.e.
- lazily (if [lazy_tc = true]) [tac H] is called.
+ of [lem] should be performed before (if [lazy_tc = false]) or after (if
+ [lazy_tc = true]) [tac H] is called.
Both variants of [lazy_tc] are used in other tactics that build on top of
[iPoseProofCore]:
@@ -898,12 +898,18 @@ Tactic Notation "iPoseProofCore" open_constr(lem)
let t := lazymatch type of t with string => constr:(INamed t) | _ => t end in
let spec_tac _ :=
lazymatch lem with
- | ITrm ?t ?xs ?pat => iSpecializeCore (ITrm Htmp xs pat) as p
+ | ITrm _ ?xs ?pat => iSpecializeCore (ITrm Htmp xs pat) as p
| _ => idtac
end in
- lazymatch eval compute in lazy_tc with
- | true => iPoseProofCore_go Htmp t ltac:(fun _ => spec_tac (); [..| tac Htmp ])
- | false => iPoseProofCore_go Htmp t spec_tac; [..| tac Htmp ]
+ lazymatch type of t with
+ | ident => iPoseProofCoreHyp t as Htmp; spec_tac (); [..|tac Htmp]
+ | _ =>
+ lazymatch eval compute in lazy_tc with
+ | true =>
+ iPoseProofCoreLem t as Htmp before_tc (spec_tac (); [..|tac Htmp])
+ | false =>
+ iPoseProofCoreLem t as Htmp before_tc (spec_tac ()); [..|tac Htmp]
+ end
end.
(** [iApply lem] takes an argument [lem : P₠-∗ .. -∗ Pₙ -∗ Q] (after the
--
GitLab