Изабель: степень многочлена, умноженная на константу

Я работаю с библиотекой HOL/Library/Polynomial.thy.

Простое свойство не сработало. Например, степень 2x *2 равна степени 2x-

Как я могу доказать леммы (т.е. убрать извинения):

lemma mylemma:
    fixes y ::  "('a::comm_ring_1 poly)" and x ::  "('a::comm_ring_1)"
    shows "1 = 1" (* dummy *)
 proof- 
 have "⋀ x. degree [: x :] = 0" by simp

 from this have "⋀ x y. degree (y * [: x :] ) = degree y" sorry

 (* different notation: *)
 from this have "⋀ x y. degree (y * (CONST pCons x 0)) = degree y" sorry

.

Из ответа Мануэля решение, которое я искал:

 have 1: "⋀ x. degree [: x :] = 0" by simp
 {
   fix y :: "('a::comm_ring_1 poly)" and x :: "('a::comm_ring_1)"
   from 1 have "degree (y * [: x :]) ≤ degree y"
   by (metis Nat.add_0_right degree_mult_le)
 }

polynomial-math isabelle
person mrsteve    schedule 21.11.2013    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Здесь есть ряд вопросов.

Прежде всего, утверждение, которое вы пытаетесь показать, просто не годится для всех x. Если x = 0 и y непостоянны, например y = [:0,1:], у вас есть

degree (y * [: x :]) = degree 0 = 0 ≠ 1 = degree y

Очевидный способ исправить это - предположить x ≠ 0.

Однако и этого недостаточно, поскольку вы только предположили, что 'a является коммутативным кольцом. Однако в коммутативном кольце, как правило, делители нуля могут быть. Рассмотрим коммутативное кольцо ℤ/4ℤ. Пусть x = 2 и y = [:0,2:]. Потом y * [:x:] = [:0,4:], но 4 = 0 в ℤ/4ℤ. Следовательно y * [:x:] = 0, и, следовательно, снова,

degree (y * [: x :]) = degree 0 = 0 ≠ 1 = degree y

Итак, что вам действительно нужно, это одно из следующих двух:

  1. предположение x ≠ 0 и 'a :: idom вместо' a :: comm_ring. idom означает «область целостности», и это просто коммутативное кольцо с единицей и без делителей нуля.
  2. в более общем плане предположение, что x не является делителем нуля
  3. даже в более общем плане, предположение, что x * y ≠ 0 или, что то же самое, x умноженное на ведущий коэффициент y не равно 0

Кроме того, использование ⋀ в доказательствах Isar временами проблематично. «Правильный» способ Isar сделать это:

fix x :: "'a::idom" and y :: "'a poly"
assume "x ≠ 0"
hence "degree (y * [:x:]) = degree y" by simp

Соответствующие леммы degree_mult_eq и degree_smult_eq, вы увидите, что они требуют, чтобы тип коэффициента был идомом. Это работает для первого случая, который я описал выше, для двух других, я думаю, потребуются дополнительные рассуждения вручную.

РЕДАКТИРОВАТЬ: небольшая подсказка: вы можете найти подобные теоремы, набрав

find_theorems "degree (_ * _)"

Если вы попытаетесь применить degree_mult_eq, который он показывает к вашей ситуации (с comm_ring), вы обнаружите, что это не удается, даже если условия кажутся совпадающими. Если это так, обычно это проблема типа, поэтому вы можете написать что-нибудь вроде

from [[show_sorts]] degree_mult_eq

чтобы увидеть, какие типы и сортировки требуются леммой, и там написано idom.

person Manuel Eberl    schedule 21.11.2013
comment
Спасибо за супер ответ. Действительно, для моего доказательства достаточно ‹= степени y. - person mrsteve; 22.11.2013
comment
В этом случае я предлагаю degree_mult_le, который работает даже с коммутативными полукольцами. - person Manuel Eberl; 22.11.2013