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
Iris
Iris
Commits
2471db29
Commit
2471db29
authored
Jun 18, 2019
by
Robbert Krebbers
Browse files
Merge branch 'dropdeadltacbranch' into 'master'
ltac_tactics.v: drop dead branch See merge request
!273
parents
17aec881
7b9d27ea
Pipeline
#17674
passed with stage
in 17 minutes and 14 seconds
Changes
3
Pipelines
1
Hide whitespace changes
Inline
Sidebyside
tests/proofmode.ref
View file @
2471db29
...
...
@@ 553,13 +553,13 @@ Tactic failure: iStartProof: not a BI assertion.
: string
The command has indeed failed with message:
In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
"iPoseProofCore (open_constr) as (constr)
(constr)
(tactic3)",
"iPoseProofCore (open_constr) as (constr) (tactic3)",
"iPoseProofCoreLem (constr) as (constr) before_tc (tactic3)" 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)
(tactic3)",
"iPoseProofCore (open_constr) as (constr) (tactic3)",
"iPoseProofCoreLem (constr) as (constr) before_tc (tactic3)",
"tac" (bound to spec_tac ltac:(()); [ ..  tac Htmp ]),
"tac" (bound to spec_tac ltac:(()); [ ..  tac Htmp ]),
...
...
@@ 573,14 +573,14 @@ Tactic failure: iRename: "H" not fresh.
: string
The command has indeed failed with message:
In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
"iPoseProofCore (open_constr) as (constr)
(constr)
(tactic3)" and
"iPoseProofCore (open_constr) as (constr) (tactic3)" and
"iPoseProofCoreHyp (constr) as (constr)", last call failed.
Tactic failure: iPoseProof: "Hx" not found.
"iPoseProof_not_found_fail2"
: string
The command has indeed failed with message:
In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
"iPoseProofCore (open_constr) as (constr)
(constr)
(tactic3)",
"iPoseProofCore (open_constr) as (constr) (tactic3)",
"iPoseProofCoreLem (constr) as (constr) before_tc (tactic3)",
"tac" (bound to spec_tac ltac:(()); [ ..  tac Htmp ]),
"tac" (bound to spec_tac ltac:(()); [ ..  tac Htmp ]),
...
...
@@ 648,7 +648,7 @@ Tactic failure: iOrDestruct: "H1" or "H'" not fresh.
: string
The command has indeed failed with message:
In nested Ltac calls to "iApply (open_constr)",
"iPoseProofCore (open_constr) as (constr)
(constr)
(tactic3)",
"iPoseProofCore (open_constr) as (constr) (tactic3)",
"tac" (bound to fun H => iApplyHyp H) and "iApplyHyp (constr)", last call
failed.
Tactic failure: iApply: cannot apply P.
...
...
@@ 656,7 +656,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)
(tactic3)",
"iPoseProofCore (open_constr) as (constr) (tactic3)",
"tac" (bound to fun H => iApplyHyp H) and "iApplyHyp (constr)", last call
failed.
Tactic failure: iApply: Q
...
...
@@ 665,7 +665,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)
(tactic3)",
"iPoseProofCore (open_constr) as (constr) (tactic3)",
"tac" (bound to fun H => iApplyHyp H) and "iApplyHyp (constr)", last call
failed.
Tactic failure: iApply: Q
...
...
theories/heap_lang/proofmode.v
View file @
2471db29
...
...
@@ 396,7 +396,7 @@ End heap.
happens *after* [tac H] got executed. *)
Tactic
Notation
"wp_apply_core"
open_constr
(
lem
)
tactic
(
tac
)
:
=
wp_pures
;
iPoseProofCore
lem
as
false
true
(
fun
H
=>
iPoseProofCore
lem
as
false
(
fun
H
=>
lazymatch
goal
with


envs_entails
_
(
wp
?s
?E
?e
?Q
)
=>
reshape_expr
e
ltac
:
(
fun
K
e'
=>
...
...
theories/proofmode/ltac_tactics.v
View file @
2471db29
...
...
@@ 992,30 +992,15 @@ Tactic Notation "iSpecialize" open_constr(t) :=
Tactic
Notation
"iSpecialize"
open_constr
(
t
)
"as"
"#"
:
=
iSpecializeCore
t
as
true
.
(** The tactic [iPoseProofCore lem as p
lazy_tc
tac] inserts the resource
(** The tactic [iPoseProofCore lem as p 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
the hypothesis containing [lem].
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 (if
[lazy_tc = true]) [tac H] is called.
Both variants of [lazy_tc] are used in other tactics that build on top of
[iPoseProofCore]:
 The tactic [iApply] uses lazy type class inference (i.e. [lazy_tc = true]),
so that evars can first be matched against the goal before being solved by
type class inference.
 The tactic [iDestruct] uses eager type class inference (i.e. [lazy_tc = false])
because it may be not possible to eliminate logical connectives before all
type class constraints have been resolved. *)
The argument [p] is like that of [iSpecialize]. It is a Boolean that denotes
whether the conclusion of the specialized term [lem] is persistent. *)
Tactic
Notation
"iPoseProofCore"
open_constr
(
lem
)
"as"
constr
(
p
)
constr
(
lazy_tc
)
tactic3
(
tac
)
:
=
"as"
constr
(
p
)
tactic3
(
tac
)
:
=
iStartProof
;
let
Htmp
:
=
iFresh
in
let
t
:
=
lazymatch
lem
with
ITrm
?t
?xs
?pat
=>
t

_
=>
lem
end
in
...
...
@@ 1027,13 +1012,7 @@ Tactic Notation "iPoseProofCore" open_constr(lem)
end
in
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

_
=>
iPoseProofCoreLem
t
as
Htmp
before_tc
(
spec_tac
()
;
[..
tac
Htmp
])
end
.
(** * The apply tactic *)
...
...
@@ 1084,7 +1063,7 @@ Tactic Notation "iApplyHyp" constr(H) :=
end
].
Tactic
Notation
"iApply"
open_constr
(
lem
)
:
=
iPoseProofCore
lem
as
false
true
(
fun
H
=>
iApplyHyp
H
).
iPoseProofCore
lem
as
false
(
fun
H
=>
iApplyHyp
H
).
(** * Disjunction *)
Tactic
Notation
"iLeft"
:
=
...
...
@@ 1743,7 +1722,7 @@ Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic3(tac) :=
(which cannot be kept). *)
iStartProof
;
lazymatch
ident
with

None
=>
iPoseProofCore
lem
as
p
false
tac

None
=>
iPoseProofCore
lem
as
p
tac

Some
?H
=>
lazymatch
iTypeOf
H
with

None
=>
...
...
@@ 1752,7 +1731,7 @@ Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic3(tac) :=

Some
(
true
,
?P
)
=>
(* intuitionistic hypothesis, check for a CopyDestruct instance *)
tryif
(
let
dummy
:
=
constr
:
(
_
:
CopyDestruct
P
)
in
idtac
)
then
(
iPoseProofCore
lem
as
p
false
tac
)
then
(
iPoseProofCore
lem
as
p
tac
)
else
(
iSpecializeCore
lem
as
p
;
[..
tac
H
])

Some
(
false
,
?P
)
=>
(* spatial hypothesis, cannot copy *)
...
...
@@ 1810,49 +1789,49 @@ Tactic Notation "iDestruct" open_constr(lem) "as" "%" simple_intropattern(pat) :
iDestructCore
lem
as
true
(
fun
H
=>
iPure
H
as
pat
).
Tactic
Notation
"iPoseProof"
open_constr
(
lem
)
"as"
constr
(
pat
)
:
=
iPoseProofCore
lem
as
pat
false
(
fun
H
=>
iDestructHyp
H
as
pat
).
iPoseProofCore
lem
as
pat
(
fun
H
=>
iDestructHyp
H
as
pat
).
Tactic
Notation
"iPoseProof"
open_constr
(
lem
)
"as"
"("
simple_intropattern
(
x1
)
")"
constr
(
pat
)
:
=
iPoseProofCore
lem
as
pat
false
(
fun
H
=>
iDestructHyp
H
as
(
x1
)
pat
).
iPoseProofCore
lem
as
pat
(
fun
H
=>
iDestructHyp
H
as
(
x1
)
pat
).
Tactic
Notation
"iPoseProof"
open_constr
(
lem
)
"as"
"("
simple_intropattern
(
x1
)
simple_intropattern
(
x2
)
")"
constr
(
pat
)
:
=
iPoseProofCore
lem
as
pat
false
(
fun
H
=>
iDestructHyp
H
as
(
x1
x2
)
pat
).
iPoseProofCore
lem
as
pat
(
fun
H
=>
iDestructHyp
H
as
(
x1
x2
)
pat
).
Tactic
Notation
"iPoseProof"
open_constr
(
lem
)
"as"
"("
simple_intropattern
(
x1
)
simple_intropattern
(
x2
)
simple_intropattern
(
x3
)
")"
constr
(
pat
)
:
=
iPoseProofCore
lem
as
pat
false
(
fun
H
=>
iDestructHyp
H
as
(
x1
x2
x3
)
pat
).
iPoseProofCore
lem
as
pat
(
fun
H
=>
iDestructHyp
H
as
(
x1
x2
x3
)
pat
).
Tactic
Notation
"iPoseProof"
open_constr
(
lem
)
"as"
"("
simple_intropattern
(
x1
)
simple_intropattern
(
x2
)
simple_intropattern
(
x3
)
simple_intropattern
(
x4
)
")"
constr
(
pat
)
:
=
iPoseProofCore
lem
as
pat
false
(
fun
H
=>
iDestructHyp
H
as
(
x1
x2
x3
x4
)
pat
).
iPoseProofCore
lem
as
pat
(
fun
H
=>
iDestructHyp
H
as
(
x1
x2
x3
x4
)
pat
).
Tactic
Notation
"iPoseProof"
open_constr
(
lem
)
"as"
"("
simple_intropattern
(
x1
)
simple_intropattern
(
x2
)
simple_intropattern
(
x3
)
simple_intropattern
(
x4
)
simple_intropattern
(
x5
)
")"
constr
(
pat
)
:
=
iPoseProofCore
lem
as
pat
false
(
fun
H
=>
iDestructHyp
H
as
(
x1
x2
x3
x4
x5
)
pat
).
iPoseProofCore
lem
as
pat
(
fun
H
=>
iDestructHyp
H
as
(
x1
x2
x3
x4
x5
)
pat
).
Tactic
Notation
"iPoseProof"
open_constr
(
lem
)
"as"
"("
simple_intropattern
(
x1
)
simple_intropattern
(
x2
)
simple_intropattern
(
x3
)
simple_intropattern
(
x4
)
simple_intropattern
(
x5
)
simple_intropattern
(
x6
)
")"
constr
(
pat
)
:
=
iPoseProofCore
lem
as
pat
false
(
fun
H
=>
iDestructHyp
H
as
(
x1
x2
x3
x4
x5
x6
)
pat
).
iPoseProofCore
lem
as
pat
(
fun
H
=>
iDestructHyp
H
as
(
x1
x2
x3
x4
x5
x6
)
pat
).
Tactic
Notation
"iPoseProof"
open_constr
(
lem
)
"as"
"("
simple_intropattern
(
x1
)
simple_intropattern
(
x2
)
simple_intropattern
(
x3
)
simple_intropattern
(
x4
)
simple_intropattern
(
x5
)
simple_intropattern
(
x6
)
simple_intropattern
(
x7
)
")"
constr
(
pat
)
:
=
iPoseProofCore
lem
as
pat
false
(
fun
H
=>
iDestructHyp
H
as
(
x1
x2
x3
x4
x5
x6
x7
)
pat
).
iPoseProofCore
lem
as
pat
(
fun
H
=>
iDestructHyp
H
as
(
x1
x2
x3
x4
x5
x6
x7
)
pat
).
Tactic
Notation
"iPoseProof"
open_constr
(
lem
)
"as"
"("
simple_intropattern
(
x1
)
simple_intropattern
(
x2
)
simple_intropattern
(
x3
)
simple_intropattern
(
x4
)
simple_intropattern
(
x5
)
simple_intropattern
(
x6
)
simple_intropattern
(
x7
)
simple_intropattern
(
x8
)
")"
constr
(
pat
)
:
=
iPoseProofCore
lem
as
pat
false
(
fun
H
=>
iDestructHyp
H
as
(
x1
x2
x3
x4
x5
x6
x7
x8
)
pat
).
iPoseProofCore
lem
as
pat
(
fun
H
=>
iDestructHyp
H
as
(
x1
x2
x3
x4
x5
x6
x7
x8
)
pat
).
Tactic
Notation
"iPoseProof"
open_constr
(
lem
)
"as"
"("
simple_intropattern
(
x1
)
simple_intropattern
(
x2
)
simple_intropattern
(
x3
)
simple_intropattern
(
x4
)
simple_intropattern
(
x5
)
simple_intropattern
(
x6
)
simple_intropattern
(
x7
)
simple_intropattern
(
x8
)
simple_intropattern
(
x9
)
")"
constr
(
pat
)
:
=
iPoseProofCore
lem
as
pat
false
(
fun
H
=>
iDestructHyp
H
as
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
)
pat
).
iPoseProofCore
lem
as
pat
(
fun
H
=>
iDestructHyp
H
as
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
)
pat
).
Tactic
Notation
"iPoseProof"
open_constr
(
lem
)
"as"
"("
simple_intropattern
(
x1
)
simple_intropattern
(
x2
)
simple_intropattern
(
x3
)
simple_intropattern
(
x4
)
simple_intropattern
(
x5
)
simple_intropattern
(
x6
)
simple_intropattern
(
x7
)
simple_intropattern
(
x8
)
simple_intropattern
(
x9
)
simple_intropattern
(
x10
)
")"
constr
(
pat
)
:
=
iPoseProofCore
lem
as
pat
false
(
fun
H
=>
iDestructHyp
H
as
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
x10
)
pat
).
iPoseProofCore
lem
as
pat
(
fun
H
=>
iDestructHyp
H
as
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
x10
)
pat
).
(** * Induction *)
(* An invocation of [iInduction (x) as pat IH forall (x1...xn) Hs] will
...
...
@@ 2212,7 +2191,7 @@ Local Ltac iRewriteFindPred :=
end
.
Local
Tactic
Notation
"iRewriteCore"
constr
(
lr
)
open_constr
(
lem
)
:
=
iPoseProofCore
lem
as
true
true
(
fun
Heq
=>
iPoseProofCore
lem
as
true
(
fun
Heq
=>
eapply
(
tac_rewrite
_
Heq
_
_
lr
)
;
[
pm_reflexivity

let
Heq
:
=
pretty_ident
Heq
in
...
...
@@ 2227,7 +2206,7 @@ Tactic Notation "iRewrite" open_constr(lem) := iRewriteCore Right lem.
Tactic
Notation
"iRewrite"
""
open_constr
(
lem
)
:
=
iRewriteCore
Left
lem
.
Local
Tactic
Notation
"iRewriteCore"
constr
(
lr
)
open_constr
(
lem
)
"in"
constr
(
H
)
:
=
iPoseProofCore
lem
as
true
true
(
fun
Heq
=>
iPoseProofCore
lem
as
true
(
fun
Heq
=>
eapply
(
tac_rewrite_in
_
Heq
_
_
H
_
_
lr
)
;
[
pm_reflexivity

let
Heq
:
=
pretty_ident
Heq
in
...
...
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