Decidable propositions III

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