## Stream: new members

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

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: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_addin 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;
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