From bec1b1b9198af0c370b68412393895d75e2d68cb Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Sun, 6 Feb 2022 12:35:54 -0500
Subject: [PATCH] Revising for tomorrow's lecture

---
 Interpreters.v |  6 +++---
 frap_book.tex  | 10 +++-------
 2 files changed, 6 insertions(+), 10 deletions(-)

diff --git a/Interpreters.v b/Interpreters.v
index e06d7ed..0ee4f76 100644
--- a/Interpreters.v
+++ b/Interpreters.v
@@ -220,7 +220,7 @@ Proof.
    * an induction hypothesis.  Let's ask Coq to search its library for lemmas
    * that would justify such a rewrite, giving a pattern with wildcards, to
    * specify the essential structure that the rewrite should match. *)
-  SearchRewrite ((_ ++ _) ++ _).
+  Search ((_ ++ _) ++ _).
   (* Ah, we see just the one! *)
   rewrite app_assoc_reverse.
   rewrite IHe1.
@@ -251,8 +251,8 @@ Proof.
 
   (* To match the form of our lemma, we need to replace [compile e] with
    * [compile e ++ nil], adding a "pointless" concatenation of the empty list.
-   * [SearchRewrite] again helps us find a library lemma. *)
-  SearchRewrite (_ ++ nil).
+   * [Search] again helps us find a library lemma. *)
+  Search (_ ++ nil).
   rewrite (app_nil_end (compile e)).
   (* Note that we can use [rewrite] with explicit values of the first few
    * quantified variables of a lemma.  Otherwise, [rewrite] picks an
diff --git a/frap_book.tex b/frap_book.tex
index 757d58a..2115a95 100644
--- a/frap_book.tex
+++ b/frap_book.tex
@@ -711,7 +711,6 @@ We apply the following notations throughout the book: \\
 
 As the name advertises, finite maps are functions with finite domains, where the domain may be expanded by each extension operation.
 Two axioms explain the essential interactions of the basic operators.
-
 $$\infer{\msel{\mupd{m}{k}{v}}{k} = v}{}
 \quad
 \infer{\msel{\mupd{m}{k_1}{v}}{k_2} = m(k_2)}{
@@ -723,7 +722,7 @@ $$\infer{\msel{\mupd{m}{k}{v}}{k} = v}{}
 With these operators in hand, we can write a semantics for arithmetic expressions.
 This is a recursive function that \emph{maps variable valuations to numbers}.
 We write $\denote{e}$ for the meaning of $e$; this notation is often referred to as \emph{Oxford brackets}\index{Oxford brackets}.
-Recall that we allow notations like this as syntactic sugar for arbitrary functions, even when giving the equations that define those functions.
+Recall that we allow this kind of notation as syntactic sugar for arbitrary functions, even when giving the equations that define those functions.
 We write $v$ for a valuation (finite map).
 \encoding
 \begin{eqnarray*}
@@ -758,7 +757,6 @@ We can prove a key compatibility property of these two recursive functions.
 
 That is, in some sense, the operations of interpretation and substitution \emph{commute} with each other.
 That intuition gives rise to the common notion of a \emph{commuting diagram}\index{commuting diagram}, like the one below for this particular example.
-
 \[
 \begin{tikzcd}
 (e, v) \arrow{r}{\subst{\ldots}{x}{e'}} \arrow{d}{\mupd{\ldots}{x}{\denote{e'}v}} & (\subst{e}{x}{e'}, v) \arrow{d}{\denote{\ldots}} \\
@@ -916,7 +914,7 @@ We'll write $\opt{\ldots}$ for this and other optimizations, which move neither
 
 Note that, when multiple defining equations apply to some function input, by convention we apply the \emph{earliest} equation that matches.
 
-Let's prove that this optimization preserves program behavior; that is, we prove that it is \emph{semantics preserving}\index{semantics preservation}.
+Let's prove that this optimization preserves program behavior; that is, we prove that it is \emph{semantics-preserving}\index{semantics preservation}.
 
 \begin{theorem}\label{unroll}
   $\denote{\opt{c}}v = \denote{c}v$.
@@ -925,7 +923,6 @@ Let's prove that this optimization preserves program behavior; that is, we prove
 It all looks so straightforward from that statement, doesn't it?
 Indeed, there actually isn't so much work to do to prove this theorem.
 We can also present it as a commuting diagram much like the prior one.
-
 \[
 \begin{tikzcd}
 c \arrow{r}{\opt{\ldots}} \arrow{dr}{\denote{\ldots}} & \opt{c} \arrow{d}{\denote{\ldots}} \\
@@ -933,14 +930,13 @@ c \arrow{r}{\opt{\ldots}} \arrow{dr}{\denote{\ldots}} & \opt{c} \arrow{d}{\denot
 \end{tikzcd}
 \]
 
-The statement of Theorem \ref{unroll} happens to already be in the right form to do induction directly, but we need a helper lemma, capturing the interaction of $^nc$ and the semantics.
+The statement of Theorem \ref{unroll} happens to be already in the right form to do induction directly, but we need a helper lemma, capturing the interaction of $^nc$ and the semantics.
 
 \begin{lemma}
   $\denote{^nc} = \denote{c}^n$.
 \end{lemma}
 
 Let us end the chapter with the commuting-diagram version of the lemma statement.
-
 \[
 \begin{tikzcd}
 c \arrow{r}{^n\ldots} \arrow{d}{\denote{\ldots}} & ^nc \arrow{d}{\denote{\ldots}} \\