Zulip Chat Archive

Stream: general

Topic: using induction hypothesis in match


Chris Hughes (Jan 27 2019 at 20:40):

Why does the second one work but not the first?

def id1 (x : ) :  :=
match x with
| 0 := 0
| (n+1) := _match n + 1 --fails
end

def id2 (x : ) :  :=
match x with
| 0 := 0
| (n+1) := by exact _match n + 1 --works
end

Mohammad Pedramfar (Jan 27 2019 at 20:48):

(deleted)

Sebastian Ullrich (Jan 27 2019 at 20:53):

Because the first one is intended to not work and the second one is not intended to work

Bryan Gin-ge Chen (Jan 27 2019 at 20:58):

I noticed this too, back here; I guess we're "supposed to" put x to the right of the colon like Mario did in that thread.

Chris Hughes (Jan 27 2019 at 21:31):

Sometimes x isn't an argument to the function however, it's something defined later.

Mario Carneiro (Jan 27 2019 at 21:48):

the "official" solution is to just have an auxiliary function, or use induction to construct the function. In lean 4, if my suggestion to sebastian worked, we will have an actual term mode notation for this using let


Last updated: Dec 20 2023 at 11:08 UTC