## Stream: general

### Topic: proving properties of recursive functions with let/match

#### Alexandre Rademaker (Mar 09 2021 at 13:36):

After some experimenting I realise that using either let or match in a recursive definition like this is a lousy idea.

Thank you @Kevin Buzzard for your ideas. But the main point here is precise that your second -- and the standard definition -- for splitAt traverses the list twice. The implementation of splitAt with only one traverse of the list was proposed as an exercise in https://www.amazon.com/Thinking-Functionally-Haskell-Richard-Bird/dp/1107452643. During the Haskell course, I am trying to use Lean to formalize some informal (equational) proofs from the book. But clearly, not all of them are obvious to formalize...

#### Kevin Buzzard (Mar 09 2021 at 14:26):

I conjecture that most of them will not be too bad if you know some of the tricks. Would you like to post some #mwe examples of things which you think might not be obvious to formalise?

#### Alexandre Rademaker (Mar 09 2021 at 18:48):

Sure, I will share more examples. The problem is that once functions are optimized in a way or another, proofs became more difficult, as the example above. But for some properties such as map f . map g = map (f . g) we done, see https://github.com/emap-aa/demo-lean/blob/main/src/fp.lean#L60-L69

#### Alexandre Rademaker (Mar 23 2021 at 13:43):

One more case @Kevin Buzzard , the reverse (reverse xs) was fine.

theorem rev_rev_id {a : Type } (xs : list a) : (reverse ∘ reverse) xs  = id xs :=
begin
induction xs with b bs hi,
simp [reverse,append],

unfold comp, rw reverse,
unfold comp at hi,
rw rev_aux,
rw hi, simp,
end


But why I can't use the point-free Haskell style in the declaration?

theorem rev_rev_id : (reverse ∘ reverse)  = id := sorry


#### Eric Wieser (Mar 23 2021 at 13:45):

Because lean doesn't know what type of list you're stating it aabout

#### Eric Wieser (Mar 23 2021 at 13:45):

(reverse ∘ reverse) = (id : list a → list a) should work

#### Alexandre Rademaker (Mar 23 2021 at 13:46):

Hum, but Lean understood #check reverse ∘ reverse = id.

#### Eric Wieser (Mar 23 2021 at 13:46):

yes, but it put wildcards in. Those aren't allowed in lemma statements.

Thank you

#### Alexandre Rademaker (Mar 23 2021 at 13:48):

Turns out the proof is more complex anyway.

#### Yakov Pechersky (Mar 23 2021 at 14:43):

The proof should only have two more steps of

funext,
rw [function.comp_app, id.def],


and then your proof above.

Last updated: May 11 2021 at 21:10 UTC