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

Pingback: Decidable propositions II – exlean

Pingback: Decidable propositions III – exlean