# Zulip Chat Archive

## Stream: new members

### Topic: component-wise list addition

#### Charlie Conneen (May 30 2020 at 23:35):

I've implemented addition in lists as adding each index together. End goal is to create component-wise addition in the `vector`

type, which depends on lists. Issue is, the list type allows for arbitrary length, and for some reason I'm having real trouble showing that the sum of two lists of the same length is another list of that same length. I can't seem to split into cases on the definition of `list_add`

.

MWE:

```
abbreviation n_tuple (K : Type*) [field K] (n : ℕ) := vector K n
abbreviation R3 := n_tuple ℝ 3
def list_add (α : Type*) [has_add α] : list α → list α → list α
| [] l := l
| l [] := l
| (a :: as) (b :: bs) := (a+b) :: list_add as bs
instance (α : Type*) [has_add α] : has_add (list α) := ⟨list_add α⟩
lemma sum_r3 (x y : R3) : list.length (x.1 + y.1) = 3 := sorry
def vec_add : R3 → R3 → R3 := λ x y, ⟨x.1 + y.1, sum_r3 x y⟩
```

Any ideas on how to prove `sum_r3`

?

#### Scott Morrison (May 31 2020 at 00:30):

You should probably define `list_add`

in terms of `list.zip_with`

, and you'll already have relevant lemmas available.

#### Scott Morrison (May 31 2020 at 00:31):

e.g. src#list.length_zip

#### Scott Morrison (May 31 2020 at 00:32):

But if you want to do it yourself, follow the proof of list.length_zip, i.e. prove the theorem using the same pattern matching as you used to define the function.

#### Charlie Conneen (May 31 2020 at 00:43):

Aha! I see. Instead of doing cases within tactic state, do cases outside. I had compartmentalized proofs of theorems as either being exact statements or using tactic state, and that was leading me astray.

#### Charlie Conneen (May 31 2020 at 00:44):

Thank you very much for pointing me towards this. Relying on `zip_with`

will be helpful, but I'll assuredly still prove this directly just to verify my understanding.

#### Scott Morrison (May 31 2020 at 00:46):

You can equally well do cases (better, induction) inside the tactic state. That's actually what I tend to do. The problem is just that you need to do induction, so it's easier to prove the theorem about general length lists, and then specialise to 3, rather than try to prove something about length 3.

#### Charlie Conneen (May 31 2020 at 00:48):

How exactly would you apply cases in this example? I attempted this, and no matter my fiddling I was still getting errors

#### Scott Morrison (May 31 2020 at 01:02):

Post something you've tried!

#### Charlie Conneen (May 31 2020 at 01:21):

My issue is, I would like to do cases on `list_add`

, and break it down that way. But that throws errors. All I can seem to do is get cases on hypotheses:

```
lemma sum_r3 (x y : R3) : list.length (x.1 + y.1) = 3 :=
begin
cases x,
cases y,
simp,
cases x_val,
cases y_val,
repeat{sorry},
end
```

but this isn't what I want. I want to mimic the proof using pipes in the theorem `length_zip`

, which you linked. I'm not sure how to do this, because `cases list_add`

doesn't exactly work.

#### Charlie Conneen (May 31 2020 at 01:23):

Obviously I have a solution, which is to scrap this and just define `list_add`

in terms of `list.zip_with`

, but I would still like to know how to translate proofs that go through each constructor to proofs in tactic state

#### Mario Carneiro (May 31 2020 at 01:27):

You have to case on the arguments in the same way as they are cased in `list_add`

, then you can rewrite with the definitional lemmas

#### Scott Morrison (May 31 2020 at 01:29):

You'll really find it easier if you prove a lemma about `(list_add x y).length`

, rather than one about `R3`

.

#### Scott Morrison (May 31 2020 at 01:30):

The point is you need to do induction on the lists themselves, so the length is going to be varying.

#### Scott Morrison (May 31 2020 at 01:30):

Does that make sense? Try writing at least the statement about `list_add`

. Then proceed by calling `induction ?`

, on whatever variable you're doing the pattern matching on in `list_add`

.

#### Mario Carneiro (May 31 2020 at 01:35):

```
lemma sum_r3 (x y : R3) : list.length (x.1 + y.1) = 3 :=
begin
cases x with as ha,
cases y with bs hb,
change (list_add _ as bs).length = 3,
generalize_hyp : 3 = n at ha hb ⊢,
induction as with a as IH generalizing n bs;
cases bs with b bs;
rw list_add,
iterate 3 { assumption },
cases n, {cases ha},
injection ha with ha, injection hb with hb,
cases IH _ _ hb ha, refl
end
```

#### Mario Carneiro (May 31 2020 at 01:35):

Another way to prove this uses cases 3 times, rather than generalizing 3 to n and using induction

#### Mario Carneiro (May 31 2020 at 01:36):

But it is definitely easiest to use the equation compiler to do this:

```
lemma sum_r3 : ∀ (x y : R3), list.length (x.1 + y.1) = 3
| ⟨[x₁, x₂, x₃], _⟩ ⟨[y₁, y₂, y₃], _⟩ := rfl
```

#### Charlie Conneen (May 31 2020 at 01:46):

I see. I'm baffled, to be honest. The proof makes sense, I've just never seen `generalize_hyp`

or `injection`

used before, so I can't have thought of that. It's a little unclear to me how rfl proves the lemma in the second example. Does it go through the recursive computation and see that the output is a list of length 3?

#### Mario Carneiro (May 31 2020 at 01:52):

lean has the notion of definitional equality, which involves computations "by definition", along the equations that define the function. In this case it works because if you reduce `list_add [x₁, x₂, x₃] [y₁, y₂, y₃]`

you get `[x₁ + y₁, x₂ + y₂, x₃ + y₃]`

, which is manifestly a list of length 3

#### Mario Carneiro (May 31 2020 at 01:53):

It's kind of like symbolic execution, if you are familiar with that

#### Mario Carneiro (May 31 2020 at 01:54):

`generalize_hyp`

is the mathlib version of `generalize`

. There are more low tech ways of doing the same thing but the gist of it is we want to prove the theorem for all `3`

#### Mario Carneiro (May 31 2020 at 01:55):

this is actually important for the induction proof because `n`

changes in the inductive hypothesis, so if the inductive hypothesis only talked about lists of length 3 it would be useless

#### Mario Carneiro (May 31 2020 at 01:56):

`injection`

here is just applying injectivity of `nat.succ`

, again using a bit of definitional equality to reduce `length (a :: as)`

to `nat.succ (length as)`

#### Mario Carneiro (May 31 2020 at 01:56):

You can replace the first `injection`

by `have ha := nat.succ.inj ha`

, for example

#### Mario Carneiro (May 31 2020 at 01:58):

(I also don't expect you to be able to come up with the proof, I am showing it so that you can learn about some tools you may not have seen before)

#### Charlie Conneen (May 31 2020 at 01:58):

Right, that makes sense. The intuition is clear, and I see now what I need to practice to be more familiar with not only converting/simplifying proofs, but also familiarizing myself with certain tactics I haven't yet come across. Thank you!

#### Sam Lichtenstein (May 31 2020 at 02:20):

I think a cool way to solve your underlying question (defining component-wise addition on `R3`

) is to show that `vector.of_fn`

defines a bijection from functions `(fin 3) → ℝ`

to `vector ℝ 3`

. If you define its inverse `to_fn`

, you can use the fact that component-wise addition is already defined on `(fin 3) → ℝ`

to get:

```
instance : has_add R3 := { add := λ (v w), vector.of_fn ((to_fn v) + (to_fn w)) }
```

Then the proof that this is in fact component-wise addition is really short!

```
lemma component_wise (x y z x' y' z' : ℝ) :
x :: y :: z :: vector.nil + x' :: y' :: z' :: vector.nil =
(x + x') :: (y + y') :: (z + z') :: vector.nil := rfl
```

Last updated: May 13 2021 at 20:13 UTC