Recall from our previous post the definition of decidable
.
class inductive decidable (p : Prop) : Type
| is_false : ¬p → decidable
| is_true : p → decidable
We’ll later discuss how this class works in conjunction with type class inference to automate proofs of decidable
propositions. In this post, we show how conditionals are implemented in Lean using the decidable
recursor.
If-then-else
The ite
function is one of two Lean implementations of an ‘if-then-else’ construct.
def ite (c : Prop) [d : decidable c] {α} (t e : α) : α := decidable.rec_on d (λ hnc, e) (λ hc, t)
Given a decidable
proposition c and terms t and e of some Sort α, the expression ite c t e reduces to e in the case that c ‘is false’ and to t in the case that c ‘is true’. By ‘is true’, I mean that the instance d results from the application of the is_false constructor of decidable. Likewise for ‘is true’.
In the following example application, the proposition c
is 5 = 6
. But where is the instance of decidable (5 = 6)
?
lemma foo : ite (5 = 6) 10 20 = 20 := rfl
The answer is that Lean uses type class inference to provide the appropriate instance. You can see this in action by enabling the display of implicit parameters then printing the definition of foo
.
set_option pp.implicit true
#print foo
Lean spits out (inter alia):
theorem foo : @ite ℕ (5 = 6) (nat.decidable_eq 5 6) 10 20 = 20
@rfl ℕ (@ite ℕ (5 = 6) (nat.decidable_eq 5 6) 10 20)
nat.decidable_eq 5 6
is an proof of decidable (5=6)
. This is a simple example, but Lean can use type class inference to chain instances:
lemma bar : ite (5 ≠ 6) 10 20 = 10 := rfl
The lemma bar
has definition:
theorem bar : @ite ℕ (5 ≠ 6) (@ne.decidable ℕ (λ (a b : ℕ), nat.decidable_eq a b) 5 6) 10 20 = 10 :=
@rfl ℕ (@ite ℕ (5 ≠ 6) (@ne.decidable ℕ (λ (a b : ℕ), nat.decidable_eq a b) 5 6) 10 20)
Lean has chained ne.decidable
and nat.decidable_eq
to prove decidable (5 ≠ 6)
.
Dependent if-then-else
For some applications, it isn’t sufficient to know whether a proposition p
is true of false, we may also need a proof of the truth or falsity of p
. The solution is to use dite
, the dependent if-then-else function.
def dite {α} (c : Prop) [h : decidable c] : (c → α) → (¬ c → α) → α := λ t e, decidable.rec_on h e t
Given a decidable proposition c
, given t : c → α
and e : ¬ c → α
, the term dite c t e
either to t hc
, for a given proof hc : c
or to e hnc
, for a proof hnc : ¬c
.
As an example, we prove the law of the excluded middle, that p ∨ ¬p
for a decidable proposition p
.
lemma em (p : Prop) [decidable p] : p ∨ ¬p
:= dite p (λ hp, or.inl hp) (λ hnp, or.inr hnp)
If-then-else notation
ite
and dite
are so important that Lean facilitates their use via special notation. Our lemma bar
can be written in this notation as:
lemma bar : (if (5 ≠ 6) then 10 else 20) = 10 := rfl
Similarly, the law of the excluded middle has the following proof:
lemma em (p : Prop) [decidable p] : p ∨ ¬p :=
if hp : p then or.inl hp else or.inr hp
Take care with the latter notation: in the ‘then’ clause above, hp
is a proof of p
whereas hp
is a proof of ¬p
in the ‘else’ clause.
Using this notation, we define a function mod
such that mod a b
is be the least natural number c
such that \(a\equiv c\pmod b\).
def mod : ℕ → ℕ → ℕ
| a 0 := a
| a (b + 1) :=
if h : a < (b + 1) then a else
have a - (b + 1) < a, from nat.sub_lt (show 0 < a, by linarith) (show 0 < (b+1), by linarith),
mod (a - (b + 1)) (b + 1)
The have
expression above is needed for well-founded recursion.
Pingback: Decidable propositions I – exlean
Pingback: Decidable propositions III – exlean