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.

Decidable propositions I

In our last post, we looked at relations and briefly showed how Lean can sometimes prove a relation is decidable. Here, we take a closer look at decidability, a concept that rests on three pillars:

  • An inductive type class through which propositions can be marked as decidable.
  • A type class inference system for automatically proving decidability of propositions. This system is not limited to decidable but pertains to all type classes.
  • A mechanism for automatically proving true decidable propositions via type class inference.

In this post, we discuss the first two points. The follow-on posts are Decidable propositions II and Decidable propositions III.

The decidable type class

decidable is an inductive type class with two constructors.

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

Thus, to provide an instance of decidable p is either to prove ¬p or to prove p. For instance, we can produce instances of decidable true and decidable false.

instance decidable_true : decidable true := is_true trivial

instance decidable_false : decidable false :=
is_false (λ q, false.elim q)

Here, trivial is a proof of true.

Of greater interest, we can use instances to derive other instances. Below, we produce an instance of decidable ¬p, given an instance of decidable p.

instance decidable_not (p : Prop) [h : decidable p] : decidable ¬p :=
match h with
| (is_false hnp)  := is_true hnp
| (is_true hp)    := is_false (λ hnp, hnp hp)
end

Likewise, an instance of decidable (p ∧ q) can be produced from instances of decidable p and decidable q.

instance decidable_and (p q : Prop) [h₁ : decidable p]
[h₂ : decidable q] : decidable (p ∧ q) :=
match h₁, h₂ with
| (is_false hnp), h₂              := is_false (λ hpq, hnp hpq.left)
| (is_true hp),   (is_false hnq)  := is_false (λ hpq, hnq hpq.right)
| (is_true hp),   (is_true hq)    := is_true ⟨hp, hq⟩ 
end

Try proving decidable (p ∨ q) using the same idea.

Type class inference

Now the clever bit. To prove decidable (p → q), we can rewrite p → q as ¬p ∨ q (a task that, admittedly, requires decidability of p) and then ask Lean to apply the instances it already knows!

instance decidable_if (p q : Prop) [h₁ : decidable p]
[h₂ : decidable q] : decidable (p → q) :=
by { rw imp_iff_not_or, apply_instance }

Lean first reduces the problem to finding instances of decidable ¬p and decidable q. The latter is a hypothesis. The former, reduced (via our result decidable_not) to finding an instance of decidable p.

In term-mode, infer_instance plays the same role as the tactic apply_instance.

example (p q : Prop) [decidable p] [decidable q] :
decidable $ (p ∧ q) → q := infer_instance

Relations in Lean

What is a relation?

In a typical undergraduate mathematics course, a relation on a set \(A\) is defined to be a subset of \(A\times A\), the cartesian product of \(A\) with itself.

In the Lean approach, a relation on a type α is a function of type α → α → Prop. That is, a function that takes two terms x and y of type α and returns a Prop.

The Lean approach corresponds much more closely with the intuitive notion of relation than does the more traditional approach. Consider the following definition.

def near_to (x y : ℕ) : Prop := (x - y) < 5 ∧ (y - x) < 5

This defines a relation on natural numbers. It is reflexive and symmetric, but not transitive. Here’s a proof of reflexivity.

example : reflexive near_to :=
begin
  intro x, split; { rw nat.sub_self, norm_num }, 
end

What does this do? The definition of reflexive (which one finds by typing #print reflexive) is:

def reflexive : Π {β : Sort v}, (β → β → Prop) → Prop :=
λ {β : Sort v} (r : β → β → Prop), ∀ (x : β), r x x

So to prove that a relation on a type β is reflexive is precisely to show ∀ (x : β), r x x. Our proof begins by introducing a term x of type ℕ. To prove near_to x x is to show (x – x) < 5 ∧ (x – x) < 5. Each conjunct is dealt with identically.

As an exercise, fill in the sorrys in the following. Post your solutions as a comment!

example : symmetric near_to := sorry

example : ¬(transitive near_to) := sorry

Decidable relations

It would be nice if we could deduce simple numerical results with minimal effort. We’ll see how to do that and also introduce some nice notation.

The command below introduces the symbol ∼ to be used as an infix name for the relation near_to.

local infix `∼`:50 := near_to

With this notation, we’ll prove 5 is near to 7.

example : 5 ∼ 7 := by { split; norm_num }

Fine. But can’t Lean just see this obvious fact? It can if we can prove that near_to is a decidable_rel. That is, we must show for every x and y that near_to x y is decidable, a proposition for which there is an algorithm for determining its truth or falsity.

Fortunately, Lean provides a mechanism that can, in many cases, automatically derive that a relation (or Prop) is decidable. Having made the above definition, we can invoke the derive handler by adding the attribute [derive decidable_rel] to near_to. Make sure first to import tactic.

attribute [derive decidable_rel] near_to 

Alternatively, the previous definition could be decorated:

@[derive decidable_rel]
def near_to (x y : ℕ) : Prop := (x - y) < 5 ∧ (y - x) < 5

Via either method, Lean will derive that a typeclass instance of decidable_rel near_to. After this, the previous numerical result can be proved using dec_trivial,

example : 5 ∼ 7 := dec_trivial