Zulip Chat Archive

Stream: general

Topic: convoy pattern


view this post on Zulip Oliver Nash (Jan 26 2021 at 14:23):

What is the right way to prove bar_spec in the following snippet:

def foo (n : ) := n + n

def bar (n : ) :  :=
match foo n with
| 0     := 0
| k + 1 := foo n -- Key property: value here depends on (in fact equals) pattern we're matching.
end

lemma bar_spec {n : } : bar n = foo n :=
begin
  unfold bar,
  cases foo n with k,
  { refl, },
  { change foo n = k + 1,
    -- No access to fact that `foo n = k + 1` from match.
    sorry, },
end

If I remember my Coq correctly, I'd use the so-called "convoy pattern" there but I'm hoping there's some tactic that saves me from such things in Lean / Mathlib?

view this post on Zulip Eric Wieser (Jan 26 2021 at 14:25):

cases h : foo n with k

view this post on Zulip Oliver Nash (Jan 26 2021 at 14:25):

Thanks :-) I must have tried every variant I could think of except that!


Last updated: May 08 2021 at 04:14 UTC