Zulip Chat Archive

Stream: general

Topic: rewrite failing with definition


Alexandre Rademaker (Mar 04 2021 at 20:42):

I am trying to prove that a simple definition of a function over lists is doing the right thing.

import tactic
import data.list
import data.real.basic
import init.function
open function

def splitAt {a : Type} :   (list a)  (list a × list a)
 |                   0 xs := ([], xs)
 |                   _ [] := ([], [])
 | (nat.succ n) (x :: xs) :=  match splitAt n xs with (ys, zs) := (x :: ys, zs)  end

example : splitAt 2 [1,2,3,4] = ([1,2],[3,4]) :=
begin
 rw splitAt,
 rw splitAt,
 rw splitAt,
 rw splitAt._match_1,
 rw splitAt._match_1,
end

example (a : Type) (n : ) (xs : list a) :
 (λ x, (prod.fst x) ++ (prod.snd x) == xs) (splitAt n xs) :=
begin
 induction xs with d hd,
 simp,
 rw splitAt,    --  <- ERROR
end
  1. why unfold does not work in the proofs?
  2. why the rw is working in the first proof, but in the second it doesn't work.
  3. The definition looks ugly compared to the original Haskell code, is it possible to simplify it?

Kevin Buzzard (Mar 04 2021 at 21:22):

If you look at the output of #print prefix splitAt you will see that there are four equation lemmas -- 0 [], 0 (a :: L), (succ n) [] and (succ n) (a :: L). So you need to do cases n and then the rewrite will work.

Alexandre Rademaker (Mar 04 2021 at 21:28):

Thank you, I have never used the #print prefix before. But why the first proof works without the cases?

Kevin Buzzard (Mar 05 2021 at 07:49):

Here's my effort to tidy up:

def splitAt {a : Type} :   (list a)  (list a × list a)
 |              0 xs := ([], xs)
 |              _ [] := ([], [])
 | (n + 1) (x :: xs) :=  let (ys, zs) := splitAt n xs in (x :: ys, zs)

example : splitAt 2 [1,2,3,4] = ([1,2],[3,4]) :=
begin
  simp [splitAt],
end

Note: you don't need any imports. You never need import init.function -- this is not in mathlib, this is core Lean so already imported.

Kevin Buzzard (Mar 05 2021 at 08:03):

As for ==, I think that you think that == means something different to what Lean means by it. It's heterogeneous equality, which is used to compare elements of different types in certain circumstances, and is not needed in situations like this.

Patrick Massot (Mar 05 2021 at 08:10):

Technically, not all of core Lean is imported automatically, only what is in init, but this doesn't change anything here.

Kevin Buzzard (Mar 05 2021 at 08:15):

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

def splitAt {a : Type} :   (list a)  (list a × list a)
 |              0 xs := ([], xs)
 |              _ [] := ([], [])
 | (n + 1) (x :: xs) := (x :: (splitAt n xs).1, (splitAt n xs).2)

Then the simplifier can prove

example (a : Type) (n : ) (xs : list a) :
 (λ x, (prod.fst x) ++ (prod.snd x) = xs) (splitAt n xs) :=

without too much trouble (I can post my proof if you want, but I don't know if it's a spoiler)

Kevin Buzzard (Mar 05 2021 at 08:18):

I remembered Zulip does spoilers now :-)


Last updated: Dec 20 2023 at 11:08 UTC