## Stream: new members

### Topic: Handling inductive definitions

#### 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)?

0 :: _ :: l?

#### Yakov Pechersky (Aug 01 2020 at 00:02):

Because [0] does match 0 :: g

#### Yakov Pechersky (Aug 01 2020 at 00:03):

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

#### 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).

#### 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


#### Chris B (Aug 01 2020 at 01:11):

How dare you golf me.

Last updated: May 15 2021 at 23:13 UTC