rewrite failing with definition

Stream: general

[Alexandre Rademaker]

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]

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]

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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]

I remembered Zulip does spoilers now :-)

import tactic

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)

example : splitAt 2 [1,2,3,4] = ([1,2],[3,4]) :=
begin
  simp [splitAt],
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 IH generalizing n,
  { induction n with m hm;
    simp [splitAt] },
  { induction n with m hm,
    { simp [splitAt] },
    { simp [splitAt, IH, hm] } }
end