Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Rice Wine
Iris
Commits
e3fb7049
Commit
e3fb7049
authored
Mar 16, 2017
by
Robbert Krebbers
Browse files
Fix issue #80: better error message when hyps are missing.
parent
e78dfb5f
Changes
1
Hide whitespace changes
Inline
Sidebyside
theories/proofmode/tactics.v
View file @
e3fb7049
...
@@ 32,6 +32,15 @@ Ltac iFresh' H :=
...
@@ 32,6 +32,15 @@ Ltac iFresh' H :=
end
.
end
.
Ltac
iFresh
:
=
iFresh'
"~"
.
Ltac
iFresh
:
=
iFresh'
"~"
.
Ltac
iMissingHyps
Hs
:
=
let
Δ
:
=
lazymatch
goal
with


of_envs
?
Δ
⊢
_
=>
Δ


context
[
envs_split
_
_
?
Δ
]
=>
Δ
end
in
let
Hhyps
:
=
eval
env_cbv
in
(
envs_dom
Δ
)
in
eval
vm_compute
in
(
list_difference
Hs
Hhyps
).
Tactic
Notation
"iTypeOf"
constr
(
H
)
tactic
(
tac
)
:
=
Tactic
Notation
"iTypeOf"
constr
(
H
)
tactic
(
tac
)
:
=
let
Δ
:
=
match
goal
with

of_envs
?
Δ
⊢
_
=>
Δ
end
in
let
Δ
:
=
match
goal
with

of_envs
?
Δ
⊢
_
=>
Δ
end
in
lazymatch
eval
env_cbv
in
(
envs_lookup
H
Δ
)
with
lazymatch
eval
env_cbv
in
(
envs_lookup
H
Δ
)
with
...
@@ 238,7 +247,7 @@ Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
...
@@ 238,7 +247,7 @@ Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
Tactic
Notation
"iFrame"
constr
(
Hs
)
:
=
Tactic
Notation
"iFrame"
constr
(
Hs
)
:
=
let
rec
go
Hs
:
=
let
rec
go
Hs
:
=
match
Hs
with
lazy
match
Hs
with

[]
=>
idtac

[]
=>
idtac

SelPure
::
?Hs
=>
iFrameAnyPure
;
go
Hs

SelPure
::
?Hs
=>
iFrameAnyPure
;
go
Hs

SelPersistent
::
?Hs
=>
iFrameAnyPersistent
;
go
Hs

SelPersistent
::
?Hs
=>
iFrameAnyPersistent
;
go
Hs
...
@@ 357,7 +366,7 @@ Notation "( H 'with' pat )" := (ITrm H hnil pat) (at level 0).
...
@@ 357,7 +366,7 @@ Notation "( H 'with' pat )" := (ITrm H hnil pat) (at level 0).
Local
Tactic
Notation
"iSpecializeArgs"
constr
(
H
)
open_constr
(
xs
)
:
=
Local
Tactic
Notation
"iSpecializeArgs"
constr
(
H
)
open_constr
(
xs
)
:
=
let
rec
go
xs
:
=
let
rec
go
xs
:
=
match
xs
with
lazy
match
xs
with

hnil
=>
idtac

hnil
=>
idtac

hcons
?x
?xs
=>

hcons
?x
?xs
=>
eapply
tac_forall_specialize
with
_
H
_
_
_;
(* (i:=H) (a:=x) *)
eapply
tac_forall_specialize
with
_
H
_
_
_;
(* (i:=H) (a:=x) *)
...
@@ 420,7 +429,9 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
...
@@ 420,7 +429,9 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=

GSpatial
=>
apply
elim_modal_dummy

GSpatial
=>
apply
elim_modal_dummy

GModal
=>
apply
_

fail
"iSpecialize: goal not a modality"

GModal
=>
apply
_

fail
"iSpecialize: goal not a modality"
end
end

env_reflexivity

fail
"iSpecialize:"
Hs
"not found"

env_reflexivity

let
Hs'
:
=
iMissingHyps
Hs'
in
fail
"iSpecialize: hypotheses"
Hs'
"not found in the context"

iFrame
Hs_frame
;
done_if
d
(*goal*)

iFrame
Hs_frame
;
done_if
d
(*goal*)

go
H1
pats
]

go
H1
pats
]

SAutoFrame
GPersistent
::
?pats
=>

SAutoFrame
GPersistent
::
?pats
=>
...
@@ 674,8 +685,11 @@ Tactic Notation "iSplitL" constr(Hs) :=
...
@@ 674,8 +685,11 @@ Tactic Notation "iSplitL" constr(Hs) :=
[
apply
_

[
apply
_

let
P
:
=
match
goal
with

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

FromSep
?P
_
_
=>
P
end
in
fail
"iSplitL:"
P
"not a separating conjunction"
fail
"iSplitL:"
P
"not a separating conjunction"

env_reflexivity

fail
"iSplitL: hypotheses"
Hs

env_reflexivity

"not found in the context"

].
let
Hs
:
=
iMissingHyps
Hs
in
fail
"iSplitL: hypotheses"
Hs
"not found in the context"

].
Tactic
Notation
"iSplitR"
constr
(
Hs
)
:
=
Tactic
Notation
"iSplitR"
constr
(
Hs
)
:
=
iStartProof
;
iStartProof
;
let
Hs
:
=
words
Hs
in
let
Hs
:
=
words
Hs
in
...
@@ 683,8 +697,10 @@ Tactic Notation "iSplitR" constr(Hs) :=
...
@@ 683,8 +697,10 @@ Tactic Notation "iSplitR" constr(Hs) :=
[
apply
_

[
apply
_

let
P
:
=
match
goal
with

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

FromSep
?P
_
_
=>
P
end
in
fail
"iSplitR:"
P
"not a separating conjunction"
fail
"iSplitR:"
P
"not a separating conjunction"

env_reflexivity

fail
"iSplitR: hypotheses"
Hs

env_reflexivity

"not found in the context"

].
let
Hs
:
=
iMissingHyps
Hs
in
fail
"iSplitR: hypotheses"
Hs
"not found in the context"

].
Tactic
Notation
"iSplitL"
:
=
iSplitR
""
.
Tactic
Notation
"iSplitL"
:
=
iSplitR
""
.
Tactic
Notation
"iSplitR"
:
=
iSplitL
""
.
Tactic
Notation
"iSplitR"
:
=
iSplitL
""
.
...
@@ 709,7 +725,9 @@ Local Tactic Notation "iAndDestructChoice" constr(H) "as" constr(lr) constr(H')
...
@@ 709,7 +725,9 @@ Local Tactic Notation "iAndDestructChoice" constr(H) "as" constr(lr) constr(H')
Tactic
Notation
"iCombine"
constr
(
Hs
)
"as"
constr
(
H
)
:
=
Tactic
Notation
"iCombine"
constr
(
Hs
)
"as"
constr
(
H
)
:
=
let
Hs
:
=
words
Hs
in
let
Hs
:
=
words
Hs
in
eapply
tac_combine
with
_
_
Hs
_
_
H
_;
eapply
tac_combine
with
_
_
Hs
_
_
H
_;
[
env_reflexivity

fail
"iCombine:"
Hs
"not found"
[
env_reflexivity

let
Hs
:
=
iMissingHyps
Hs
in
fail
"iCombine: hypotheses"
Hs
"not found in the context"

apply
_

apply
_

env_reflexivity

fail
"iCombine:"
H
"not fresh"
].

env_reflexivity

fail
"iCombine:"
H
"not fresh"
].
...
@@ 1326,20 +1344,24 @@ Tactic Notation "iAssertCore" open_constr(Q)
...
@@ 1326,20 +1344,24 @@ Tactic Notation "iAssertCore" open_constr(Q)

[
SGoal
(
SpecGoal
?m
?lr
?Hs_frame
?Hs
?d
)]
=>

[
SGoal
(
SpecGoal
?m
?lr
?Hs_frame
?Hs
?d
)]
=>
let
Hs'
:
=
eval
cbv
in
(
if
lr
then
Hs
else
Hs_frame
++
Hs
)
in
let
Hs'
:
=
eval
cbv
in
(
if
lr
then
Hs
else
Hs_frame
++
Hs
)
in
let
p'
:
=
eval
cbv
in
(
match
m
with
GModal
=>
false

_
=>
p
end
)
in
let
p'
:
=
eval
cbv
in
(
match
m
with
GModal
=>
false

_
=>
p
end
)
in
match
p'
with
lazy
match
p'
with

false
=>

false
=>
eapply
tac_assert
with
_
_
_
lr
Hs'
H
Q
_;
eapply
tac_assert
with
_
_
_
lr
Hs'
H
Q
_;
[
lazymatch
m
with
[
lazymatch
m
with

GSpatial
=>
apply
elim_modal_dummy

GSpatial
=>
apply
elim_modal_dummy

GModal
=>
apply
_

fail
"iAssert: goal not a modality"

GModal
=>
apply
_

fail
"iAssert: goal not a modality"
end
end

env_reflexivity

fail
"iAssert:"
Hs
"not found"

env_reflexivity

let
Hs'
:
=
iMissingHyps
Hs'
in
fail
"iAssert: hypotheses"
Hs'
"not found in the context"

env_reflexivity

env_reflexivity

iFrame
Hs_frame
;
done_if
d
(*goal*)

iFrame
Hs_frame
;
done_if
d
(*goal*)

tac
H
]

tac
H
]

true
=>

true
=>
eapply
tac_assert_persistent
with
_
_
_
lr
Hs'
H
Q
;
eapply
tac_assert_persistent
with
_
_
_
lr
Hs'
H
Q
;
[
env_reflexivity
[
env_reflexivity

let
Hs'
:
=
iMissingHyps
Hs'
in
fail
"iAssert: hypotheses"
Hs'
"not found in the context"

env_reflexivity

env_reflexivity

apply
_

fail
"iAssert:"
Q
"not persistent"

apply
_

fail
"iAssert:"
Q
"not persistent"

done_if
d
(*goal*)

done_if
d
(*goal*)
...
@@ 1350,7 +1372,7 @@ Tactic Notation "iAssertCore" open_constr(Q)
...
@@ 1350,7 +1372,7 @@ Tactic Notation "iAssertCore" open_constr(Q)
Tactic
Notation
"iAssertCore"
open_constr
(
Q
)
"as"
constr
(
p
)
tactic
(
tac
)
:
=
Tactic
Notation
"iAssertCore"
open_constr
(
Q
)
"as"
constr
(
p
)
tactic
(
tac
)
:
=
let
p
:
=
intro_pat_persistent
p
in
let
p
:
=
intro_pat_persistent
p
in
match
p
with
lazy
match
p
with

true
=>
iAssertCore
Q
with
"[#]"
as
p
tac

true
=>
iAssertCore
Q
with
"[#]"
as
p
tac

false
=>
iAssertCore
Q
with
"[]"
as
p
tac

false
=>
iAssertCore
Q
with
"[]"
as
p
tac
end
.
end
.
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a 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