component-wise list addition

Stream: new members

[Charlie Conneen]

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]

You should probably define list_add in terms of list.zip_with, and you'll already have relevant lemmas available.

[Scott Morrison]

e.g. src#list.length_zip

[Scott Morrison]

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]

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]

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]

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]

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

[Scott Morrison]

Post something you've tried!

[Charlie Conneen]

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]

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]

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]

You'll really find it easier if you prove a lemma about (list_add x y).length, rather than one about R3.

[Scott Morrison]

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

[Scott Morrison]

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]

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]

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

[Mario Carneiro]

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]

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]

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]

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

[Mario Carneiro]

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]

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]

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]

You can replace the first injection by have ha := nat.succ.inj ha, for example

[Mario Carneiro]

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

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]

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