Zulip Chat Archive

Stream: new members

Topic: dev_null n = 0


view this post on Zulip 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)

view this post on Zulip Anas Himmi (Feb 07 2021 at 10:48):

Use induction

view this post on Zulip Huỳnh Trần Khanh (Feb 07 2021 at 10:51):

Wow that worked. Thanks.

view this post on Zulip 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

view this post on Zulip 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 .

view this post on Zulip 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