fix to Decidable and related extra files

src/Decidable.lagda

@@ -212,25 +212,43 @@ or of the form `no ¬x`, where `¬x` provides evidence that `A` cannot hold
 
 For example, here is a function which given two numbers decides whether one
 is less than or equal to the other, and provides evidence to justify its conclusion.
+
+First, we introduce two functions useful for constructing evidence that
+an inequality does not hold.
+\begin{code}
+¬s≤z : ∀ {m : ℕ} → ¬ (suc m ≤ zero)
+¬s≤z ()
+
+¬s≤s : ∀ {m n : ℕ} → ¬ (m ≤ n) → ¬ (suc m ≤ suc n)
+¬s≤s ¬m≤n (s≤s m≤n) = ¬m≤n m≤n
+\end{code}
+The first of these asserts that `¬ (suc m ≤ zero)`, and follows by
+absurdity, since any evidence of inequality has the form `zero ≤ n`
+or `suc m ≤ suc n`, neither of which match `suc m ≤ suc n`. The second
+of these takes evidence `¬m≤n` of `¬ (m ≤ n)` and returns a proof of
+`¬ (suc m ≤ suc n)`.  Any evidence of `suc m ≤ suc n` must have the
+form `s≤s m≤n` where `m≤n` is evidence that `m ≤ n`.  Hence, we have
+a contradiction, evidenced by `¬m≤n m≤n`.
+
+Using these, it is straightforward to decide an inequality.
 \begin{code}
 _≤?_ : ∀ (m n : ℕ) → Dec (m ≤ n)
 zero ≤? n = yes z≤n
-suc m ≤? zero = no λ()
+suc m ≤? zero = no ¬s≤z
 suc m ≤? suc n with m ≤? n
 ... | yes m≤n = yes (s≤s m≤n)
-... | no ¬m≤n = no λ{ (s≤s m≤n) → ¬m≤n m≤n }
+... | no ¬m≤n = no (¬s≤s ¬m≤n)
 \end{code}
-As with `_≤ᵇ_`, the definition has three clauses.  In the first clause,
+As with `_≤ᵇ_`, the definition has three clauses.  In the first
-it is immediate that `zero ≤ n` holds, and it is evidenced by `z≤n`.
+clause, it is immediate that `zero ≤ n` holds, and it is evidenced by
-In the second clause, it is immediate that `suc m ≤ n` does not hold,
+`z≤n`.  In the second clause, it is immediate that `suc m ≤ n` does
-and the absence of possible evidence is attested by `λ()`.  In the third
+not hold, and it is evidenced by `¬s≤z`.
-clause, to decide whether `suc m ≤ suc n` holds we recursively invoke
+In the third clause, to decide whether `suc m ≤ suc n` holds we
-`m ≤? n`.  There are two possibilities.  In the `yes` case it returns evidence `m≤n` that
+recursively invoke `m ≤? n`.  There are two possibilities.  In the
-`m ≤ n`, and `s≤s m≤n` provides evidence that `suc m ≤ suc n`.
+`yes` case it returns evidence `m≤n` that `m ≤ n`, and `s≤s m≤n`
-In the `no` case it returns evidence `¬m≤n` that `¬ (m ≤ n)`.  Then given evidence
+provides evidence that `suc m ≤ suc n`.  In the `no` case it returns
-`s≤s m≤n` that `suc m ≤ suc n` holds, we can combine `¬m≤n` and `m≤n` to derive
+evidence `¬m≤n` that `¬ (m ≤ n)`, and `¬s≤s ¬m≤n` provides evidence
-a contradiction, and hence we know that `¬ (suc m ≤ suc n)`.  In the `no`
+that `¬ (suc m ≤ suc n)`.
-case, we need not consider `z≤n`, because it cannot prove `suc m ≤ suc n`.
 
 When we wrote `_≤ᵇ_`, we had to write two other functions, `≤ᵇ→≤` and `≤→≤ᵇ`,
 in order to show that it was correct.  In contrast, the definition of `_≤?_`
@@ -242,25 +260,19 @@ to derive them from the first.
 We can use our new function to *compute* the *evidence* that earlier we had to
 think up on our own.
 \begin{code}
-_ : Dec (2 ≤ 4)
+_ : 2 ≤? 4 ≡ yes (s≤s (s≤s z≤n))
-_ = 2 ≤? 4   -- evaluates to:  yes (s≤s (s≤s z≤n))
+_ = refl
 
-_ : Dec (4 ≤ 2)
+_ : 4 ≤? 2 ≡ no (¬s≤s (¬s≤s ¬s≤z))
-_ = 4 ≤? 2   -- evaluates to:  no λ{(s≤s (s≤s ()))}
+_ = refl
 \end{code}
-You can check that Agda will indeed compute these values.  Replace the
+You can check that Agda will indeed compute these values.  Typing
-right hand sides of the two equations above by holes; fill in the
+`^C ^N` and providing `2 ≤? 4` or `4 ≤? 2` as the requested expression
-holes with, respectively, `2 ≤? 4` and `4 ≤? 2`, then type `^C ^N`
+causes Agda to print the values given above.
-while in the holes to compute the corresponding values.  In the first
-case, it yields exactly the given value. In the second case, it
-yields
-
-    no (λ { (s≤s m≤n) → (λ { (s≤s m≤n) → (λ ()) m≤n }) m≤n })
-
-which simplifies to the value given above.  (As of this writing there
-is a bug in Agda, which yields a spurious `1` in the middle of the
-term above.)
 
+(A subtlety: if we do not define `¬s≤z` and `¬s≤s` as top-level functions,
+but instead use inline anonymous functions then Agda may have
+trouble normalising evidence of negation.)
 
 ## Decidables from booleans, and booleans from decidables
 

src/extra/DecidableBroken.agda

@@ -0,0 +1,35 @@
+import Relation.Binary.PropositionalEquality as Eq
+open Eq using (_≡_; refl)
+open import Data.Nat using (ℕ; zero; suc)
+open import Relation.Nullary using (Dec; yes; no)
+
+data _≤_ : ℕ → ℕ → Set where
+  z≤n : ∀ {n : ℕ} → zero ≤ n
+  s≤s : ∀ {m n : ℕ} → m ≤ n → suc m ≤ suc n
+
+_≤?_ : ∀ (m n : ℕ) → Dec (m ≤ n)
+zero ≤? n = yes z≤n
+suc m ≤? zero = no λ()
+suc m ≤? suc n with m ≤? n
+... | yes m≤n = yes (s≤s m≤n)
+... | no ¬m≤n = no λ{ (s≤s m≤n) → ¬m≤n m≤n }
+
+_ : Dec (2 ≤ 4)
+_ = 2 ≤? 4   -- yes (s≤s (s≤s z≤n))
+
+_ : 2 ≤? 4 ≡ yes (s≤s (s≤s z≤n))
+_ = refl
+
+_ : Dec (4 ≤ 2)
+_ = 4 ≤? 2   -- no λ{(s≤s (s≤s ()))}
+
+_ : 4 ≤? 2 ≡ no (λ { (s≤s m≤n) → (λ { (s≤s m≤n) → (λ ()) m≤n }) m≤n })
+_ = refl
+
+{-
+/Users/wadler/sf/src/extra/DecidableBroken.agda:27,5-9
+(λ { (s≤s m≤n) → (λ { (s≤s m≤n) → (λ ()) 1 m≤n }) m≤n }) x !=
+(λ { (s≤s m≤n) → _34 m≤n }) x of type .Data.Empty.⊥
+when checking that the expression refl has type
+(4 ≤? 2) ≡ no (λ { (s≤s m≤n) → _34 m≤n })
+-}

src/extra/DecidableFixed.agda

@@ -0,0 +1,28 @@
+import Relation.Binary.PropositionalEquality as Eq
+open Eq using (_≡_; refl)
+open import Data.Nat using (ℕ; zero; suc)
+open import Relation.Nullary using (¬_; Dec; yes; no)
+
+data _≤_ : ℕ → ℕ → Set where
+  z≤n : ∀ {n : ℕ} → zero ≤ n
+  s≤s : ∀ {m n : ℕ} → m ≤ n → suc m ≤ suc n
+
+¬s≤z : ∀ {m : ℕ} → ¬ (suc m ≤ zero)
+¬s≤z ()
+
+¬s≤s : ∀ {m n : ℕ} → ¬ (m ≤ n) → ¬ (suc m ≤ suc n)
+¬s≤s ¬m≤n (s≤s m≤n) = ¬m≤n m≤n
+
+_≤?_ : ∀ (m n : ℕ) → Dec (m ≤ n)
+zero ≤? n = yes z≤n
+suc m ≤? zero = no ¬s≤z
+suc m ≤? suc n with m ≤? n
+... | yes m≤n = yes (s≤s m≤n)
+... | no ¬m≤n = no (¬s≤s ¬m≤n)
+
+_ : 2 ≤? 4 ≡ yes (s≤s (s≤s z≤n))
+_ = refl
+
+_ : 4 ≤? 2 ≡ no (¬s≤s (¬s≤s ¬s≤z))
+_ = refl
+