Степень полинома меньше числа

Question

Я работаю над леммой, которая показывает, что степень суммы мономов всегда меньше или равна 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 *) 

Answer 1

Последний шаг не следует из вашего 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 из библиотеки полиномов должна быть полезна.

Answer 2

Как правило, считается непристойным для использования авто как ничего, кроме последнего метода в сценарии приложения, поскольку такие доказательства имеют тенденцию быть довольно хрупкими. Я полностью исключаю лемму «конечный набор», это ненужный конкретный частный случай Collect_le_nat. Кроме того, имена верблюдов для теорем обычно не используются в Изабель.

Во всяком случае, это мое предположение о том, как сделать корректуру лучше:

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