Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Rice Wine
Iris
Commits
49f26fdc
Commit
49f26fdc
authored
Jun 15, 2018
by
Ralf Jung
Browse files
test and fix some more proof mode error messages
parent
db57a33e
Changes
3
Hide whitespace changes
Inline
Side-by-side
tests/proofmode.ref
View file @
49f26fdc
...
...
@@ -184,15 +184,21 @@ 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 non-empty.
"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: "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.
...
...
@@ -201,12 +207,87 @@ 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 @
49f26fdc
...
...
@@ -553,14 +553,17 @@ 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
.
Check
"iIntros_dup_name"
.
Lemma
iIntros_dup_name
P
Q
:
P
-
∗
Q
-
∗
∀
x
y
:
(),
P
.
Proof
.
...
...
@@ -568,16 +571,46 @@ Proof.
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
.
Lemma
iExact_not_found
P
:
P
-
∗
P
.
Check
"iExact_fail"
.
Lemma
iExact_fail
P
Q
:
<
affine
>
P
-
∗
Q
-
∗
<
affine
>
P
.
Proof
.
iIntros
"HP"
.
Fail
iExact
"HQ"
.
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 @
49f26fdc
...
...
@@ -62,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
.
...
...
@@ -83,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
.
...
...
@@ -133,8 +133,12 @@ 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
...
...
@@ -172,18 +176,19 @@ Local Ltac iClearHyp H :=
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
.
...
...
@@ -192,11 +197,14 @@ Tactic Notation "iClear" "(" ident_list(xs) ")" constr(Hs) :=
Tactic
Notation
"iExact"
constr
(
H
)
:
=
eapply
tac_assumption
with
_
H
_
_;
(* (i:=H) *)
[
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"
:
=
...
...
@@ -508,8 +516,7 @@ 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
=>
...
...
@@ -523,9 +530,10 @@ Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
|
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
:
=
...
...
@@ -737,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
...
...
@@ -843,7 +851,7 @@ Tactic Notation "iRevert" constr(Hs) :=
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
.
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment