0

我正在研究一个引理，该引理表明，n如果每个单项式的指数小于或等于 ，则单项式之和的次数总是小于或等于n。

lemma degree_poly_smaller:
  fixes a :: "('a::comm_ring_1 poly)" and n::nat
  shows "degree (∑x∷nat | x ≤ n . monom (coeff a x) x) ≤ n"
sorry

到目前为止，我要做的如下（请注意，我是 Isabelle 的初学者）：

lemma degree_smaller:
  fixes a :: "('a::comm_ring_1 poly)" and n::nat
  shows "degree (∑x∷nat | x ≤ n . monom (coeff a x) x) ≤ n"
proof-

 have th01: "⋀k. k ≤ n ⟹ 
             degree (setsum (λ x . monom (coeff a x) k) {x∷nat. x ≤ n})  ≤ n" 
                    by (metis degree_monom_le monom_setsum order_trans)

 have min_lemma1: "k∈{x∷nat. x ≤ n} ⟹ k ≤ n" by simp

 from this th01 have th02: 
     "⋀k. k∈{x∷nat. x ≤ n} ⟹ 
     degree (setsum (λ x . monom (coeff a x) k) {x∷nat. x ≤ n})  ≤ n" 
                                             by (metis mem_Collect_eq)

 have min_lemma2: "(SOME y . y ≤ n) ≤ n" by (metis (full_types) le0 some_eq_ex)

 from this have th03: 
     "degree (∑x∷nat | x ≤ n . monom (coeff a x) (SOME y . y ≤ n)) ≤ n" 
                                                         by (metis th01)

 from min_lemma1 min_lemma2 have min_lemma3: 
     "(SOME y . y∈{x∷nat. x ≤ n}) ≤ n" by (metis (full_types) mem_Collect_eq some_eq_ex)

 from this th01 th02 th03 have th04: 
     "degree (∑x∷nat | x ≤ n . monom (coeff a x) (SOME y . y∈{x∷nat. x ≤ n}) ) ≤ n" 
                                                                      by presburger

这就是问题所在，我不明白为什么以下引理不足以完成证明。特别是，我希望最后一部分（抱歉的地方）足够简单，让大锤找到证据： 

 from this th01 th02 th03 th04  have th05: 
 "degree 
  (setsum (λ i . monom (coeff a i) (SOME y . y∈{x∷nat. x ≤ n})) {x∷nat. x ≤ n})
   ≤ n"
        by linarith

  (* how can I prove this last step ? *)
  from this have 
    "degree (setsum (λ i . monom (coeff a i) i) {x∷nat. x ≤ n}) ≤ n" sorry 

  from this show ?thesis by auto
qed

.
布赖恩霍夫曼出色回答的解决方案：
。 

lemma degree_setsum_smaller:
  "finite A ⟹ ∀x∈A. degree (f x) ≤ n ⟹ degree (∑x∈A. f x) ≤ n"
apply(induct rule: finite_induct)
apply(auto)
by (metis degree_add_le)

lemma finiteSetSmallerThanNumber: 
   "finite {x∷nat. x ≤ n}" 
by (metis finite_Collect_le_nat)

lemma degree_smaller:
  fixes a :: "('a::comm_ring_1 poly)" and n::nat
  shows "degree (∑x∷nat | x ≤ n . monom (coeff a x) x) ≤ n"
apply (rule degree_setsum_smaller)
apply(simp add: finiteSetSmallerThanNumber)
by (metis degree_0 degree_monom_eq le0 mem_Collect_eq monom_eq_0_iff) (* from sledgehammer *)
4

2 回答 2

3

最后一步不遵循您的th05. 问题是您似乎想(SOME y. y∈{x∷nat. x ≤ n})与绑定变量统一i。然而，在 HOL(SOME y. y∈{x∷nat. x ≤ n})中只有一个值，它只依赖于n而不依赖于i。此外，您无法选择值；使用SOME的定理与具有普遍量化变量的定理不同。

我的建议是完全避免使用SOME，而是首先尝试证明您的定理的推广：

lemma degree_setsum_smaller:
  "finite A ⟹ ∀x∈A. degree (f x) ≤ n ⟹ degree (∑x∈A. f x) ≤ n"

你应该能够degree_setsum_smaller通过归纳证明A（使用induct rule: finite_induct），然后用它来证明degree_poly_smaller。多项式库中的引理degree_add_le应该很有用。

于 2013-09-12T22:33:11.430 回答
1

通常认为将 auto 用作应用脚本中最后一种方法以外的任何方法都被认为是不好的风格，因为这样的证明往往非常脆弱。我会完全消除“finiteSetSmallerThanNumber”引理，它是 Collect_le_nat 的一个不必要的特殊情况。此外，Isabelle 中通常不使用定理的驼峰式名称。

无论如何，这是我对如何使证明更好的建议：

lemma degree_setsum_smaller:
  "finite A ⟹ ∀x∈A. degree (f x) ≤ n ⟹ degree (∑x∈A. f x) ≤ n"
by (induct rule: finite_induct, simp_all add: degree_add_le)

lemma degree_smaller:
  fixes a :: "('a::comm_ring_1 poly)" and n::nat
  shows "degree (∑x∷nat | x ≤ n . monom (coeff a x) x) ≤ n"
proof (rule degree_setsum_smaller)
  show "finite {x. x ≤ n}" using finite_Collect_le_nat .
  {
    fix x assume "x ≤ n"
    hence "degree (monom (coeff a x) x) ≤ n"
        by (cases "coeff a x = 0", simp_all add: degree_monom_eq)
  }
  thus "∀x∈{x. x≤ n}. degree (monom (coeff a x) x) ≤ n" by simp
qed
于 2013-09-24T21:27:18.987 回答