Proof of function containing match statement

Stream: new members

[Do Nhat Minh]

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]

have you tried change?

[Do Nhat Minh]

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

[Kenny Lau]

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]

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]

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]

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

[Kenny Lau]

@Do Nhat Minh

[Do Nhat Minh]

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