Zulip Chat Archive

Stream: new members

Topic: Handling inductive definitions


view this post on Zulip Pim Spelier (Jul 31 2020 at 23:19):

I'm having trouble with handling inductive definitions with overlapping patterns. A MWE of what I'm trying to do (or at least, as minimal as I can get it):

def f : list   
| [0] := 0
| (0 :: l) := 1
| _ := arbitrary 

variables (g : list ) (hg : g  [])

include hg
def eval_fg : (f (0 :: g) = 1) :=
begin
  sorry
end

As far as I understand, this definition is allowed (and it indeed compiles), and when calculating f, it'll take the first matching pattern. But how can I tell Lean that the pattern [0] doesn't match (0 :: g), and hence it should use the second pattern to evaluate f (0 :: g)?

view this post on Zulip Yakov Pechersky (Aug 01 2020 at 00:01):

0 :: _ :: l?

view this post on Zulip Yakov Pechersky (Aug 01 2020 at 00:02):

Because [0] does match 0 :: g

view this post on Zulip Yakov Pechersky (Aug 01 2020 at 00:03):

Or have f take a proof about the non emptiness of l

view this post on Zulip Chris B (Aug 01 2020 at 01:02):

Your definition is fine too since you included a hypothesis that g != 0.

def eval_fg : (f (0 :: g) = 1) :=
begin
  cases g,
  exfalso,
  apply hg,
  refl,
  unfold f,
end

Just to add to what he said, [0] is (0 :: nil).

view this post on Zulip Pim Spelier (Aug 01 2020 at 01:10):

Thanks, that works! I forgot that cases could help me here, as lean does know that 0 :: g_hd :: g_tl does not match the pattern [0]. The proof can even be shortened to

include hg
def eval_fg : (f (0 :: g) = 1) :=
begin
  cases g;
  trivial,
end

view this post on Zulip Chris B (Aug 01 2020 at 01:11):

How dare you golf me.


Last updated: May 15 2021 at 23:13 UTC