12 Decidable

Given a property or relation, we can compute whether it holds using Booleans, or we can produce inductively-defined evidence that it holds (or does not hold). There are pros and cons for each approach. The advantage of Booleans is that we’re all used to computing with them. But a Boolean value doesn’t tell us why it was computed that way, what the implications are. The colloquial term for this is "Boolean blindness". It’s not as easy to compute with evidence, but it’s a lot easier to reason with it.

It’s an intermediate-level Agda technique to go back and forth between one approach and the other as needed. This is made a lot easier by decorating Booleans with that missing justification. That is, instead of a value that is "true" or "false", we have an indication of "true" together with a proof of it, or an indication of "false" with a proof of it. This is the basis of the Dec inductive datatype.

This chapter explores the use of Dec, and argues that it should be preferred to the use of Booleans. It will be used in the second half of PLFA.

12.1 Relating evidence and computation

I believe this file is the first time where one difference between Agda 2.5.4.2 (originally used to develop PLFA) and Agda 2.6 is evident. In Agda 2.6, a definitional equation that contains an absurd pattern can be omitted as long as there is at least one that does not. The completeness checker can deduce and verify the omitted line, and interactive development will not generate it. This means that one of the lines in T→≡ and ≤ᵇ→≤ will not be generated if we start from scratch, as we do with the starter file. It doesn’t hurt to include the lines, so the code in PLFA is not incorrect, and a case can be made that including them improves readability. We’ll see this more and more as we continue with PLFA, so please don’t be alarmed by this minor divergence.

12.2 The best of both worlds

data Dec (A : Set) : Set where
  yes :   A → Dec A
  no  : ¬ A → Dec A

The design of a function to decide inequality for natural numbers using this definition strongly resembles the Boolean function. The only slight wrinkle is that helper functions are preferred to compute negative evidence, rather than lambdas, due to the different ways that top-level definitions and pattern lambdas are handled in Agda.

¬s≤z : ∀ {m : ℕ} → ¬ (suc m ≤ zero)
¬s≤z ()

¬s≤s : ∀ {m n : ℕ} → ¬ (m ≤ n) → ¬ (suc m ≤ suc n)
¬s≤s ¬m≤n (s≤s x) = ¬m≤n x

_≤?_ : ∀ (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)

12.3 Logical connectives

Since Dec is a generalization of Bool, it’s not surprising that the Boolean operators can be extended to operations on Dec. Once again, I’ve chosen not to produce asciicasts of the material in this section, to avoid the repetitive effect of slight variations on the same techniques. Trying to derive the implementations yourself is good practice.

12.4 Proof by reflection

The idea introduced in this section is a small, specific instance of a general technique, where decision procedures are used to compute parts of a proof. In this case we automate the use of the decision procedure during typechecking, taking advantage of the handling of implicits that are record types. This is essentially a convenient hack that will save us from having to provide labourious proofs of obvious propositions later on, in the Lambda chapter.

The version of Dec presented in this chapter is the one originally used in the Agda standard library. However, recent revisions have replaced it with a record whose fields contain the Boolean value and the proof. This leads to more desirable computational behaviour. yes and no are still available, defined as "pattern synonyms", so previous proofs (including those in PLFA) will still work. The library module README.Design.Decidability has more details on the reasons and implications of the change.

When using the library code (as we will later), the synonyms will not be used by Agda during interaction (much as with the syntax for ∃). In anticipation, I’ll briefly describe the library version, so it won’t come as a surprise.

We start with a datatype that wraps up evidence for or against a proposition P, but in addition, indexed by the appropriate Boolean (we say the Boolean value "reflects" the truth value) and with constructor names that will make sense shortly.

data Reflects {p} (P : Set p) : Bool → Set p where
  ofʸ : ( p :   P) → Reflects P true
  ofⁿ : (¬p : ¬ P) → Reflects P false

The new Dec is now a two-field record, the first being the Boolean value, and the second (dependent on the first) the proof it reflects.

record Dec {p} (P : Set p) : Set p where
  constructor _because_
  field
    does  : Bool
    proof : Reflects P does

During interaction, when we have a pattern variable of type Dec P, and we split on it, it will expand to something like does₁ because proof₁. The new variable does₁ takes on Boolean values, and the new variable proof₁ will be ofʸ p for p a proof of P, or ofⁿ ¬p for ¬p a proof of ¬ P. That motivates the following pattern definitions.

pattern yes p =  true because ofʸ  p
pattern no ¬p = false because ofⁿ ¬p

You can practice with these by using the import given at the bottom of the PLFA chapter, but I don’t think it’s really necessary; if it looks confusing later on, just refer back to this description.