Isabelle: this lemma about polynomials is only provable for idoms

Question

In short: I have only a backgroung in computer science and not mathematics. I have proven a lemma in Isabelle for idoms and concluded that it cannot be proven for polynomials of rings 'a::comm_ring_1 poly. But I am not fully sure.

In the Isabelle library, there is the following lemma:

Polynomial.coeff_mult_degree_sum:
    coeff (p * q) (degree p + degree q) = coeff p (degree p) * coeff q (degree q)

(where (p∷?'a∷comm_semiring_0 poly) and (q∷?'a∷comm_semiring_0 poly); the lemma is from HOL/Library/Polynomial.thy)

I have proven the following lemma in Isabelle (product/sum of polynomials):

lemma coeff_mult_setprod_setsum:
fixes S :: "'b::idom poly set"
shows "finite S ⟹ coeff (setprod (λx. x) S) (setsum (λx. degree x) S) = setprod (λ x. coeff x (degree x)) S"
by (induct rule: finite_induct, simp, simp_all add: coeff_setprod_setsum_induct_step)  

My question:
Is it true that the above lemma requires idoms (i.e., without zero divisors) and cannot be proven for S :: "'a::comm_ring_1 poly set"?

..
..
Here is the full proof:

(* tested with Isabelle2013-2  *)
theory Notepad
imports
  Main
  "~~/src/HOL/Library/Polynomial"
begin

lemma degree_product_setsum:
  fixes S :: "('a::comm_ring_1) poly set"
  assumes "finite S"
  shows "degree (∏S) ≤ setsum degree S" 
using `finite S`
proof-
  (* Sledgehammer proof *)
  have th1: "⋀x⇩1 x⇩2 x⇩3. degree ((x⇩1∷'a poly) * x⇩2) ≤ degree x⇩1 + x⇩3 ∨ ¬ degree x⇩2 ≤ x⇩3" 
  by (metis add_le_cancel_right degree_mult_le dual_order.trans nat_add_commute) 
  show ?thesis using `finite S`
    apply(induct)
    apply(simp)
    by (metis (full_types) th1 setprod.insert setsum.insert)
qed

lemma coeff_setprod_setsum_induct_step:
fixes x :: "'b::idom poly" and   F :: "'b::idom poly set"
assumes a1: "finite F"
and a2: "x ∉ F"
and a3: "coeff (∏F) (setsum degree F) = (∏x∷'b poly∈F. coeff x (degree x))"
shows "coeff (x * ∏F) (degree x + setsum degree F) = coeff x (degree x) * (∏x∈F. coeff x (degree x))"
proof-

from coeff_mult_degree_sum[of x "∏F"]
have 1: "coeff (x * ∏F) (degree x + degree (∏F)) = coeff x (degree x) * coeff (∏F) (degree (∏F))" by fast

from a1
have 3: "degree (∏F) ≤ setsum degree F" using degree_product_setsum by fast

(** BEWARE SLEDGEHAMMER PROOF! (don't care at the moment about it) *)
show ?thesis
proof -
  have "(∏R∈F. coeff R (degree R)) = 0 ∨ setsum degree F ≤ degree (∏F)"
    by (metis a3 le_degree)
  hence f1: "setsum degree F = degree (∏F) ∨ (∏R∈F. coeff R (degree R)) = 0"
    by (metis "3" le_antisym)
  have f2: "setsum degree F = degree (∏F) ∨ ¬ setsum degree F ≤ degree (∏F)"
    by (metis "3" le_antisym)
  hence "coeff (∏F) (degree (∏F)) = (∏R∈F. coeff R (degree R)) ⟶ coeff x (degree x) * (∏R∈F. coeff R (degree R)) = coeff (x * ∏F) (degree (x * ∏F))"
  by (metis (full_types) "1" degree_mult_eq leading_coeff_0_iff mult_eq_0_iff)
  moreover
  { assume "coeff (∏F) (degree (∏F)) ≠ (∏R∈F. coeff R (degree R))"
    hence "setsum degree F ≠ degree (∏F)"
      using a3 by force }
  moreover
  { assume "coeff x (degree x) * (∏R∈F. coeff R (degree R)) = coeff (x * ∏F) (degree (x * ∏F))"
    hence "setsum degree F = degree (∏F) ⟶ coeff (x * ∏F) (degree x + setsum degree F) = coeff x (degree x) * (∏R∈F. coeff R (degree R))"
by (metis (lifting, no_types) "1" calculation(2))}
  ultimately have "setsum degree F = degree (∏F) ⟶ coeff (x * ∏F) (degree x + setsum degree F) = coeff x (degree x) * (∏R∈F. coeff R (degree R))"
    by fastforce
  hence "setsum degree F ≠ degree (∏F) ∧ ¬ degree x + setsum degree F ≤ degree x + degree (∏F) ∨ coeff (x * ∏F) (degree x + setsum degree F) = coeff x (degree x) * (∏R∈F. coeff R (degree R))"
    using f2 add_le_cancel_left by blast
  hence "setsum degree F ≠ degree (∏F) ∧ coeff (x * ∏F) (degree x + setsum degree F) = 0 ∨ coeff (x * ∏F) (degree x + setsum degree F) = coeff x (degree x) * (∏R∈F. coeff R (degree R))"
by (metis (full_types) coeff_0 degree_mult_eq le_degree mult_eq_0_iff)
  thus "coeff (x * ∏F) (degree x + setsum degree F) = coeff x (degree x) * (∏x∈F. coeff x (degree x))"
    using f1 by force
qed
qed

lemma coeff_setprod_setsum:
fixes S :: "'b::idom poly set" (* lemma is not true for S :: "'a::comm_ring_1 poly set"*)
shows "finite S ⟹ coeff (setprod (λx. x) S) (setsum (λx. degree x) S) = setprod (λ x. coeff x (degree x)) S"
by (induct rule: finite_induct, simp, simp_all add: coeff_setprod_setsum_induct_step)

Looking at three polynomials, the problem is visible:

notepad
begin
 fix p q r :: "'a::comm_ring_1 poly"
 have "coeff (p * q * r) (degree (p * q) + degree r) = coeff (p * q) (degree (p * q)) * coeff r (degree r)"
using Polynomial.coeff_mult_degree_sum[of "p * q" r]  by fast
end

However, it is impossible to imply that degree (p * q) is equal to degree p + degree q for the type 'a::comm_ring_1 poly.

Consider this lemma that requires idoms:

Polynomial.degree_mult_eq: (?p∷?'a∷idom poly) ≠ (0∷?'a∷idom poly) ⟹ (?q∷?'a∷idom poly) ≠ (0∷?'a∷idom poly) ⟹ 
degree (?p * ?q) = degree ?p + degree ?q

..
..
..

Solution from Brian Huffman

lemma degree_setprod_le: "degree (∏i∈S. f i) ≤ (∑i∈S. degree (f i))"
apply(cases "finite S", simp_all, induct rule: finite_induct, simp_all)
by (metis (lifting) degree_mult_le dual_order.trans nat_add_left_cancel_le)

lemma coeff_mult_sum: "degree p ≤ m ⟹ degree q ≤ n ⟹ coeff (p * q) (m + n) = coeff p m * coeff q n"
apply(cases "degree p = m ∧ degree q = n")
apply(insert coeff_mult_degree_sum[of p q], simp) [1]
apply(cases "degree p < m", cases "degree q < n")
by(insert coeff_eq_0[of q n] coeff_eq_0[of p m] degree_mult_le[of p q] coeff_eq_0[of "p*q" "m + n"], simp_all)

lemma coeff_mult_setprod_setsum:
"coeff (setprod (λx. x) S) (setsum (λx. degree x) S) = setprod (λ x. coeff x (degree x)) S"
by(cases "finite S", induct rule: finite_induct, simp_all add: coeff_mult_sum degree_setprod_le)

Answer 1

Yes, your lemma coeff_mult_setprod_setsum is in fact provable for arbitrary comm_ring_1 types. The reason it works without the idom class constraint is that you are never actually computing the degree of the result of a polynomial multiplication, you only are using the degrees of the factors.

I was able to prove this by induction on S using the following two lemmas:

lemma degree_setprod_le: "degree (∏i∈S. f i) ≤ (∑i∈S. degree (f i))" Proof is by cases on whether S is finite, followed by induction on S, and using library lemma degree_mult_le to solve the inductive step.

lemma coeff_mult_sum: "degree p ≤ m ⟹ degree q ≤ n ⟹ coeff (p * q) (m + n) = coeff p m * coeff q n" Proof is by case analysis on whether degree p < m or degree p = m (similarly for q and n). In the less-than cases, library lemma coeff_eq_0 shows that both sides are zero; the final case follows from library lemma coeff_mult_degree_sum.

Answer 2

The problem is, quite simply, that if you don't have an integral domain, coefficients might become zero when multiplying two polynomials, in fact, even the entire polynomial can become zero. For example, consider the commutative ring ℤ/4ℤ, i.e. integers modulo 4. Then the polynomial 2X has degree 1, but 2X · 2X = 4X² = 0 has degree -∞ (or 0, by Isabelle convention).

You need the fact that there are no zero divisors for something like this.

On a related note: it is called “idom”, for “integral domain”, not “ideom”.