# 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``````

## 2 thoughts on “Decidable propositions I”

1. Pingback: Decidable propositions II – exlean

2. Pingback: Decidable propositions III – exlean