From 90ce509af6ddb811d1489bb8ff07fc78d7e6816a Mon Sep 17 00:00:00 2001
From: wadler <wadler@inf.ed.ac.uk>
Date: Sat, 13 Jul 2019 20:46:33 -0300
Subject: [PATCH] small changes

---
 extra/iso-exercise.lagda | 48 ++++++++++++++++++++++++++++++++++++++++
 src/plfa/Decidable.lagda |  2 +-
 src/plfa/Lambda.lagda    | 15 +++++++++----
 3 files changed, 60 insertions(+), 5 deletions(-)
 create mode 100644 extra/iso-exercise.lagda

diff --git a/extra/iso-exercise.lagda b/extra/iso-exercise.lagda
new file mode 100644
index 00000000..22de31b5
--- /dev/null
+++ b/extra/iso-exercise.lagda
@@ -0,0 +1,48 @@
+\begin{code}
+module iso-exercise where
+
+import Relation.Binary.PropositionalEquality as Eq
+open Eq using (_≡_; refl; cong₂)
+open Eq.≡-Reasoning
+open import plfa.Isomorphism using (_≃_)
+open import Data.List using (List; []; _∷_)
+open import Data.List.All using (All; []; _∷_)
+open import Data.List.Any using (Any; here; there)
+open import Data.List.Membership.Propositional using (_∈_)
+open import Function using (_∘_)
+
+postulate
+  extensionality : ∀ {A : Set} {B : A → Set} {C : A → Set} {f g : {x : A} → B x → C x}
+                → (∀ {x : A} (bx : B x) → f {x} bx ≡ g {x} bx)
+                  --------------------------------------------
+                → (λ {x} → f {x}) ≡ (λ {x} → g {x})
+
+f : ∀ {A : Set} {P : A → Set} {xs : List A} → All P xs → (∀ {x} -> x ∈ xs -> P x)
+f [] ()
+f (px ∷ pxs) (here refl) = px
+f (px ∷ pxs) (there x∈xs) = f pxs x∈xs
+
+g : ∀ {A : Set} {P : A → Set} {xs : List A} → (∀ {x} -> x ∈ xs -> P x) → All P xs
+g {xs = []} h = []
+g {xs = x ∷ xs} h = h {x} (here refl) ∷ g (h ∘ there)
+
+gf : ∀ {A : Set} {P : A → Set} {xs : List A} → ∀ (pxs : All P xs) → g (f pxs) ≡ pxs
+gf [] = refl
+gf (px ∷ pxs) = Eq.cong₂ _∷_ refl (gf pxs)
+
+fg : ∀ {A : Set} {P : A → Set} {xs : List A}
+      → ∀ (h : ∀ {x} -> x ∈ xs -> P x) → ∀ {x} (x∈ : x ∈ xs) → f (g h) {x} x∈ ≡ h {x} x∈
+fg {xs = []} h ()
+fg {xs = x ∷ xs} h (here refl) = refl
+fg {xs = x ∷ xs} h (there x∈xs) = fg (h ∘ there) x∈xs
+
+lemma : ∀ {A : Set} {P : A → Set} {xs : List A} → All P xs ≃ (∀ {x} -> x ∈ xs -> P x)
+lemma =
+  record
+    { to = f
+    ; from = g
+    ; from∘to = gf
+    ; to∘from = extensionality ∘ fg
+    }
+
+\end{code}
diff --git a/src/plfa/Decidable.lagda b/src/plfa/Decidable.lagda
index 7cd20aa6..a8db23ef 100644
--- a/src/plfa/Decidable.lagda
+++ b/src/plfa/Decidable.lagda
@@ -541,7 +541,7 @@ Show that erasure relates corresponding boolean and decidable operations:
 \begin{code}
 postulate
   ∧-× : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ ∧ ⌊ y ⌋ ≡ ⌊ x ×-dec y ⌋
-  ∨-× : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ ∨ ⌊ y ⌋ ≡ ⌊ x ⊎-dec y ⌋
+  ∨-⊎ : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ ∨ ⌊ y ⌋ ≡ ⌊ x ⊎-dec y ⌋
   not-¬ : ∀ {A : Set} (x : Dec A) → not ⌊ x ⌋ ≡ ⌊ ¬? x ⌋
 \end{code}
 
diff --git a/src/plfa/Lambda.lagda b/src/plfa/Lambda.lagda
index ca580c81..cf73ad5f 100644
--- a/src/plfa/Lambda.lagda
+++ b/src/plfa/Lambda.lagda
@@ -569,9 +569,9 @@ replaces the formal parameter by the actual parameter.
 
 If a term is a value, then no reduction applies; conversely,
 if a reduction applies to a term then it is not a value.
-We will show in the next chapter that for well-typed terms
-this exhausts the possibilities: for every well-typed term
-either a reduction applies or it is a value.
+We will show in the next chapter that 
+this exhausts the possibilities: every well-typed term
+either reduces or is a value.
 
 For numbers, zero does not reduce and successor reduces the subterm.
 A case expression reduces its argument to a number, and then chooses
@@ -628,13 +628,20 @@ data _—→_ : Term → Term → Set where
 
 The reduction rules are carefully designed to ensure that subterms
 of a term are reduced to values before the whole term is reduced.
-This is referred to as _call by value_ reduction.
+This is referred to as _call-by-value_ reduction.
 
 Further, we have arranged that subterms are reduced in a
 left-to-right order.  This means that reduction is _deterministic_:
 for any term, there is at most one other term to which it reduces.
 Put another way, our reduction relation `—→` is in fact a function.
 
+This style of explaining the meaning of terms is called
+a _small-step operational semantics_.  If `M —→ N`, we say that
+term `M` _reduces_ to term `N`, or equivalently,
+term `M` _steps_ to term `N`.  Each compatibility rule has
+another reduction rule in its premise; so a step always consists
+of a beta rule, possibly adjusted by zero or more compatibility rules.
+
 
 #### Quiz