Zulip Chat Archive

Stream: new members

Topic: Proof of function containing match statement


view this post on Zulip 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?

view this post on Zulip Kenny Lau (Jun 27 2019 at 21:37):

have you tried change?

view this post on Zulip Do Nhat Minh (Jun 27 2019 at 21:44):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jun 27 2019 at 22:53):

@Do Nhat Minh

view this post on Zulip 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