Zulip Chat Archive

Stream: general

Topic: proving properties of recursive functions with let/match


view this post on Zulip 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...

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Mar 23 2021 at 13:45):

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

view this post on Zulip Eric Wieser (Mar 23 2021 at 13:45):

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

view this post on Zulip Alexandre Rademaker (Mar 23 2021 at 13:46):

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

view this post on Zulip Eric Wieser (Mar 23 2021 at 13:46):

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

view this post on Zulip Alexandre Rademaker (Mar 23 2021 at 13:48):

Thank you

view this post on Zulip Alexandre Rademaker (Mar 23 2021 at 13:48):

Turns out the proof is more complex anyway.

view this post on Zulip 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