added simpler example to Lambda and Properties

src/plta/Lambda.lagda

@@ -669,6 +669,24 @@ above are isomorphic.
 
 ## Examples
 
+We start with a simple example. The Church numeral two applied to the
+successor function and zero yields the natural number two.
+\begin{code}
+_ : twoᶜ · sucᶜ · `zero ↠ `suc `suc `zero
+_ =
+  begin
+    twoᶜ · sucᶜ · `zero
+  ↦⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩
+    (ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · `zero
+  ↦⟨ β-ƛ V-zero ⟩
+    sucᶜ · (sucᶜ · `zero)
+  ↦⟨ ξ-·₂ V-ƛ (β-ƛ V-zero) ⟩
+    sucᶜ · `suc `zero
+  ↦⟨ β-ƛ (V-suc V-zero) ⟩
+   `suc (`suc `zero)
+  ∎
+\end{code}
+
 Here is a sample reduction demonstrating that two plus two is four.
 \begin{code}
 _ : four ↠ `suc `suc `suc `suc `zero

src/plta/Properties.lagda

@@ -1058,8 +1058,32 @@ _ : eval (gas 3) ⊢sucμ ≡
 _ = refl
 \end{code}
 
-Similarly, we can use Agda to compute the reduction sequence for two plus two
+Similarly, we can use Agda to compute the reductions sequences given
-given in the preceding chapter.  Supplying 100 steps of gas is more than enough.
+in the previous chapter.  We start with the Church numeral two
+applied to successor and zero.  Supplying 100 steps of gas is more than enough.
+\begin{code}
+_ : eval (gas 100) (⊢twoᶜ · ⊢sucᶜ · ⊢zero) ≡
+  steps
+  ((ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) · (ƛ "n" ⇒ `suc ` "n")
+   · `zero
+   ↦⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩
+   (ƛ "z" ⇒ (ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · ` "z")) ·
+   `zero
+   ↦⟨ β-ƛ V-zero ⟩
+   (ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · `zero) ↦⟨
+   ξ-·₂ V-ƛ (β-ƛ V-zero) ⟩
+   (ƛ "n" ⇒ `suc ` "n") · `suc `zero ↦⟨ β-ƛ (V-suc V-zero) ⟩
+   `suc (`suc `zero) ∎)
+  (done (V-suc (V-suc V-zero)))
+_ = refl
+\end{code}
+The example above was generated by using `C `N to normalise the
+left-hand side of the equation and pasting in the result as the
+right-hand side of the equation.  The example reduction of the
+previous chapter was derived from this result, reformatting and
+writing `twoᶜ` and `sucᶜ` in place of their expansions.
+
+Next, we show two plus two is four.
 \begin{code}
 _ : eval (gas 100) ⊢four ≡
   steps
@@ -1219,11 +1243,8 @@ _ : eval (gas 100) ⊢four ≡
   (done (V-suc (V-suc (V-suc (V-suc V-zero)))))
 _ = refl
 \end{code}
-The example above was generated by using `C `N to normalise the
+Again, the derivation in the previous chapter was derived by
-left-hand side of the equation and pasting in the result as the
+editing the above.
-right-hand side of the equation.  The example reduction of the
-previous chapter was derived from this result, by writing `plus` and
-`two` in place of their corresponding expansions and reformatting.
 
 Similarly, can evaluate the corresponding term for Church numerals.
 \begin{code}
@@ -1290,7 +1311,7 @@ _ : eval (gas 100) ⊢fourᶜ ≡
   (done (V-suc (V-suc (V-suc (V-suc V-zero)))))
 _ = refl
 \end{code}
-Again, the example in the previous section was derived by editing the
+And again, the example in the previous section was derived by editing the
 above.
 
 ## Well-typed terms don't get stuck