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

-- list addition
def ladd : list R → list R → list R := list.zip_with (has_add.add)

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

-- WTS ladd is commutative
lemma ladd_comm : ∀ x y : list R, ladd x y = ladd y x :=
begin
intros,
induction x, -- doing induction  one at a time
rw [add_nil_left, add_nil_right],
induction y,
rw [add_nil_right, add_nil_left],
change (x_hd + y_hd) :: (ladd x_tl y_tl) = (y_hd + x_hd) :: (ladd y_tl x_tl),
rw add_comm,
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]

-- list addition
def ladd : list R → list R → list R := list.zip_with (has_add.add)

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

-- WTS ladd is commutative
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'
{ rw [add_nil_left, add_nil_right] },
{ cases l' with hd' tl',
{ rw [add_nil_left, add_nil_right] },
rw ladd at hl ⊢,
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]

-- list addition
def ladd : list R → list R → list R := list.zip_with (has_add.add)

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

-- WTS ladd is commutative
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'
{ rw [add_nil_left, add_nil_right] },
{ cases l' with hd' tl',
{ rw [add_nil_left, add_nil_right] },
simpa [ladd, add_comm] using hl 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]

-- list addition
def ladd : list R → list R → list R := list.zip_with (has_add.add)

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

-- WTS ladd is commutative
lemma ladd_comm : ∀ x y : list R, ladd x y = ladd y x :=
begin
intros l l',
rw [ladd, to_prove]
end


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

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

Last updated: May 13 2021 at 17:42 UTC