Commit f8e99264 authored by Robbert Krebbers's avatar Robbert Krebbers

Move `iPoseProofCore*` tactics up so others can depend on it.

parent 1d23872c
......@@ -595,7 +595,7 @@ Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
ident(x5) ident(x6) ident(x7) ident(x8) ")" constr(Hs) :=
iRevert Hs; iRevert ( x1 x2 x3 x4 x5 x6 x7 x8 ).
(** * Specialize *)
(** * The specialize and pose proof tactics *)
Record iTrm {X As S} :=
ITrm { itrm : X ; itrm_vars : hlist As ; itrm_hyps : S }.
Arguments ITrm {_ _ _} _ _ _.
......@@ -606,6 +606,74 @@ Notation "( H $! x1 .. xn 'with' pat )" :=
(ITrm H (hcons x1 .. (hcons xn hnil) ..) pat) (at level 0, x1, xn at level 9).
Notation "( H 'with' pat )" := (ITrm H hnil pat) (at level 0).
(* The tactic [iIntoEmpValid] tactic solves a goal [bi_emp_valid Q]. The
argument [t] must be a Coq term whose type is of the following shape:
[∀ (x_1 : A_1) .. (x_n : A_n), φ]
and so that we have an instance `AsValid φ Q`.
Examples of such [φ]s are
- [bi_emp_valid P], in which case [Q] should be [P]
- [P1 ⊢ P2], in which case [Q] should be [P1 -∗ P2]
- [P1 ⊣⊢ P2], in which case [Q] should be [P1 ↔ P2]
The tactic instantiates each dependent argument [x_i] with an evar and generates
a goal [R] for each non-dependent argument [x_i : R]. For example, if the
original goal was [Q] and [t] has type [∀ x, P x → Q], then it generates an evar
[?x] for [x] and a subgoal [P ?x]. *)
Local Ltac iIntoEmpValid t :=
let go_specialize t tT :=
lazymatch tT with (* We do not use hnf of tT, because, if
entailment is not opaque, then it would
unfold it. *)
| ?P ?Q => let H := fresh in assert P as H; [|iIntoEmpValid uconstr:(t H); clear H]
| _ : ?T, _ =>
(* Put [T] inside an [id] to avoid TC inference from being invoked. *)
(* This is a workarround for Coq bug #6583. *)
let e := fresh in evar (e:id T);
let e' := eval unfold e in e in clear e; iIntoEmpValid (t e')
end
in
(* We try two reduction tactics for the type of t before trying to
specialize it. We first try the head normal form in order to
unfold all the definition that could hide an entailment. Then,
we try the much weaker [eval cbv zeta], because entailment is
not necessarilly opaque, and could be unfolded by [hnf].
However, for calling type class search, we only use [cbv zeta]
in order to make sure we do not unfold [bi_emp_valid]. *)
let tT := type of t in
first
[ let tT' := eval hnf in tT in go_specialize t tT'
| let tT' := eval cbv zeta in tT in go_specialize t tT'
| let tT' := eval cbv zeta in tT in
notypeclasses refine (as_emp_valid_1 tT _ _);
[iSolveTC || fail 1 "iPoseProof: not a BI assertion"
|exact t]].
Tactic Notation "iPoseProofCoreHyp" constr(H) "as" constr(Hnew) :=
eapply tac_pose_proof_hyp with _ _ H _ Hnew _;
[pm_reflexivity ||
let H := pretty_ident H in
fail "iPoseProof:" H "not found"
|pm_reflexivity ||
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 Hnew in
fail "iPoseProof:" Hnew "not fresh"
|tac];
(* Solve all remaining TC premises generated by [iIntoEmpValid] *)
try iSolveTC.
(** There is some hacky stuff going on here: because of Coq bug #6583, unresolved
type classes in the arguments `xs` are resolved at arbitrary moments. Tactics
like `apply`, `split` and `eexists` wrongly trigger type class search to resolve
......@@ -807,75 +875,6 @@ Tactic Notation "iSpecialize" open_constr(t) :=
Tactic Notation "iSpecialize" open_constr(t) "as" "#" :=
iSpecializeCore t as true.
(** * Pose proof *)
(* The tactic [iIntoEmpValid] tactic solves a goal [bi_emp_valid Q]. The
argument [t] must be a Coq term whose type is of the following shape:
[∀ (x_1 : A_1) .. (x_n : A_n), φ]
and so that we have an instance `AsValid φ Q`.
Examples of such [φ]s are
- [bi_emp_valid P], in which case [Q] should be [P]
- [P1 ⊢ P2], in which case [Q] should be [P1 -∗ P2]
- [P1 ⊣⊢ P2], in which case [Q] should be [P1 ↔ P2]
The tactic instantiates each dependent argument [x_i] with an evar and generates
a goal [R] for each non-dependent argument [x_i : R]. For example, if the
original goal was [Q] and [t] has type [∀ x, P x → Q], then it generates an evar
[?x] for [x] and a subgoal [P ?x]. *)
Local Ltac iIntoEmpValid t :=
let go_specialize t tT :=
lazymatch tT with (* We do not use hnf of tT, because, if
entailment is not opaque, then it would
unfold it. *)
| ?P ?Q => let H := fresh in assert P as H; [|iIntoEmpValid uconstr:(t H); clear H]
| _ : ?T, _ =>
(* Put [T] inside an [id] to avoid TC inference from being invoked. *)
(* This is a workarround for Coq bug #6583. *)
let e := fresh in evar (e:id T);
let e' := eval unfold e in e in clear e; iIntoEmpValid (t e')
end
in
(* We try two reduction tactics for the type of t before trying to
specialize it. We first try the head normal form in order to
unfold all the definition that could hide an entailment. Then,
we try the much weaker [eval cbv zeta], because entailment is
not necessarilly opaque, and could be unfolded by [hnf].
However, for calling type class search, we only use [cbv zeta]
in order to make sure we do not unfold [bi_emp_valid]. *)
let tT := type of t in
first
[ let tT' := eval hnf in tT in go_specialize t tT'
| let tT' := eval cbv zeta in tT in go_specialize t tT'
| let tT' := eval cbv zeta in tT in
notypeclasses refine (as_emp_valid_1 tT _ _);
[iSolveTC || fail 1 "iPoseProof: not a BI assertion"
|exact t]].
Tactic Notation "iPoseProofCoreHyp" constr(H) "as" constr(Hnew) :=
eapply tac_pose_proof_hyp with _ _ H _ Hnew _;
[pm_reflexivity ||
let H := pretty_ident H in
fail "iPoseProof:" H "not found"
|pm_reflexivity ||
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 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
described by [lem] into the context. The tactic takes a continuation [tac] as
its argument, which is called with a temporary fresh name [H] that refers to
......@@ -920,6 +919,7 @@ Tactic Notation "iPoseProofCore" open_constr(lem)
end
end.
(** * The apply tactic *)
(** [iApply lem] takes an argument [lem : P₁ -∗ .. -∗ Pₙ -∗ Q] (after the
specialization patterns in [lem] have been executed), where [Q] should match
the goal, and generates new goals [P1] ... [Pₙ]. Depending on the number of
......
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