Decidable propositions II

Recall from our previous post the definition of decidable.

class inductive decidable (p : Prop) : Type
| is_false  : ¬p → decidable
| is_true   : p → decidable

We’ll later discuss how this class works in conjunction with type class inference to automate proofs of decidable propositions. In this post, we show how conditionals are implemented in Lean using the decidable recursor.

If-then-else

The ite function is one of two Lean implementations of an ‘if-then-else’ construct.

def ite (c : Prop) [d : decidable c] {α} (t e : α) : α := decidable.rec_on d (λ hnc, e) (λ hc, t)

Given a decidable proposition c and terms t and e of some Sort α, the expression ite c t e reduces to e in the case that c ‘is false’ and to t in the case that c ‘is true’. By ‘is true’, I mean that the instance d results from the application of the is_false constructor of decidable. Likewise for ‘is true’.

In the following example application, the proposition c is 5 = 6. But where is the instance of decidable (5 = 6)?

lemma foo : ite (5 = 6) 10 20 = 20 := rfl

The answer is that Lean uses type class inference to provide the appropriate instance. You can see this in action by enabling the display of implicit parameters then printing the definition of foo.

set_option pp.implicit true

#print foo

Lean spits out (inter alia):

theorem foo : @ite ℕ (5 = 6) (nat.decidable_eq 5 6) 10 20 = 20
@rfl ℕ (@ite ℕ (5 = 6) (nat.decidable_eq 5 6) 10 20)

nat.decidable_eq 5 6 is an proof of decidable (5=6). This is a simple example, but Lean can use type class inference to chain instances:

lemma bar : ite (5 ≠ 6) 10 20 = 10 := rfl

The lemma bar has definition:

theorem bar : @ite ℕ (5 ≠ 6) (@ne.decidable ℕ (λ (a b : ℕ), nat.decidable_eq a b) 5 6) 10 20 = 10 :=
@rfl ℕ (@ite ℕ (5 ≠ 6) (@ne.decidable ℕ (λ (a b : ℕ), nat.decidable_eq a b) 5 6) 10 20)

Lean has chained ne.decidable and nat.decidable_eq to prove decidable (5 ≠ 6).

Dependent if-then-else

For some applications, it isn’t sufficient to know whether a proposition p is true of false, we may also need a proof of the truth or falsity of p. The solution is to use dite, the dependent if-then-else function.

def dite {α} (c : Prop) [h : decidable c] : (c → α) → (¬ c → α) → α := λ t e, decidable.rec_on h e t

Given a decidable proposition c, given t : c → α and e : ¬ c → α, the term dite c t e either to t hc, for a given proof hc : c or to e hnc, for a proof hnc : ¬c.

As an example, we prove the law of the excluded middle, that p ∨ ¬p for a decidable proposition p.

lemma em (p : Prop) [decidable p] : p ∨ ¬p
:= dite p (λ hp, or.inl hp) (λ hnp, or.inr hnp)

If-then-else notation

ite and dite are so important that Lean facilitates their use via special notation. Our lemma bar can be written in this notation as:

lemma bar : (if (5 ≠ 6) then 10 else 20) = 10 := rfl

Similarly, the law of the excluded middle has the following proof:

lemma em (p : Prop) [decidable p] : p ∨ ¬p :=
if hp : p then or.inl hp else or.inr hp

Take care with the latter notation: in the ‘then’ clause above, hp is a proof of p whereas hp is a proof of ¬p in the ‘else’ clause.

Using this notation, we define a function mod such that mod a b is be the least natural number c such that \(a\equiv c\pmod b\).

def mod : ℕ → ℕ → ℕ
| a 0       := a
| a (b + 1)   :=  
if h : a < (b + 1) then a else
  have a - (b + 1) < a, from nat.sub_lt (show 0 < a, by linarith) (show 0 < (b+1), by linarith),
  mod (a - (b + 1)) (b + 1)

The have expression above is needed for well-founded recursion.