From 2935cc99f65a2a6531630373b840b79f74f2af1e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 2 Feb 2016 23:11:46 +0100
Subject: [PATCH] Add documentation to heap_lang_tactics.
---
barrier/heap_lang_tactics.v | 14 ++++++++++++++
1 file changed, 14 insertions(+)
diff --git a/barrier/heap_lang_tactics.v b/barrier/heap_lang_tactics.v
index 78fea003a..87e9f7a9d 100644
--- a/barrier/heap_lang_tactics.v
+++ b/barrier/heap_lang_tactics.v
@@ -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;
--
GitLab