Stream: new members
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 :: 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
 doesn't match
(0 :: g), and hence it should use the second pattern to evaluate
f (0 :: g)?
Yakov Pechersky (Aug 01 2020 at 00:01):
0 :: _ :: l?
Yakov Pechersky (Aug 01 2020 at 00:02):
Because  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,  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
. 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