## Stream: new members

### Topic: TPIL 7.10.2.a

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

#### 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 list.cons_append,
unfold length,
rw hs,
end


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

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


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

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


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

#### Joe (Dec 17 2019 at 02:45):

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

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


#### Joe (Dec 17 2019 at 02:47):

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

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

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


#### Eduardo Cavazos (Dec 17 2019 at 03:22):

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


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

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

#### Joe (Dec 17 2019 at 04:51):

You're welcome.

Last updated: May 15 2021 at 00:39 UTC