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
Jonas Kastberg
iris
Commits
2935cc99
Commit
2935cc99
authored
Feb 02, 2016
by
Robbert Krebbers
Browse files
Add documentation to heap_lang_tactics.
parent
735dd18f
Changes
1
Hide whitespace changes
Inline
Side-by-side
barrier/heap_lang_tactics.v
View file @
2935cc99
...
...
@@ -2,6 +2,12 @@ Require Export barrier.heap_lang.
Require
Import
prelude
.
fin_maps
.
Import
heap_lang
.
(** The tactic [inv_step] performs inversion on hypotheses of the shape
[prim_step] and [head_step]. For hypotheses of the shape [prim_step] it will
decompose the evaluation context. The tactic will discharge
head-reductions starting from values, and simplifies hypothesis related
to conversions from and to values, and finite map operations. This tactic is
slightly ad-hoc and tuned for proving our lifting lemmas. *)
Ltac
inv_step
:
=
repeat
match
goal
with
|
_
=>
progress
simplify_map_equality'
(* simplify memory stuff *)
...
...
@@ -21,6 +27,9 @@ Ltac inv_step :=
inversion
H
;
subst
;
clear
H
end
.
(** The tactic [reshape_expr e tac] decomposes the expression [e] into an
evaluation context [K] and a subexpression [e']. It calls the tactic [tac K e']
for each possible decomposition until [tac] succeeds. *)
Ltac
reshape_expr
e
tac
:
=
let
rec
go
K
e
:
=
match
e
with
...
...
@@ -60,6 +69,11 @@ Ltac reshape_expr e tac :=
end
end
in
go
(@
nil
ectx_item
)
e
.
(** The tactic [do_step tac] solves goals of the shape [reducible], [prim_step]
and [head_step] by performing a reduction step and uses [tac] to solve any
side-conditions generated by individual steps. In case of goals of the shape
[reducible] and [prim_step], it will try to decompose to expression on the LHS
into an evaluation context and head-redex. *)
Ltac
do_step
tac
:
=
try
match
goal
with
|-
language
.
reducible
_
_
=>
eexists
_
,
_
,
_
end
;
simpl
;
...
...
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