issue with multiple list induction in proofs

Stream: new members

[Charlie Conneen]

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]

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

[Yakov Pechersky]

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]

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]

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

[Charlie Conneen]

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]

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]

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