Handling inductive definitions

Stream: new members

[Pim Spelier]

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

[Yakov Pechersky]

0 :: _ :: l?

[Yakov Pechersky]

Because [0] does match 0 :: g

[Yakov Pechersky]

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

[Chris B]

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]

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]

How dare you golf me.