## Stream: new members

### Topic: dev_null n = 0

#### Huỳnh Trần Khanh (Feb 07 2021 at 10:41):

How would you prove that dev_null n = 0?

def dev_null : ℕ → ℕ
| 0 := 0
| (n + 1) := dev_null n

example { n : ℕ } : dev_null n = 0 := begin
sorry,
end


I don't really know how to prove properties about recursive functions defined through pattern matching. I have been dodging it by using if-then-else expressions instead and then unfold and split_ifs.

def dev_null_2 : ℕ → ℕ
| n := if is_zero: n = 0 then 0 else have n - 1 < n := buffer.lt_aux_2 (pos_iff_ne_zero.mpr is_zero), dev_null_2 (n - 1)


#### Anas Himmi (Feb 07 2021 at 10:48):

Use induction

#### Huỳnh Trần Khanh (Feb 07 2021 at 10:51):

Wow that worked. Thanks.

#### Eric Wieser (Feb 07 2021 at 11:06):

Or using the equation compiler:

lemma dev_null_zero : ∀ n, dev_null n = 0
| 0 := rfl
| (n + 1) := dev_null_zero n


but induction is usually easier to use

#### Kevin Buzzard (Feb 07 2021 at 11:13):

@Huỳnh Trần Khanh you might want to look at chapters 7 and 8 of #tpil .

#### Kevin Buzzard (Feb 07 2021 at 11:17):

In particular, at the beginning of chapter 8 they go through examples of how to prove theorems about inductive types.

Last updated: May 10 2021 at 23:11 UTC