dev_null n = 0

Stream: new members

[Huỳnh Trần Khanh]

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]

Use induction

[Huỳnh Trần Khanh]

Wow that worked. Thanks.

[Eric Wieser]

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]

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

[Kevin Buzzard]

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