Skip to content
GitLab
Menu
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Lennard Gäher
Iris
Commits
1471ae26
Commit
1471ae26
authored
Jun 16, 2018
by
Ralf Jung
Browse files
Merge branch 'ralf/errors' into 'gen_proofmode'
Improve and test more proof mode error messages See merge request FP/iriscoq!160
parents
f510b666
49f26fdc
Changes
3
Hide whitespace changes
Inline
Sidebyside
tests/proofmode.ref
View file @
1471ae26
...
...
@@ 36,12 +36,12 @@ Ltac call to "done" failed.
No applicable tactic.
The command has indeed failed with message:
In nested Ltac calls to "iClear (constr)", "iElaborateSelPat" and
"iElaborateSelPat_go", last call failed.
Tactic failure: iElaborateSelPat:
(INamed
"HQ"
)
not found.
"
<iris.proofmode.ltac_tactics.
iElaborateSelPat_go
>
", last call failed.
Tactic failure: iElaborateSelPat: "HQ" not found.
The command has indeed failed with message:
In nested Ltac calls to "iClear (constr)", "iElaborateSelPat" and
"iElaborateSelPat_go", last call failed.
Tactic failure: iElaborateSelPat:
(INamed
"HQ"
)
not found.
"
<iris.proofmode.ltac_tactics.
iElaborateSelPat_go
>
", last call failed.
Tactic failure: iElaborateSelPat: "HQ" not found.
The command has indeed failed with message:
In nested Ltac calls to "iSpecialize (open_constr)",
"iSpecializeCore (open_constr) as (constr)",
...
...
@@ 223,22 +223,110 @@ Tactic failure: iFrame: cannot frame Q.
={E1,E2}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
={E1,E2}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
"iAlways_spatial_non_empty"
: string
The command has indeed failed with message:
In nested Ltac calls to "iAlways", "iModIntro" and
"iModIntro (uconstr)", last call failed.
Tactic failure: iModIntro: spatial context is nonempty.
"iDestruct_bad_name"
: string
The command has indeed failed with message:
In nested Ltac calls to "iDestruct (open_constr) as (constr)",
"iDestructCore (open_constr) as (constr) (tactic)" and
"iDestructCore (open_constr) as (constr) (tactic)", last call failed.
Tactic failure: iDestruct: (INamed "HQ") not found.
Tactic failure: iDestruct: "HQ" not found.
"iIntros_dup_name"
: string
The command has indeed failed with message:
In nested Ltac calls to "iIntros (constr)", "iIntros_go" and
"iIntro (constr)", last call failed.
Tactic failure: iIntro: "HP" not fresh.
The command has indeed failed with message:
In nested Ltac calls to "iIntros ( (intropattern) )",
"iIntro ( (intropattern) )" and "intros x", last call failed.
x is already used.
"iSplit_one_of_many"
: string
The command has indeed failed with message:
Ltac call to "iSplitL (constr)" failed.
Tactic failure: iSplitL: hypotheses ["HPx"] not found.
The command has indeed failed with message:
Ltac call to "iSplitL (constr)" failed.
Tactic failure: iSplitL: hypotheses ["HPx"] not found.
"iExact_fail"
: string
The command has indeed failed with message:
Ltac call to "iExact (constr)" failed.
Tactic failure: iExact: "HQ" not found.
The command has indeed failed with message:
Ltac call to "iExact (constr)" failed.
Tactic failure: iExact: "HQ" : Q does not match goal.
The command has indeed failed with message:
Ltac call to "iExact (constr)" failed.
Tactic failure: iExact: "HP"
not absorbing and the remaining hypotheses not affine.
"iClear_fail"
: string
The command has indeed failed with message:
In nested Ltac calls to "iClear (constr)", "iElaborateSelPat" and
"<iris.proofmode.ltac_tactics.iElaborateSelPat_go>", last call failed.
Tactic failure: iElaborateSelPat: "HP" not found.
The command has indeed failed with message:
In nested Ltac calls to "iClear (constr)",
"<iris.proofmode.ltac_tactics.iClear_go>" and
"<iris.proofmode.ltac_tactics.iClearHyp>", last call failed.
Tactic failure: iClear: "HP" : P not affine and the goal not absorbing.
"iSpecializeArgs_fail"
: string
The command has indeed failed with message:
In nested Ltac calls to "iSpecialize (open_constr)",
"iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
"iSpecializeArgs (constr) (open_constr)",
"<iris.proofmode.ltac_tactics.iSpecializeArgs_go>" and
"notypeclasses refine (uconstr)", last call failed.
In environment
PROP : sbi
P : PROP
The term "true" has type "bool" while it is expected to have type "nat".
"iStartProof_fail"
: string
The command has indeed failed with message:
In nested Ltac calls to "iStartProof" and "iStartProof", last call failed.
Tactic failure: iStartProof: not a BI assertion.
"iPoseProof_fail"
: string
The command has indeed failed with message:
In nested Ltac calls to "iPoseProof (open_constr) as (constr)" and
"iPoseProofCore (open_constr) as (constr) (constr) (tactic)", 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)" and
"iPoseProofCore (open_constr) as (constr) (constr) (tactic)", last call
failed.
Tactic failure: iRename: "H" not fresh.
"iRevert_fail"
: string
The command has indeed failed with message:
In nested Ltac calls to "iRevert (constr)", "iElaborateSelPat" and
"<iris.proofmode.ltac_tactics.iElaborateSelPat_go>", last call failed.
Tactic failure: iElaborateSelPat: "H" not found.
"iDestruct_fail"
: string
The command has indeed failed with message:
In nested Ltac calls to "iDestruct (open_constr) as (constr)",
"iDestructCore (open_constr) as (constr) (tactic)",
"iDestructCore (open_constr) as (constr) (tactic)" and
"iDestructCore (open_constr) as (constr) (tactic)", last call failed.
Tactic failure: iDestruct: "{HP}"
should contain exactly one proper introduction pattern.
The command has indeed failed with message:
In nested Ltac calls to "iDestruct (open_constr) as (constr)",
"iDestructCore (open_constr) as (constr) (tactic)",
"iDestructCore (open_constr) as (constr) (tactic)" and
"iDestructCore (open_constr) as (constr) (tactic)", last call failed.
Tactic failure: iDestruct: (IList [[IClear (sel_patterns.SelIdent "HP")]])
invalid.
tests/proofmode.v
View file @
1471ae26
...
...
@@ 576,22 +576,64 @@ Section error_tests.
Context
{
PROP
:
sbi
}.
Implicit
Types
P
Q
R
:
PROP
.
Check
"iAlways_spatial_non_empty"
.
Lemma
iAlways_spatial_non_empty
P
:
P

∗
□
emp
.
Proof
.
iIntros
"HP"
.
Fail
iAlways
.
Abort
.
Check
"iDestruct_bad_name"
.
Lemma
iDestruct_bad_name
P
:
P

∗
P
.
Proof
.
iIntros
"HP"
.
Fail
iDestruct
"HQ"
as
"HP"
.
Abort
.
Lemma
iIntros_dup_name
P
:
P

∗
∀
x
y
:
(),
P
.
Proof
.
iIntros
"HP"
(
x
).
Fail
iIntros
(
x
).
Abort
.
Check
"iIntros_dup_name"
.
Lemma
iIntros_dup_name
P
Q
:
P

∗
Q

∗
∀
x
y
:
(),
P
.
Proof
.
iIntros
"HP"
.
Fail
iIntros
"HP"
.
iIntros
"HQ"
(
x
).
Fail
iIntros
(
x
).
Abort
.
Check
"iSplit_one_of_many"
.
Lemma
iSplit_one_of_many
P
:
P

∗
P

∗
P
∗
P
.
Proof
.
iIntros
"HP1 HP2"
.
Fail
iSplitL
"HP1 HPx"
.
Fail
iSplitL
"HPx HP1"
.
Abort
.
Check
"iExact_fail"
.
Lemma
iExact_fail
P
Q
:
<
affine
>
P

∗
Q

∗
<
affine
>
P
.
Proof
.
iIntros
"HP"
.
Fail
iExact
"HQ"
.
iIntros
"HQ"
.
Fail
iExact
"HQ"
.
Fail
iExact
"HP"
.
Abort
.
Check
"iClear_fail"
.
Lemma
iClear_fail
P
:
P

∗
P
.
Proof
.
Fail
iClear
"HP"
.
iIntros
"HP"
.
Fail
iClear
"HP"
.
Abort
.
Check
"iSpecializeArgs_fail"
.
Lemma
iSpecializeArgs_fail
P
:
(
∀
x
:
nat
,
P
)

∗
P
.
Proof
.
iIntros
"HP"
.
Fail
iSpecialize
(
"HP"
$!
true
).
Abort
.
Check
"iStartProof_fail"
.
Lemma
iStartProof_fail
:
0
=
0
.
Proof
.
Fail
iStartProof
.
Abort
.
Check
"iPoseProof_fail"
.
Lemma
iPoseProof_fail
P
:
P

∗
P
.
Proof
.
Fail
iPoseProof
(
eq_refl
0
)
as
"H"
.
iIntros
"H"
.
Fail
iPoseProof
bi
.
and_intro
as
"H"
.
Abort
.
Check
"iRevert_fail"
.
Lemma
iRevert_fail
P
:
P

∗
P
.
Proof
.
Fail
iRevert
"H"
.
Abort
.
Check
"iDestruct_fail"
.
Lemma
iDestruct_fail
P
:
P

∗
<
absorb
>
P
.
Proof
.
iIntros
"HP"
.
Fail
iDestruct
"HP"
as
"{HP}"
.
Fail
iDestruct
"HP"
as
"[{HP}]"
.
Abort
.
End
error_tests
.
theories/proofmode/ltac_tactics.v
View file @
1471ae26
...
...
@@ 30,6 +30,13 @@ and iInv. *)
Ltac
iSolveSideCondition
:
=
split_and
?
;
try
solve
[
fast_done

solve_ndisj
].
(** Used for printing [string]s and [ident]s. *)
Ltac
pretty_ident
H
:
=
lazymatch
H
with

INamed
?H
=>
H

?H
=>
H
end
.
(** * Misc *)
Ltac
iMissingHyps
Hs
:
=
...
...
@@ 55,7 +62,7 @@ Tactic Notation "iStartProof" :=
lazymatch
goal
with


envs_entails
_
_
=>
idtac


?
φ
=>
notypeclasses
refine
(
as_emp_valid_2
φ
_
_
)
;
[
iSolveTC

fail
"iStartProof: not a B
i entailment
"
[
iSolveTC

fail
"iStartProof: not a B
I assertion
"

apply
tac_adequate
]
end
.
...
...
@@ 76,7 +83,7 @@ Tactic Notation "iStartProof" uconstr(PROP) :=
[bi_car _], and hence trigger the canonical structures mechanism
to find the corresponding bi. *)


?
φ
=>
notypeclasses
refine
((
λ
P
:
PROP
,
@
as_emp_valid_2
φ
_
P
)
_
_
_
)
;
[
iSolveTC

fail
"iStartProof: not a B
i entailment
"
[
iSolveTC

fail
"iStartProof: not a B
I assertion
"

apply
tac_adequate
]
end
.
...
...
@@ 126,14 +133,18 @@ possible in Ltac2. *)
(** * Context manipulation *)
Tactic
Notation
"iRename"
constr
(
H1
)
"into"
constr
(
H2
)
:
=
eapply
tac_rename
with
_
H1
H2
_
_;
(* (i:=H1) (j:=H2) *)
[
pm_reflexivity

fail
"iRename:"
H1
"not found"

pm_reflexivity

fail
"iRename:"
H2
"not fresh"
].
[
pm_reflexivity

let
H1
:
=
pretty_ident
H1
in
fail
"iRename:"
H1
"not found"

pm_reflexivity

let
H2
:
=
pretty_ident
H2
in
fail
"iRename:"
H2
"not fresh"
].
Local
Inductive
esel_pat
:
=

ESelPure

ESelIdent
:
bool
→
ident
→
esel_pat
.
Ltac
iElaborateSelPat_go
pat
Δ
Hs
:
=
Local
Ltac
iElaborateSelPat_go
pat
Δ
Hs
:
=
lazymatch
pat
with

[]
=>
eval
cbv
in
Hs

SelPure
::
?pat
=>
iElaborateSelPat_go
pat
Δ
(
ESelPure
::
Hs
)
...
...
@@ 148,7 +159,9 @@ Ltac iElaborateSelPat_go pat Δ Hs :=

SelIdent
?H
::
?pat
=>
lazymatch
pm_eval
(
envs_lookup_delete
false
H
Δ
)
with

Some
(
?p
,
_
,?
Δ
'
)
=>
iElaborateSelPat_go
pat
Δ
'
(
ESelIdent
p
H
::
Hs
)

None
=>
fail
"iElaborateSelPat:"
H
"not found"

None
=>
let
H
:
=
pretty_ident
H
in
fail
"iElaborateSelPat:"
H
"not found"
end
end
.
Ltac
iElaborateSelPat
pat
:
=
...
...
@@ 159,20 +172,23 @@ Ltac iElaborateSelPat pat :=
Local
Ltac
iClearHyp
H
:
=
eapply
tac_clear
with
_
H
_
_;
(* (i:=H) *)
[
pm_reflexivity

fail
"iClear:"
H
"not found"
[
pm_reflexivity

let
H
:
=
pretty_ident
H
in
fail
"iClear:"
H
"not found"

pm_reduce
;
iSolveTC

let
H
:
=
pretty_ident
H
in
let
P
:
=
match
goal
with

TCOr
(
Affine
?P
)
_
=>
P
end
in
fail
"iClear:"
H
":"
P
"not affine and the goal not absorbing"
].
Local
Ltac
iClear_go
Hs
:
=
lazymatch
Hs
with

[]
=>
idtac

ESelPure
::
?Hs
=>
clear
;
iClear_go
Hs

ESelIdent
_
?H
::
?Hs
=>
iClearHyp
H
;
iClear_go
Hs
end
.
Tactic
Notation
"iClear"
constr
(
Hs
)
:
=
let
rec
go
Hs
:
=
lazymatch
Hs
with

[]
=>
idtac

ESelPure
::
?Hs
=>
clear
;
go
Hs

ESelIdent
_
?H
::
?Hs
=>
iClearHyp
H
;
go
Hs
end
in
let
Hs
:
=
iElaborateSelPat
Hs
in
iStartProof
;
go
Hs
.
iStartProof
;
let
Hs
:
=
iElaborateSelPat
Hs
in
iClear_go
Hs
.
Tactic
Notation
"iClear"
"("
ident_list
(
xs
)
")"
constr
(
Hs
)
:
=
iClear
Hs
;
clear
xs
.
...
...
@@ 180,11 +196,15 @@ Tactic Notation "iClear" "(" ident_list(xs) ")" constr(Hs) :=
(** * Assumptions *)
Tactic
Notation
"iExact"
constr
(
H
)
:
=
eapply
tac_assumption
with
_
H
_
_;
(* (i:=H) *)
[
pm_reflexivity

fail
"iExact:"
H
"not found"
[
pm_reflexivity

let
H
:
=
pretty_ident
H
in
fail
"iExact:"
H
"not found"

iSolveTC

let
H
:
=
pretty_ident
H
in
let
P
:
=
match
goal
with

FromAssumption
_
?P
_
=>
P
end
in
fail
"iExact:"
H
":"
P
"does not match goal"

pm_reduce
;
iSolveTC

let
H
:
=
pretty_ident
H
in
fail
"iExact:"
H
"not absorbing and the remaining hypotheses not affine"
].
Tactic
Notation
"iAssumptionCore"
:
=
...
...
@@ 232,7 +252,9 @@ Tactic Notation "iExFalso" := apply tac_ex_falso.
(** * Making hypotheses persistent or pure *)
Local
Tactic
Notation
"iPersistent"
constr
(
H
)
:
=
eapply
tac_persistent
with
_
H
_
_
_;
(* (i:=H) *)
[
pm_reflexivity

fail
"iPersistent:"
H
"not found"
[
pm_reflexivity

let
H
:
=
pretty_ident
H
in
fail
"iPersistent:"
H
"not found"

iSolveTC

let
P
:
=
match
goal
with

IntoPersistent
_
?P
_
=>
P
end
in
fail
"iPersistent:"
P
"not persistent"
...
...
@@ 243,7 +265,9 @@ Local Tactic Notation "iPersistent" constr(H) :=
Local
Tactic
Notation
"iPure"
constr
(
H
)
"as"
simple_intropattern
(
pat
)
:
=
eapply
tac_pure
with
_
H
_
_
_;
(* (i:=H1) *)
[
pm_reflexivity

fail
"iPure:"
H
"not found"
[
pm_reflexivity

let
H
:
=
pretty_ident
H
in
fail
"iPure:"
H
"not found"

iSolveTC

let
P
:
=
match
goal
with

IntoPure
?P
_
=>
P
end
in
fail
"iPure:"
P
"not pure"
...
...
@@ 285,7 +309,9 @@ Local Ltac iFramePure t :=
Local
Ltac
iFrameHyp
H
:
=
iStartProof
;
eapply
tac_frame
with
_
H
_
_
_;
[
pm_reflexivity

fail
"iFrame:"
H
"not found"
[
pm_reflexivity

let
H
:
=
pretty_ident
H
in
fail
"iFrame:"
H
"not found"

iSolveTC

let
R
:
=
match
goal
with

Frame
_
?R
_
_
=>
R
end
in
fail
"iFrame: cannot frame"
R
...
...
@@ 395,13 +421,17 @@ Local Tactic Notation "iIntro" constr(H) :=
let
P
:
=
lazymatch
goal
with

Persistent
?P
=>
P
end
in
fail
1
"iIntro: introducing nonpersistent"
H
":"
P
"into nonempty spatial context"

pm_reflexivity

fail
1
"iIntro:"
H
"not fresh"

pm_reflexivity

let
H
:
=
pretty_ident
H
in
fail
1
"iIntro:"
H
"not fresh"

iSolveTC
]

(* (_ ∗ _) *)
eapply
tac_wand_intro
with
_
H
_
_;
(* (i:=H) *)
[
iSolveTC

pm_reflexivity

fail
1
"iIntro:"
H
"not fresh"

pm_reflexivity

let
H
:
=
pretty_ident
H
in
fail
1
"iIntro:"
H
"not fresh"
]

fail
"iIntro: nothing to introduce"
].
...
...
@@ 414,7 +444,9 @@ Local Tactic Notation "iIntro" "#" constr(H) :=

iSolveTC

let
P
:
=
match
goal
with

IntoPersistent
_
?P
_
=>
P
end
in
fail
1
"iIntro:"
P
"not persistent"

pm_reflexivity

fail
1
"iIntro:"
H
"not fresh"

pm_reflexivity

let
H
:
=
pretty_ident
H
in
fail
1
"iIntro:"
H
"not fresh"
]

(* (?P ∗ _) *)
eapply
tac_wand_intro_persistent
with
_
H
_
_
_;
(* (i:=H) *)
...
...
@@ 425,7 +457,9 @@ Local Tactic Notation "iIntro" "#" constr(H) :=

iSolveTC

let
P
:
=
match
goal
with

TCOr
(
Affine
?P
)
_
=>
P
end
in
fail
1
"iIntro:"
P
"not affine and the goal not absorbing"

pm_reflexivity

fail
1
"iIntro:"
H
"not fresh"

pm_reflexivity

let
H
:
=
pretty_ident
H
in
fail
1
"iIntro:"
H
"not fresh"
]

fail
"iIntro: nothing to introduce"
].
...
...
@@ 482,22 +516,24 @@ type classes in the arguments `xs` are resolved at arbitrary moments. Tactics
like `apply`, `split` and `eexists` wrongly trigger type class search to resolve
these holes. To avoid TC being triggered too eagerly, this tactic uses `refine`
at most places instead of `apply`. *)
Local
Tactic
Notation
"iSpecializeArgs"
constr
(
H
)
open_constr
(
xs
)
:
=
let
rec
go
xs
:
=
Local
Ltac
iSpecializeArgs_go
H
xs
:
=
lazymatch
xs
with

hnil
=>
idtac

hcons
?x
?xs
=>
notypeclasses
refine
(
tac_forall_specialize
_
_
H
_
_
_
_
_
_
_
)
;
[
pm_reflexivity

fail
"iSpecialize:"
H
"not found"
[
pm_reflexivity

let
H
:
=
pretty_ident
H
in
fail
"iSpecialize:"
H
"not found"

iSolveTC

let
P
:
=
match
goal
with

IntoForall
?P
_
=>
P
end
in
fail
"iSpecialize: cannot instantiate"
P
"with"
x

lazymatch
goal
with
(* Force [A] in [ex_intro] to deal with coercions. *)


∃
_
:
?A
,
_
=>
notypeclasses
refine
(@
ex_intro
A
_
x
(
conj
_
_
))
end
;
[
shelve
..
pm_reflexivity

go
xs
]]
end
in
go
xs
.
end
;
[
shelve
..
pm_reflexivity

iSpecializeArgs_go
H
xs
]]
end
.
Local
Tactic
Notation
"iSpecializeArgs"
constr
(
H
)
open_constr
(
xs
)
:
=
iSpecializeArgs_go
H
xs
.
Ltac
iSpecializePat_go
H1
pats
:
=
let
solve_to_wand
H1
:
=
...
...
@@ 519,8 +555,12 @@ Ltac iSpecializePat_go H1 pats :=
iSpecializePat_go
H1
pats

SIdent
?H2
::
?pats
=>
notypeclasses
refine
(
tac_specialize
_
_
_
H2
_
H1
_
_
_
_
_
_
_
_
_
_
)
;
[
pm_reflexivity

fail
"iSpecialize:"
H2
"not found"

pm_reflexivity

fail
"iSpecialize:"
H1
"not found"
[
pm_reflexivity

let
H2
:
=
pretty_ident
H2
in
fail
"iSpecialize:"
H2
"not found"

pm_reflexivity

let
H1
:
=
pretty_ident
H1
in
fail
"iSpecialize:"
H1
"not found"

iSolveTC

let
P
:
=
match
goal
with

IntoWand
_
_
?P
?Q
_
=>
P
end
in
let
Q
:
=
match
goal
with

IntoWand
_
_
?P
?Q
_
=>
Q
end
in
...
...
@@ 528,7 +568,9 @@ Ltac iSpecializePat_go H1 pats :=

pm_reflexivity

iSpecializePat_go
H1
pats
]

SPureGoal
?d
::
?pats
=>
notypeclasses
refine
(
tac_specialize_assert_pure
_
_
H1
_
_
_
_
_
_
_
_
_
_
_
_
)
;
[
pm_reflexivity

fail
"iSpecialize:"
H1
"not found"
[
pm_reflexivity

let
H1
:
=
pretty_ident
H1
in
fail
"iSpecialize:"
H1
"not found"

solve_to_wand
H1

iSolveTC

let
Q
:
=
match
goal
with

FromPure
_
?Q
_
=>
Q
end
in
...
...
@@ 538,7 +580,9 @@ Ltac iSpecializePat_go H1 pats :=

iSpecializePat_go
H1
pats
]

SGoal
(
SpecGoal
GPersistent
false
?Hs_frame
[]
?d
)
::
?pats
=>
notypeclasses
refine
(
tac_specialize_assert_persistent
_
_
_
H1
_
_
_
_
_
_
_
_
_
_
_
_
_
)
;
[
pm_reflexivity

fail
"iSpecialize:"
H1
"not found"
[
pm_reflexivity

let
H1
:
=
pretty_ident
H1
in
fail
"iSpecialize:"
H1
"not found"

solve_to_wand
H1

iSolveTC

let
Q
:
=
match
goal
with

Persistent
?Q
=>
Q
end
in
...
...
@@ 552,7 +596,9 @@ Ltac iSpecializePat_go H1 pats :=

SGoal
(
SpecGoal
?m
?lr
?Hs_frame
?Hs
?d
)
::
?pats
=>
let
Hs'
:
=
eval
cbv
in
(
if
lr
then
Hs
else
Hs_frame
++
Hs
)
in
notypeclasses
refine
(
tac_specialize_assert
_
_
_
_
H1
_
lr
Hs'
_
_
_
_
_
_
_
_
_
_
_
)
;
[
pm_reflexivity

fail
"iSpecialize:"
H1
"not found"
[
pm_reflexivity

let
H1
:
=
pretty_ident
H1
in
fail
"iSpecialize:"
H1
"not found"

solve_to_wand
H1

lazymatch
m
with

GSpatial
=>
notypeclasses
refine
(
add_modal_id
_
_
)
...
...
@@ 565,7 +611,9 @@ Ltac iSpecializePat_go H1 pats :=

iSpecializePat_go
H1
pats
]

SAutoFrame
GPersistent
::
?pats
=>
notypeclasses
refine
(
tac_specialize_assert_persistent
_
_
_
H1
_
_
_
_
_
_
_
_
_
_
_
_
_
)
;
[
pm_reflexivity

fail
"iSpecialize:"
H1
"not found"
[
pm_reflexivity

let
H1
:
=
pretty_ident
H1
in
fail
"iSpecialize:"
H1
"not found"

solve_to_wand
H1

iSolveTC

let
Q
:
=
match
goal
with

Persistent
?Q
=>
Q
end
in
...
...
@@ 575,7 +623,9 @@ Ltac iSpecializePat_go H1 pats :=

iSpecializePat_go
H1
pats
]

SAutoFrame
?m
::
?pats
=>
notypeclasses
refine
(
tac_specialize_frame
_
_
H1
_
_
_
_
_
_
_
_
_
_
_
_
)
;
[
pm_reflexivity

fail
"iSpecialize:"
H1
"not found"
[
pm_reflexivity

let
H1
:
=
pretty_ident
H1
in
fail
"iSpecialize:"
H1
"not found"

solve_to_wand
H1

lazymatch
m
with

GSpatial
=>
notypeclasses
refine
(
add_modal_id
_
_
)
...
...
@@ 625,7 +675,9 @@ Tactic Notation "iSpecializeCore" open_constr(H)

true
=>
(* FIXME: do something reasonable when the BI is not affine *)
notypeclasses
refine
(
tac_specialize_persistent_helper
_
_
H
_
_
_
_
_
_
_
_
_
_
_
)
;
[
pm_reflexivity

fail
"iSpecialize:"
H
"not found"
[
pm_reflexivity

let
H
:
=
pretty_ident
H
in
fail
"iSpecialize:"
H
"not found"

iSpecializePat
H
pat
;
[..

refine
(
tac_specialize_persistent_helper_done
_
H
_
_
_
)
;
...
...
@@ 693,7 +745,7 @@ Tactic Notation "iIntoEmpValid" open_constr(t) :=

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
"iPoseProof: not a BI assertion"
[
iSolveTC

fail
1
"iPoseProof: not a BI assertion"

exact
t
]]
with
go_specialize
t
tT
:
=
lazymatch
tT
with
(* We do not use hnf of tT, because, if
...
...
@@ 732,13 +784,19 @@ Tactic Notation "iPoseProofCore" open_constr(lem)
lazymatch
type
of
t
with

ident
=>
eapply
tac_pose_proof_hyp
with
_
_
t
_
Htmp
_;
[
pm_reflexivity

fail
"iPoseProof:"
t
"not found"

pm_reflexivity

fail
"iPoseProof:"
Htmp
"not fresh"
[
pm_reflexivity

let
t
:
=
pretty_ident
t
in
fail
"iPoseProof:"
t
"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

pm_reflexivity

fail
"iPoseProof:"
Htmp
"not fresh"

pm_reflexivity

let
Htmp
:
=
pretty_ident
Htmp
in
fail
"iPoseProof:"
Htmp
"not fresh"

goal_tac
()]
end
;
try
iSolveTC
in
...
...
@@ 788,10 +846,12 @@ Tactic Notation "iRevert" constr(Hs) :=
go
Hs

ESelIdent
_
?H
::
?Hs
=>
eapply
tac_revert
with
_
H
_
_;
(* (i:=H2) *)
[
pm_reflexivity

fail
"iRevert:"
H
"not found"
[
pm_reflexivity

let
H
:
=
pretty_ident
H
in
fail
"iRevert:"
H
"not found"

pm_reduce
;
go
Hs
]
end
in
let
Hs
:
=
iElaborateSelPat
Hs
in
iStartProof
;
go
Hs
.
iStartProof
;
let
Hs
:
=
iElaborateSelPat
Hs
in
go
Hs
.
Tactic
Notation
"iRevert"
"("
ident
(
x1
)
")"
:
=
iForallRevert
x1
.
...
...
@@ 854,12 +914,18 @@ Tactic Notation "iRight" :=
Local
Tactic
Notation
"iOrDestruct"
constr
(
H
)
"as"
constr
(
H1
)
constr
(
H2
)
:
=
eapply
tac_or_destruct
with
_
_
H
_
H1
H2
_
_
_;
(* (i:=H) (j1:=H1) (j2:=H2) *)
[
pm_reflexivity

fail
"iOrDestruct:"
H
"not found"
[
pm_reflexivity

let
H
:
=
pretty_ident
H
in
fail
"iOrDestruct:"
H
"not found"

iSolveTC

let
P
:
=
match
goal
with

IntoOr
?P
_
_
=>
P
end
in
fail
"iOrDestruct: cannot destruct"
P

pm_reflexivity

fail
"iOrDestruct:"
H1
"not fresh"

pm_reflexivity

fail
"iOrDestruct:"
H2
"not fresh"

pm_reflexivity

let
H1
:
=
pretty_ident
H1
in
fail
"iOrDestruct:"
H1
"not fresh"

pm_reflexivity

let
H2
:
=
pretty_ident
H2
in
fail
"iOrDestruct:"
H2
"not fresh"

].
(** * Conjunction and separating conjunction *)
...
...
@@ 901,7 +967,9 @@ 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) *)
[
pm_reflexivity

fail
"iAndDestruct:"
H
"not found"
[
pm_reflexivity

let
H
:
=
pretty_ident
H
in
fail
"iAndDestruct:"
H
"not found"

pm_reduce
;
iSolveTC

let
P
:
=
lazymatch
goal
with
...
...
@@ 909,7 +977,10 @@ Local Tactic Notation "iAndDestruct" constr(H) "as" constr(H1) constr(H2) :=


IntoAnd
_
?P
_
_
=>
P
end
in
fail
"iAndDestruct: cannot destruct"
P

pm_reflexivity

fail
"iAndDestruct:"
H1
"or"
H2
" not fresh"
].

pm_reflexivity

let
H1
:
=
pretty_ident
H1
in
let
H2
:
=
pretty_ident
H2
in
fail
"iAndDestruct:"
H1
"or"
H2
" not fresh"
].
Local
Tactic
Notation
"iAndDestructChoice"
constr
(
H
)
"as"
constr
(
d
)
constr
(
H'
)
:
=
eapply
tac_and_destruct_choice
with
_
H
_
d
H'
_
_
_;
...
...
@@ 917,7 +988,9 @@ Local Tactic Notation "iAndDestructChoice" constr(H) "as" constr(d) constr(H') :

pm_reduce
;
iSolveTC

let
P
:
=
match
goal
with

TCOr
(
IntoAnd
_
?P
_
_
)
_
=>
P
end
in
fail
"iAndDestructChoice: cannot destruct"
P

pm_reflexivity

fail
"iAndDestructChoice:"
H'
" not fresh"
].

pm_reflexivity

let
H'
:
=
pretty_ident
H'
in
fail
"iAndDestructChoice:"
H'
" not fresh"
].