From 4d24e7095b678695f0d9fc89141d0a847857886d Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sun, 28 Nov 2021 01:48:01 -0800
Subject: [PATCH] Make some more progress on the UCC evaluator article

---
 content/blog/coq_dawn_eval.md | 57 +++++++++++++++++++++++++++++++++--
 1 file changed, 54 insertions(+), 3 deletions(-)

diff --git a/content/blog/coq_dawn_eval.md b/content/blog/coq_dawn_eval.md
index 3af286d..58890a0 100644
--- a/content/blog/coq_dawn_eval.md
+++ b/content/blog/coq_dawn_eval.md
@@ -265,10 +265,61 @@ eval_chain nil (e_comp (e_comp true false) or) (true :: nil)
 
 This is the type of sequences (or chains) of steps corresponding to the
 evaluation of the program \\(\\text{true}\\ \\text{false}\\ \\text{or}\\),
-starting in an empty stack and evaluating to a stack with only true on top.
-Thus to say that an expression evaluates to some final stack `vs'`, in
-_some unknown number of steps_, it's sufficient to write:
+starting in an empty stack and evaluating to a stack with only
+\\(\\text{true}\\) on top. Thus to say that an expression evaluates to some
+final stack `vs'`, in _some unknown number of steps_, it's sufficient to write:
 
 ```Coq
 eval_chain vs e vs'
 ```
+
+Evaluation chains have a couple of interesting properties. First and foremost,
+they can be "concatenated". This is analagous to the `Sem_e_comp` rule
+in our original semantics: if an expression `e1` starts in stack `vs`
+and finishes in stack `vs'`, and another expression starts in stack `vs'`
+and finishes in stack `vs''`, then we can compose these two expressions,
+and the result will start in `vs` and finish in `vs''`.
+
+{{< codelines "Coq" "dawn/DawnEval.v" 69 75 >}}
+
+The proof is very short. We go
+{{< sidenote "right" "concat-note" "by induction on the left evaluation" >}}
+It's not a coincidence that defining something like <code>(++)</code>
+(list concatenation) in Haskell typically starts by pattern matching
+on the <em>left</em> list. In fact, proofs by <code>induction</code>
+actually correspond to recursive functions! It's tough putting code blocks
+in sidenotes, but if you're playing with the
+<a href="https://dev.danilafe.com/Web-Projects/blog-static/src/branch/master/code/dawn/DawnEval.v"><code>DawnEval.v</code></a> file, try running
+<code>Print eval_chain_ind</code>, and note the presence of <code>fix</code>,
+the <a href="https://en.wikipedia.org/wiki/Fixed-point_combinator">fixed point
+combinator</a> used to implement recursion.
+{{< /sidenote >}}
+chain (the one for `e1`). Coq takes care of most of the rest with `auto`.
+The key to this proof is that whatever `P` is cotained within a "node"
+in the left chain determines how `eval_step (e_comp e1 e2)` behaves. Whether
+`e1` evaluates to `final` or `middle`, the composition evaluates to `middle`
+(a composition of two expressions cannot be done in one step), so we always
+{{< sidenote "left" "cons-note" "create a new \"cons\" node." >}}
+This is <em>unlike</em> list concatenation, since we typically don't
+create new nodes when appending to an empty list.
+{{< /sidenote >}} via `chain_middle`. Then, the two cases are as follows:
+
+* If the step was `final`, then
+  the rest of the steps use only `e2`, and good news, we already have a chain
+  for that!
+* Otherwise, the step was `middle`, an we stll have a chain for some
+  intermediate program `ei` that starts in some stack `vsi` and ends in `vs'`.
+  By induction, we know that _this_ chain can be concatenated with the one
+  for `e2`, resulting in a chain for `e_comp ei e2`. All that remains is to
+  attach to this sub-chain the one step from `(vs, e1)` to `(vsi, ei)`, which
+  is handled by `chain_middle`.
+
+  {{< todo >}}A drawing would be nice here!{{< /todo >}}
+
+The `merge` operation is reversible; chains can be split into two pieces,
+one for each composed expression:
+
+{{< codelines "Coq" "dawn/DawnEval.v" 77 78 >}}
+
+While interesting, this particular fact isn't used anywhere else in this
+post, and I will omit the proof here.