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