proving properties of recursive functions with let/match

Stream: general

[Alexandre Rademaker]

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]

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]

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]

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]

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

[Eric Wieser]

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

[Alexandre Rademaker]

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

[Eric Wieser]

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

[Alexandre Rademaker]

Thank you

[Alexandre Rademaker]

Turns out the proof is more complex anyway.

[Yakov Pechersky]

The proof should only have two more steps of

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

and then your proof above.