Commit 27cfd068 authored by Ralf Jung's avatar Ralf Jung

heao_lang/tactics: update some comments

parent 2c790e9b
Pipeline #392 passed with stage
...@@ -2,12 +2,11 @@ From iris.heap_lang Require Export substitution. ...@@ -2,12 +2,11 @@ From iris.heap_lang Require Export substitution.
From iris.prelude Require Import fin_maps. From iris.prelude Require Import fin_maps.
Import heap_lang. Import heap_lang.
(** The tactic [inv_step] performs inversion on hypotheses of the shape (** The tactic [inv_step] performs inversion on hypotheses of the
[prim_step] and [head_step]. For hypotheses of the shape [prim_step] it will shape [head_step]. The tactic will discharge head-reductions starting
decompose the evaluation context. The tactic will discharge from values, and simplifies hypothesis related to conversions from and
head-reductions starting from values, and simplifies hypothesis related to values, and finite map operations. This tactic is slightly ad-hoc
to conversions from and to values, and finite map operations. This tactic is and tuned for proving our lifting lemmas. *)
slightly ad-hoc and tuned for proving our lifting lemmas. *)
Ltac inv_step := Ltac inv_step :=
repeat match goal with repeat match goal with
| _ => progress simplify_map_eq/= (* simplify memory stuff *) | _ => progress simplify_map_eq/= (* simplify memory stuff *)
...@@ -64,11 +63,10 @@ Ltac reshape_expr e tac := ...@@ -64,11 +63,10 @@ Ltac reshape_expr e tac :=
| CAS ?e0 ?e1 ?e2 => go (CasLCtx e1 e2 :: K) e0 | CAS ?e0 ?e1 ?e2 => go (CasLCtx e1 e2 :: K) e0
end in go (@nil ectx_item) e. end in go (@nil ectx_item) e.
(** The tactic [do_step tac] solves goals of the shape [reducible], [prim_step] (** The tactic [do_step tac] solves goals of the shape
and [head_step] by performing a reduction step and uses [tac] to solve any [head_reducible] and [head_step] by performing a reduction step and
side-conditions generated by individual steps. In case of goals of the shape uses [tac] to solve any side-conditions generated by individual
[reducible] and [prim_step], it will try to decompose to expression on the LHS steps. *)
into an evaluation context and head-redex. *)
Tactic Notation "do_step" tactic3(tac) := Tactic Notation "do_step" tactic3(tac) :=
try match goal with |- head_reducible _ _ => eexists _, _, _ end; try match goal with |- head_reducible _ _ => eexists _, _, _ end;
simpl; simpl;
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment