Replace use of impossible idiom with proof by reflection (#409)

* Added section on proof by reflection to Decidable.
* Define True in Decidable.
* Add exercise for defining False in Decidable.
* Rewrote text in Lambda to reflection new section on proof by reflection.
* Replace S constructor in Lambda with a version which checks the inequality implicitly.
* Define product and unit types as records in Connectives.
* Explain difference between data and records w.r.t. definitional equality in Connectives.

src/plfa/part1/Connectives.lagda.md

@@ -44,7 +44,7 @@ open plfa.part1.Isomorphism.≃-Reasoning
 
 Given two propositions `A` and `B`, the conjunction `A × B` holds
 if both `A` holds and `B` holds.  We formalise this idea by
-declaring a suitable inductive type:
+declaring a suitable record type:
 ```
 data _×_ (A B : Set) : Set where
 
@@ -76,27 +76,6 @@ proj₂ ⟨ x , y ⟩ = y
 If `L` provides evidence that `A × B` holds, then `proj₁ L` provides evidence
 that `A` holds, and `proj₂ L` provides evidence that `B` holds.
 
-Equivalently, we could also declare conjunction as a record type:
-```
-record _×′_ (A B : Set) : Set where
-  field
-    proj₁′ : A
-    proj₂′ : B
-open _×′_
-```
-Here record construction
-
-    record
-      { proj₁′ = M
-      ; proj₂′ = N
-      }
-
-corresponds to the term
-
-    ⟨ M , N ⟩
-
-where `M` is a term of type `A` and `N` is a term of type `B`.
-
 When `⟨_,_⟩` appears in a term on the right-hand side of an equation
 we refer to it as a _constructor_, and when it appears in a pattern on
 the left-hand side of an equation we refer to it as a _destructor_.
@@ -114,10 +93,7 @@ formula for the connective, which appears in a hypothesis but not in
 the conclusion. An introduction rule describes under what conditions
 we say the connective holds---how to _define_ the connective. An
 elimination rule describes what we may conclude when the connective
-holds---how to _use_ the connective.
+holds---how to _use_ the connective.[^from-wadler-2015]
-
-(The paragraph above was adopted from "Propositions as Types", Philip Wadler,
-_Communications of the ACM_, December 2015.)
 
 In this case, applying each destructor and reassembling the results with the
 constructor is the identity over products:
@@ -136,6 +112,33 @@ infixr 2 _×_
 ```
 Thus, `m ≤ n × n ≤ p` parses as `(m ≤ n) × (n ≤ p)`.
 
+Alternatively, we can declare conjunction as a record type:
+```
+record _×′_ (A B : Set) : Set where
+  constructor ⟨_,_⟩′
+  field
+    proj₁′ : A
+    proj₂′ : B
+open _×′_
+```
+The record construction `record { proj₁′ = M ; proj₂′ = N }` corresponds to the
+term `⟨ M , N ⟩` where `M` is a term of type `A` and `N` is a term of type `B`.
+The constructor declaration allows us to write `⟨ M , N ⟩′` in place of the
+record construction.
+
+The data type `_x_` and the record type `_×′_` behave similarly. One
+difference is that for data types we have to prove η-equality, but for record
+types, η-equality holds *by definition*. While proving `η-×′`, we do not have to
+pattern match on `w` to know that η-equality holds:
+```
+η-×′ : ∀ {A B : Set} (w : A ×′ B) → ⟨ proj₁′ w , proj₂′ w ⟩′ ≡ w
+η-×′ w = refl
+```
+It can be very convenient to have η-equality *definitionally*, and so the
+standard library defines `_×_` as a record type. We use the definition from the
+standard library in later chapters.
+
+
 Given two types `A` and `B`, we refer to `A × B` as the
 _product_ of `A` and `B`.  In set theory, it is also sometimes
 called the _Cartesian product_, and in computing it corresponds
@@ -245,7 +248,7 @@ is isomorphic to `(A → B) × (B → A)`.
 ## Truth is unit
 
 Truth `⊤` always holds. We formalise this idea by
-declaring a suitable inductive type:
+declaring a suitable record type:
 ```
 data ⊤ : Set where
 
@@ -266,10 +269,33 @@ value of type `⊤` must be equal to `tt`:
 η-⊤ : ∀ (w : ⊤) → tt ≡ w
 η-⊤ tt = refl
 ```
-The pattern matching on the left-hand side is essential.  Replacing
+The pattern matching on the left-hand side is essential. Replacing
 `w` by `tt` allows both sides of the propositional equality to
 simplify to the same term.
 
+Alternatively, we can declare truth as an empty record:
+```
+record ⊤′ : Set where
+  constructor tt′
+```
+The record construction `record {}` corresponds to the term `tt`. The
+constructor declaration allows us to write `tt′`.
+
+As with the product, the data type `⊤` and the record type `⊤′` behave
+similarly, but η-equality holds *by definition* for the record type. While
+proving `η-⊤′`, we do not have to pattern match on `w`---Agda *knows* it is
+equal to `tt′`:
+```
+η-⊤′ : ∀ (w : ⊤′) → tt′ ≡ w
+η-⊤′ w = refl
+```
+Agda knows that *any* value of type `⊤′` must be `tt′`, so any time we need a
+value of type `⊤′`, we can tell Agda to figure it out:
+```
+truth′ : ⊤′
+truth′ = _
+```
+
 We refer to `⊤` as the _unit_ type. And, indeed,
 type `⊤` has exactly one member, `tt`.  For example, the following
 function enumerates all possible arguments of type `⊤`:
@@ -790,3 +816,6 @@ This chapter uses the following unicode:
     ₁  U+2081  SUBSCRIPT ONE (\_1)
     ₂  U+2082  SUBSCRIPT TWO (\_2)
     ⇔  U+21D4  LEFT RIGHT DOUBLE ARROW (\<=>)
+
+
+[^from-wadler-2015]: This paragraph was adopted from "Propositions as Types", Philip Wadler, _Communications of the ACM_, December 2015.

src/plfa/part1/Decidable.lagda.md

@@ -548,7 +548,7 @@ postulate
 #### Exercise `iff-erasure` (recommended)
 
 Give analogues of the `_⇔_` operation from
-Chapter [Isomorphism]({{ site.baseurl }}/Isomorphism/#iff),
+Chapter [Isomorphism]({{ site.baseurl}}/Isomorphism/#iff),
 operation on booleans and decidables, and also show the corresponding erasure:
 ```
 postulate
@@ -561,13 +561,86 @@ postulate
 -- Your code goes here
 ```
 
+## Proof by reflection {#proof-by-reflection}
+
+Let's revisit our definition of monus from
+Chapter [Naturals]({{ site.baseurl}}/Naturals/).
+If we subtract a larger number from a smaller number, we take the result to be
+zero. We had to do something, after all. What could we have done differently? We
+could have defined a *guarded* version of minus, a function which subtracts `n`
+from `m` only if `n ≤ m`:
+
+```
+minus : (m n : ℕ) (n≤m : n ≤ m) → ℕ
+minus m       zero    _         = m
+minus (suc m) (suc n) (s≤s m≤n) = minus m n m≤n
+```
+
+Unfortunately, it is painful to use, since we have to explicitly provide
+the proof that `n ≤ m`:
+
+```
+_ : minus 5 3 (s≤s (s≤s (s≤s z≤n))) ≡ 2
+_ = refl
+```
+
+We cannot solve this problem in general, but in the scenario above, we happen to
+know the two numbers *statically*. In that case, we can use a technique called
+*proof by reflection*. Essentially, we can ask Agda to run the decidable
+equality `n ≤? m` while type checking, and make sure that `n ≤ m`!
+
+We do this by using a feature of implicits. Agda will fill in an implicit of a
+record type if it can fill in all its fields. So Agda will *always* manage to
+fill in an implicit of an *empty* record type, since there aren't any fields
+after all. This is why `⊤` is defined as an empty record.
+
+The trick is to have an implicit argument of the type `T ⌊ n ≤? m ⌋`. Let's go
+through what this means step-by-step. First, we run the decision procedure, `n
+≤? m`. This provides us with evidence whether `n ≤ m` holds or not. We erase the
+evidence to a boolean. Finally, we apply `T`. Recall that `T` maps booleans into
+the world of evidence: `true` becomes the unit type `⊤`, and `false` becomes the
+empty type `⊥`. Operationally, an implicit argument of this type works as a
+guard.
+
+- If `n ≤ m` holds, the type of the implicit value reduces to `⊤`. Agda then
+  happily provides the implicit value.
+- Otherwise, the type reduces to `⊥`, which Agda has no chance of providing, so
+  it will throw an error. For instance, if we call `3 - 5` we get `_n≤m_254 : ⊥`.
+
+We obtain the witness for `n ≤ m` using `toWitness`, which we defined earlier:
+
+```
+_-_ : (m n : ℕ) {n≤m : T ⌊ n ≤? m ⌋} → ℕ
+_-_ m n {n≤m} = minus m n (toWitness n≤m)
+```
+
+We can safely use `_-_` as long as we statically know the two numbers:
+
+```
+_ : 5 - 3 ≡ 2
+_ = refl
+```
+
+It turns out that this idiom is very common. The standard library defines a
+synonym for `T ⌊ ? ⌋` called `True`:
+
+```
+True : ∀ {Q} → Dec Q → Set
+True Q = T ⌊ Q ⌋
+```
+
+#### Exercise `False`
+
+Give analogues of `True`, `toWitness`, and `fromWitness` which work with *negated* properties. Call these `False`, `toWitnessFalse`, and `fromWitnessFalse`.
+
+
 ## Standard Library
 
 ```
 import Data.Bool.Base using (Bool; true; false; T; _∧_; _∨_; not)
 import Data.Nat using (_≤?_)
 import Relation.Nullary using (Dec; yes; no)
-import Relation.Nullary.Decidable using (⌊_⌋; toWitness; fromWitness)
+import Relation.Nullary.Decidable using (⌊_⌋; True; toWitness; fromWitness)
 import Relation.Nullary.Negation using (¬?)
 import Relation.Nullary.Product using (_×-dec_)
 import Relation.Nullary.Sum using (_⊎-dec_)

src/plfa/part1/Isomorphism.lagda.md

@@ -170,8 +170,7 @@ the fourth that `to ∘ from` is the identity, hence the names.
 The declaration `open _≃_` makes available the names `to`, `from`,
 `from∘to`, and `to∘from`, otherwise we would need to write `_≃_.to` and so on.
 
-The above is our first use of records. A record declaration is equivalent
+The above is our first use of records. A record declaration behaves similar to a single-constructor data declaration (there are minor differences, which we discuss in [Connectives]({{ site.baseurl }}/Connectives/)):
-to a corresponding inductive data declaration:
 ```
 data _≃′_ (A B : Set): Set where
   mk-≃′ : ∀ (to : A → B) →

src/plfa/part1/Relations.lagda.md

@@ -19,7 +19,7 @@ the next step is to define relations, such as _less than or equal_.
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl; cong)
 open import Data.Nat using (ℕ; zero; suc; _+_)
-open import Data.Nat.Properties using (+-comm)
+open import Data.Nat.Properties using (+-comm; +-identityʳ)
 ```
 
 
@@ -129,13 +129,25 @@ One may also identify implicit arguments by name:
 _ : 2 ≤ 4
 _ = s≤s {m = 1} {n = 3} (s≤s {m = 0} {n = 2} (z≤n {n = 2}))
 ```
-In the latter format, you may only supply some implicit arguments:
+In the latter format, you can choose to only supply some implicit arguments:
 ```
 _ : 2 ≤ 4
 _ = s≤s {n = 3} (s≤s {n = 2} z≤n)
 ```
 It is not permitted to swap implicit arguments, even when named.
 
+We can ask Agda to use the same inference to try and infer an _explicit_ term,
+by writing `_`. For instance, we can define a variant of the proposition
+`+-identityʳ` with implicit arguments:
+```
++-identityʳ′ : ∀ {m : ℕ} → m + zero ≡ m
++-identityʳ′ = +-identityʳ _
+```
+We use `_` to ask Agda to infer the value of the _explicit_ argument from
+context. There is only one value which gives us the correct proof, `m`, so Agda
+happily fills it in.
+If Agda fails to infer the value, it reports an error.
+
 
 ## Precedence
 

src/plfa/part2/Lambda.lagda.md

@@ -53,12 +53,15 @@ four.
 ## Imports
 
 ```
+open import Data.Bool using (T; not)
 open import Data.Empty using (⊥; ⊥-elim)
 open import Data.List using (List; _∷_; [])
 open import Data.Nat using (ℕ; zero; suc)
 open import Data.Product using (∃-syntax; _×_)
 open import Data.String using (String; _≟_)
 open import Relation.Nullary using (Dec; yes; no; ¬_)
+open import Relation.Nullary.Decidable using (⌊_⌋; False; toWitnessFalse)
+open import Relation.Nullary.Negation using (¬?)
 open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
 ```
 
@@ -1087,6 +1090,26 @@ Constructor `S` takes an additional parameter, which ensures that
 when we look up a variable that it is not _shadowed_ by another
 variable with the same name to its left in the list.
 
+It can be rather tedious to use the `S` constructor, as you have to provide
+proofs that `x ≢ y` each time. For example:
+
+```
+_ : ∅ , "x" ⦂ `ℕ ⇒ `ℕ , "y" ⦂ `ℕ , "z" ⦂ `ℕ ∋ "x" ⦂ `ℕ ⇒ `ℕ
+_ = S (λ()) (S (λ()) Z)
+```
+
+Instead, we'll use a "smart constructor", which uses [proof by reflection]({{ site.baseurl }}/Decidable/#proof-by-reflection) to check the inequality while type checking:
+
+```
+S′ : ∀ {Γ x y A B}
+   → {x≢y : False (x ≟ y)}
+   → Γ ∋ x ⦂ A
+     ------------------
+   → Γ , y ⦂ B ∋ x ⦂ A
+
+S′ {x≢y = x≢y} x = S (toWitnessFalse x≢y) x
+```
+
 ### Typing judgment
 
 The second judgment is written
@@ -1214,7 +1237,7 @@ Ch A = (A ⇒ A) ⇒ A ⇒ A
 ⊢twoᶜ : ∀ {Γ A} → Γ ⊢ twoᶜ ⦂ Ch A
 ⊢twoᶜ = ⊢ƛ (⊢ƛ (⊢` ∋s · (⊢` ∋s · ⊢` ∋z)))
   where
-  ∋s = S (λ()) Z
+  ∋s = S′ Z
   ∋z = Z
 ```
 
@@ -1227,11 +1250,11 @@ Here are the typings corresponding to computing two plus two:
 ⊢plus = ⊢μ (⊢ƛ (⊢ƛ (⊢case (⊢` ∋m) (⊢` ∋n)
          (⊢suc (⊢` ∋+ · ⊢` ∋m′ · ⊢` ∋n′)))))
   where
-  ∋+  = (S (λ()) (S (λ()) (S (λ()) Z)))
+  ∋+  = S′ (S′ (S′ Z))
-  ∋m  = (S (λ()) Z)
+  ∋m  = S′ Z
   ∋n  = Z
   ∋m′ = Z
-  ∋n′ = (S (λ()) Z)
+  ∋n′ = S′ Z
 
 ⊢2+2 : ∅ ⊢ plus · two · two ⦂ `ℕ
 ⊢2+2 = ⊢plus · ⊢two · ⊢two
@@ -1250,9 +1273,9 @@ And here are typings for the remainder of the Church example:
 ⊢plusᶜ : ∀ {Γ A} → Γ  ⊢ plusᶜ ⦂ Ch A ⇒ Ch A ⇒ Ch A
 ⊢plusᶜ = ⊢ƛ (⊢ƛ (⊢ƛ (⊢ƛ (⊢` ∋m · ⊢` ∋s · (⊢` ∋n · ⊢` ∋s · ⊢` ∋z)))))
   where
-  ∋m = S (λ()) (S (λ()) (S (λ()) Z))
+  ∋m = S′ (S′ (S′ Z))
-  ∋n = S (λ()) (S (λ()) Z)
+  ∋n = S′ (S′ Z)
-  ∋s = S (λ()) Z
+  ∋s = S′ Z
   ∋z = Z
 
 ⊢sucᶜ : ∀ {Γ} → Γ ⊢ sucᶜ ⦂ `ℕ ⇒ `ℕ