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