Zulip Chat Archive

Stream: new members

Topic: TPIL 7.10.2.a


view this post on Zulip Eduardo Cavazos (Dec 16 2019 at 05:28):

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!

view this post on Zulip YH (Dec 16 2019 at 06:48):

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

view this post on Zulip Kevin Buzzard (Dec 16 2019 at 08:50):

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.

view this post on Zulip YH (Dec 16 2019 at 16:24):

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

view this post on Zulip Kevin Buzzard (Dec 16 2019 at 16:26):

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

view this post on Zulip Eduardo Cavazos (Dec 16 2019 at 17:39):

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)

view this post on Zulip Eduardo Cavazos (Dec 17 2019 at 02:24):

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.

view this post on Zulip Joe (Dec 17 2019 at 02:45):

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

view this post on Zulip Joe (Dec 17 2019 at 02:46):

import data.list

namespace list

variables {α : Type*}

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

end list

view this post on Zulip Joe (Dec 17 2019 at 02:47):

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

view this post on Zulip Joe (Dec 17 2019 at 02:50):

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.

view this post on Zulip Joe (Dec 17 2019 at 02:53):

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

view this post on Zulip Eduardo Cavazos (Dec 17 2019 at 03:22):

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))

view this post on Zulip Eduardo Cavazos (Dec 17 2019 at 03:32):

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)

view this post on Zulip Eduardo Cavazos (Dec 17 2019 at 04:43):

@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!

view this post on Zulip Eduardo Cavazos (Dec 17 2019 at 04:51):

@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.

view this post on Zulip Joe (Dec 17 2019 at 04:51):

You're welcome.


Last updated: May 15 2021 at 00:39 UTC