## Stream: new members

### Topic: issue with multiple list induction in proofs

#### Charlie Conneen (Dec 22 2020 at 18:53):

I have defined a special kind of list addition, ladd, which adds two lists with entries in a ring R pairwise (starting from the head of the list), and cuts off remaining elements at the end if one of the lists is longer than the other. In proving that this operation is commutative, I've run into issues. I don't know how to perform induction on multiple objects at once during a proof, and inducting on them separately results in the following:

-- MWE
import algebra.ring

variables {R : Type*} [ring R]

-- useful lemmata
lemma add_nil_left (l : list R) : ladd ([] : list R) l = [] := rfl

lemma add_nil_right (l : list R) : ladd l ([] : list R) = [] := by cases l; refl

lemma ladd_comm : ∀ x y : list R, ladd x y = ladd y x :=
begin
intros,
induction x, -- doing induction  one at a time
induction y,
change (x_hd + y_hd) :: (ladd x_tl y_tl) = (y_hd + x_hd) :: (ladd y_tl x_tl),
refine congr rfl _,
sorry -- iterated induction doesn't get to the right goal
end


The end tactic state gives us y_ih, and implication with the current goal as the hypothesis, which seems to be useless, and the current goal is the same as the statement of the theorem, just with the heads of the lists removed. The same problem occurs when trying to prove associativity as well. I'm not sure how to progress here.

#### Yakov Pechersky (Dec 22 2020 at 18:59):

You might like the lemmas and proofs in recent PR #5455

#### Yakov Pechersky (Dec 22 2020 at 19:02):

Another crucial element is induction ... generalizing ...:

-- MWE
import algebra.ring

variables {R : Type*} [ring R]

-- useful lemmata
lemma add_nil_left (l : list R) : ladd ([] : list R) l = [] := rfl

lemma add_nil_right (l : list R) : ladd l ([] : list R) = [] := by cases l; refl

@[simp] theorem zip_with_cons_cons {α β γ} (f : α → β → γ) (a : α) (b : β) (l₁ : list α) (l₂ : list β) :
list.zip_with f (a :: l₁) (b :: l₂) = f a b :: list.zip_with f l₁ l₂ := rfl

lemma ladd_comm : ∀ x y : list R, ladd x y = ladd y x :=
begin
intros l l',
induction l with hd tl hl generalizing l', -- doing induction, have to generalize l'
{ cases l' with hd' tl',
rw [zip_with_cons_cons, zip_with_cons_cons, hl, add_comm] }
end


#### Yakov Pechersky (Dec 22 2020 at 19:03):

With a simp:

-- MWE
import algebra.ring

variables {R : Type*} [ring R]

-- useful lemmata
lemma add_nil_left (l : list R) : ladd ([] : list R) l = [] := rfl

lemma add_nil_right (l : list R) : ladd l ([] : list R) = [] := by cases l; refl

@[simp] theorem zip_with_cons_cons {α β γ} (f : α → β → γ) (a : α) (b : β) (l₁ : list α) (l₂ : list β) :
list.zip_with f (a :: l₁) (b :: l₂) = f a b :: list.zip_with f l₁ l₂ := rfl

lemma ladd_comm : ∀ x y : list R, ladd x y = ladd y x :=
begin
intros l l',
induction l with hd tl hl generalizing l', -- doing induction, have to generalize l'
{ cases l' with hd' tl',
end


#### Yakov Pechersky (Dec 22 2020 at 19:04):

A good lemma to prove (and possibly PR) is that this is true for any commutative function.

#### Charlie Conneen (Dec 22 2020 at 19:08):

Right, it did seem as though the list library was a little lackluster. Thanks for the help, I didn't know about the generalizing trick.

#### Yakov Pechersky (Dec 22 2020 at 19:10):

That is:

-- MWE
import algebra.ring

variables {R : Type*} [ring R]

lemma to_prove {α : Type*} (f : α → α → α) [is_commutative α f] : commutative (list.zip_with f) :=
sorry


And from looking at the definitions, you might notice that your ladd is too constrained, it could work for something more general than a ring