## Stream: general

### Topic: convoy pattern

#### 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?

#### Eric Wieser (Jan 26 2021 at 14:25):

cases h : foo n with k

#### 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