We’ve seen the basics of `decidable`

in Decidable propositions I and if-then-else constructions in Decidable propostions II. Now, we’ll see how to prove results through type class inference.

If you’ve been following along and recreating `decidable`

in your own hidden namespace, it’s now time to declare an important, albeit trivial, instance.

`instance decidable_eq_self {α} (x : α) : decidable (x = x) := is_true rfl`

That is, it is decidable whether `x=x`

, for any `x : α`

and for any Sort `α`

. We’ll use this to show `5 ≠ 5`

is decidable.

`example : decidable (5 ≠ 5) := infer_instance`

How did this work? Surely we can only prove `5=5`

is decidable, not `5 ≠ 5`

? But recall we’ve already prove that `¬p`

is decidable if `p`

is. Type class inference chains together these two instances.

## True and false propositions

Consider the following proof:

`example : ite (5 = 5) true false := trivial`

The term `trivial`

is a proof of `true`

. But `ite (5 = 5) true false`

is definitionally equal to `true`

. Whence, `trivial`

is an appropriate proof!

For the remainder of this post, we’ll use a stripped-down version of the natural numbers, mynat. We do this to hide the type class instances that Lean knows about for the ordinary natural number type. If you don’t want to use `mynat`

, please just replace it everywhere below with `nat`

.

Here’s our proof of `decidable (a ≤ b)`

.

```
instance decidable_mynat_le (a : mynat) : ∀ b : mynat,
decidable (a ≤ b) :=
begin
induction a with a ha,
{ intro b, apply is_true, apply mynat.zero_le, },
{ intro b,
induction b with b hb,
{ apply is_false, apply not_succ_le_zero, },
{ cases ha b with h h,
{ apply is_false, intro h₂,
apply h, exact le_of_succ_le_succ h₂, },
{ apply is_true, exact succ_le_succ_of_le h, }, } },
end
```

Using this, we have,

`example : ite ((20 : mynat) ≤ 30) true false := trivial`

effectively showing that `20 ≤ 30`

is a true decidable proposition.

Likewise,

`example : ¬ ite ((30 : mynat) ≤ 20 ) true false := false.elim`

proves that `30 ≤ 20 `

is a false decidable proposition.

Trying to get Lean to prove the truth of a false decidable proposition gives an error message. The following code

`example : ite ((30 : mynat) ≤ 4) true false := trivial`

gives the error message

```
type mismatch, term
trivial
has type
true
but is expected to have type
ite (30 ≤ 4) true false
```

The previous examples were straightforward applications of single `decidable`

instances. Of more interest, we have that `(5 ≤ 6) ∧ (x = x)`

is a true decidable proposition for any `x`

. We know this because the type class inference systems allows Lean to derive a *decision procedure* for `(5 ≤ 6) ∧ (x = x)`

by chaining together decidability of `5 ≤ 6`

and of `x = x`

`example (x : mynat) : ite (((5 : mynat) ≤ 6) ∧ (x = x)) true false := trivial`

We’ve seen enough of these examples to justify introducing the following standard Lean definition,

`def as_true (c : Prop) [decidable c] : Prop := ite c true false`

so that the above proof is more succinctly expressed as

`example (x : mynat) : as_true (((5 : mynat) ≤ 6) ∧ (x = x)) := trivial`

## Proof of a true proposition

Really, we don’t want to prove `as_true c`

, we want to prove `c`

!

The following definition is a game-changer in this respect.

```
def of_as_true {c : Prop} [h₁ : decidable c] (h₂ : as_true c) : c :=
match h₁, h₂ with
| (is_true hc), h₂ := hc
| (is_false _), h₂ := false.elim h₂
end
```

At long last, here’s a proof of a true proposition, using type class inference. I’ve removed the `mynat`

type annotation just to clarify the exposition.

`example : (20 ≤ 30) ∧ (5 = 5) := of_as_true trivial`

As an exercise, come up with an example where the second pattern in `of_as_true`

is matched. You’ll end up proving a false statement, hence at least one of your hypotheses must be false.

Lean uses the notation `dec_trivial`

as a shorthand for `of_as_true trivial`

.

`example : (5 ≠ 7) ∧ (10 ≤ 20) := dec_trivial`

## Exercise

Referring to the definition of mynat, fill in the `sorry`

below:

`instance decidable_eq (x : mynat) : ∀ y : mynat, decidable (x = y) := sorry`

Pingback: Decidable propositions II – exlean

Pingback: What the rec? Types dependent on terms, Lean eliminators, and threshold concepts – exlean