TPIL 7.10.2.a

Stream: new members

[Eduardo Cavazos]

TPIL exercise 7.10.2.a says to prove the following:

Length (s ++ t) = Length s + Length t

(Note, List and Length and others below are capitalized so as not to clash with the ones provided by Lean. Their definitions are from earlier in chapter 7.)

Here's what I have so far:

example (s t : List α) : Length (s ++ t) = Length s + Length t :=

    List.rec_on s

        (show Length (Nil ++ t) = Length Nil + Length t, from
            calc
                Length (Nil ++ t)   = Length (t)    : by rw [nil_append]
                ...                 = 0 + Length(t) : eq.symm(zero_add (Length t)))

        (λ  (a : α)
            (a_1 : List α)
            (ih : Length (a_1 ++ t) = Length a_1 + Length t),

            show Length (a :: a_1 ++ t) = Length (a :: a_1) + Length t, from

                calc

                    Length (a :: a_1 ++ t)  = Length (a :: (a_1 ++ t))              : by rw [cons_append]
                    ...                     = Length [a] + Length (a_1 ++ t)        : length_cons
                    ...                     = Length [a] + (Length a_1 + Length t)  : by rw [ih]
                    ...                     = Length [a] + Length a_1 + Length t    : by rw add_assoc
                    ...                     = Length (a :: a_1) + Length t          : length_cons)

Note that length_cons that's referenced in the calc expression does not exist. Lean seem to be OK with the rest of the proof (there are no other red squiggles).

As you can see, I sketched out an approach that assumes the existence of something like this:

theorem length_cons (a : α) (s : List α) : Length (a :: s) = Length [a] + Length s

Is this a good approach? Should I continue on in proving length_cons and use that? Or would you recommend another approach?

Thanks for any suggestions!

[YH]

lemma ex1 {A : Type} {s t : list A} : length (s ++ t) = length s + length t :=
begin
induction s with x xs hs,
unfold length,
rw list.nil_append,
rw zero_add,
rw list.cons_append,
unfold length,
rw hs,
rwa add_assoc,
end

[Kevin Buzzard]

If you can state length_cons, sorry the proof, and get the example compiling modulo that one sorry, then sure you should continue! As YH points out, it can be much easier to write this stuff in tactic mode, although I suspect they are using standard facts about lists which you might not have proved for Lists.

[YH]

nil_append and cons_append are just proved by rfl in mathlib, should be easy for List too.

@[simp] lemma nil_append (s : list α) : [] ++ s = s :=
rfl

@[simp] lemma cons_append (x : α) (s t : list α) : (x::s) ++ t = x::(s ++ t) :=
rfl

[Kevin Buzzard]

You can #print prefix List to see all the functions which Lean made for you to use with List.

[Eduardo Cavazos]

If you can state length_cons, sorry the proof, and get the example compiling modulo that one sorry, then sure you should continue! As YH points out, it can be much easier to write this stuff in tactic mode, although I suspect they are using standard facts about lists which you might not have proved for Lists.

Good suggestion @Kevin Buzzard regarding using sorry with length_cons to see if the whole thing compiles. Thanks!

This version does indeed appear to compile:

theorem length_cons (a : α) (s : List α) : Length (a :: s) = Length [a] + Length s := sorry


example (s t : List α) : Length (s ++ t) = Length s + Length t :=

    List.rec_on s

        (show Length (Nil ++ t) = Length Nil + Length t, from
            calc
                Length (Nil ++ t)   = Length (t)    : by rw [nil_append]
                ...                 = 0 + Length(t) : eq.symm(zero_add (Length t)))

        (λ  (a : α)
            (a_1 : List α)
            (ih : Length (a_1 ++ t) = Length a_1 + Length t),

            show Length (a :: a_1 ++ t) = Length (a :: a_1) + Length t, from

                calc

                    Length (a :: a_1 ++ t)  = Length (a :: (a_1 ++ t))              : by rw [cons_append]
                    ...                     = Length [a] + Length (a_1 ++ t)        : by rw length_cons
                    ...                     = Length [a] + (Length a_1 + Length t)  : by rw [ih]
                    ...                     = Length [a] + Length a_1 + Length t    : by rw add_assoc
                    ...                     = Length (a :: a_1) + Length t          : by rw ←length_cons)

[Eduardo Cavazos]

Given that the above works in terms of an assumed length_cons, I decided to look into proving that.

This section of the chapter is emphasizing rec_on so I took an approach using that first:

-- length_cons

example (a : α) (s : List α) : Length (a :: s) = Length [a] + Length s :=

    List.rec_on s

        rfl

        (λ  (α_1 : α)
            (a_2 : List α)
            (ih : Length (a :: a_2) = Length [a] + Length a_2),

            show Length (a :: α_1 :: a_2) = Length [a] + Length (α_1 :: a_2), from

                _
        )

The helper that we end up with:

ih : Length (a :: a_2) = Length [a] + Length a_2

is very awkward and doesn't seem to help.

Moreover, the goal left to prove is:

Length (a :: α_1 :: a_2) = Length [a] + Length (α_1 :: a_2)

which is seemingly more complex than the original statement! :-)

So it seems like maybe this approach to length_cons is not the way to go. Perhaps I should not use rec_on? Any suggestions are welcome.

[Joe]

length_cons should be rfl, i.e. by definition.

[Joe]

import data.list

namespace list

variables {α : Type*}

lemma length_cons' (a : α) (l : list α) : length (a :: l) = length l + 1 := rfl

end list

[Joe]

But I'm not sure of your definition of Length.

[Joe]

By the way, it seems that length_append can be solved by simp.

import data.list

namespace list

variables {α : Type*}

lemma length_cons' (a : α) (l : list α) : length (a :: l) = length l + 1 := rfl

lemma length_append' (s t : list α) : length (s ++ t) = length s + length t :=
begin
  induction s,
  { squeeze_simp },
  { squeeze_simp }
end

end list

You can look into squeeze_simp to see what lemmas are used.

[Joe]

Here is what it looks like if you do it by hand.

import data.list
import tactic.ring

namespace list

variables {α : Type*}

lemma length_cons' (a : α) (l : list α) : length (a :: l) = length l + 1 := rfl

lemma length_append' (s t : list α) : length (s ++ t) = length s + length t :=
begin
  induction s,
  { rw [nil_append, length], ring },
  { rw [cons_append, length, length, length_append], ring }
end

end list

[Eduardo Cavazos]

Thanks for your suggestions @Joe!

But I'm not sure of your definition of Length.

Here's what I'm using:

def Length : Π {α : Type u}, List α → ℕ :=
    (λ α ls,
        List.rec_on ls
            0
            (λ a ls n,
                n + 1))

[Eduardo Cavazos]

This appears to work:

theorem length_cons' (a : α) (s : List α) : Length (a :: s) = Length s + Length [a] := rfl

theorem length_cons (a : α) (s : List α) : Length (a :: s) = Length [a] + Length s :=

    calc

        Length (a :: s) = Length s + Length [a]     : by rw length_cons'
        ...             = Length [a] + Length s     : by rw add_comm


theorem length_append (s t : List α) : Length (s ++ t) = Length s + Length t :=

    List.rec_on s

        (show Length (Nil ++ t) = Length Nil + Length t, from
            calc
                Length (Nil ++ t)   = Length (t)    : by rw [nil_append]
                ...                 = 0 + Length(t) : eq.symm(zero_add (Length t)))

        (λ  (a : α)
            (a_1 : List α)
            (ih : Length (a_1 ++ t) = Length a_1 + Length t),

            show Length (a :: a_1 ++ t) = Length (a :: a_1) + Length t, from

                calc

                    Length (a :: a_1 ++ t)  = Length (a :: (a_1 ++ t))              : by rw [cons_append]
                    ...                     = Length [a] + Length (a_1 ++ t)        : by rw length_cons
                    ...                     = Length [a] + (Length a_1 + Length t)  : by rw [ih]
                    ...                     = Length [a] + Length a_1 + Length t    : by rw add_assoc
                    ...                     = Length (a :: a_1) + Length t          : by rw ←length_cons)

[Eduardo Cavazos]

@Joe ,

This comment from you was key:

length_cons should be rfl, i.e. by definition.

When I tried to use rfl, I noticed that it didn't work:

theorem length_cons (a : α) (s : List α) : Length (a :: s) = Length [a] + Length s

however, swapping the arguments to + causes it to work:

theorem length_cons' (a : α) (s : List α) : Length (a :: s) = Length s + Length [a] := rfl

Thank you so much for your help and suggestions!

[Eduardo Cavazos]

@YH , thanks for your tactics based solution!

I wanted to try to use rec_on as that was what was emphasized in the section of the chapter. This is the approach demonstrated above.

[Joe]

You're welcome.