# Zulip Chat Archive

## 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 zero_add, rw list.cons_append, unfold length, rw hs, rwa add_assoc, 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 `list`

s which you might not have proved for `List`

s.

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

s which you might not have proved for`List`

s.

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

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 (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: Dec 20 2023 at 11:08 UTC