## Stream: new members

### Topic: Proof of function containing match statement

#### Do Nhat Minh (Jun 27 2019 at 21:35):

I'm working on a proof of a function containing match statements (see here). I cannot get Lean to unfold the definitions for the implicit match statements (e.g., one at line 10). Could anyone please give me some tips on how to proceed?

#### Kenny Lau (Jun 27 2019 at 21:37):

have you tried change?

#### Do Nhat Minh (Jun 27 2019 at 21:44):

@Kenny Lau, could you give an example of how to use it?

#### Kenny Lau (Jun 27 2019 at 21:45):

def f (n : ℕ) : ℕ :=
match n with
| 0 := 1
| (k+1) := 0
end

example (hf : f 0 = 2) : true :=
begin
change 1 = 2 at hf,
guard_hyp hf := 1 = 2,
trivial
end


#### Do Nhat Minh (Jun 27 2019 at 22:35):

sorry to bother you again, @Kenny Lau , but I can't get it to work... In your example, Lean changes f 0 = 2 to 1 = 2 in the type of hf. But in my case, the input to the implicit match is not a concrete value, but a recursive function call (type_check gamma t_a_1) and h_w. How can I use change in this case?

#### Kevin Kappelmann (Jun 27 2019 at 22:48):

Not sure if I understand what you are trying to do, but if you match on your recursive function call, say f t, then you might wanna do something like cases (f t) in your proof.

#### Kenny Lau (Jun 27 2019 at 22:52):

import tactic.interactive

def f (n : ℕ) : ℕ :=
match n with
| 0 := 1
| (k+1) := 0
end

example (n:ℕ) (hf : f (n + n) = 2) : true :=
begin
generalize_hyp h : n + n = m at hf,
cases m,
case nat.zero { change 1 = 2 at hf, trivial },
case nat.succ : m { change 0 = 2 at hf, trivial }
end


@Do Nhat Minh

#### Do Nhat Minh (Jun 27 2019 at 23:46):

Thanks, @Kenny Lau and @Kevin Kappelmann . I got a little bit further thanks to @Kevin Kappelmann's advice.

Last updated: May 18 2021 at 16:25 UTC