Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
I
Iris
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
0
Issues
0
List
Boards
Labels
Service Desk
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Operations
Operations
Incidents
Environments
Analytics
Analytics
CI / CD
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
Rodolphe Lepigre
Iris
Commits
7b9d27ea
Verified
Commit
7b9d27ea
authored
Jun 17, 2019
by
Paolo G. Giarrusso
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Drop lazy_tc argument
parent
160b8c97
Changes
3
Hide whitespace changes
Inline
Side-by-side
Showing
3 changed files
with
28 additions
and
43 deletions
+28
-43
tests/proofmode.ref
tests/proofmode.ref
+7
-7
theories/heap_lang/proofmode.v
theories/heap_lang/proofmode.v
+1
-1
theories/proofmode/ltac_tactics.v
theories/proofmode/ltac_tactics.v
+20
-35
No files found.
tests/proofmode.ref
View file @
7b9d27ea
...
...
@@ -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 @
7b9d27ea
...
...
@@ -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 @
7b9d27ea
...
...
@@ -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
...
...
@@ -1078,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"
:
=
...
...
@@ -1737,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
=>
...
...
@@ -1746,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 *)
...
...
@@ -1804,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
...
...
@@ -2206,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
...
...
@@ -2221,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