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)

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⟩ 

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

2 thoughts on “Decidable propositions I

  1. Pingback: Decidable propositions II – exlean

  2. Pingback: Decidable propositions III – exlean

Leave a Reply

Your email address will not be published. Required fields are marked *