Zulip Chat Archive

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 :=
 induction xs with b bs hi,
 simp [reverse,append],

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

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.

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

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

rw [function.comp_app, id.def],

and then your proof above.

Last updated: Dec 20 2023 at 11:08 UTC