convoy pattern

Stream: general

[Oliver Nash]

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?

[Eric Wieser]

cases h : foo n with k

[Oliver Nash]

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