Доказательство существования простой факторизации (образовательной)

Question

Я пытаюсь написать доказательство существования простой факторизации чисел. Он предназначен для образования, поэтому каждая функция определена, мы стараемся не использовать Изабель, встроенную в функции. Вот мой код:

(* addition*) 
primrec suma::"nat ⇒ nat ⇒ nat" where 
"suma 0 n = 0" | 
"suma (Suc x) n = Suc (suma x n)" 

primrec pred::"nat ⇒ nat" where 
"pred 0 = 0" | 
"pred (Suc x) = x" 

(* substraction *) 
primrec resta::"nat ⇒ nat ⇒ nat" where 
"resta m 0 = m" | 
"resta m (Suc x) = pred (resta m x)" 

primrec mult::"nat ⇒ nat ⇒ nat" where 
"mult 0 m = 0" | 
"mult (Suc x) m = suma m (mult x m)" 

lemma less_pred [simp]: "(x < y) ⟶ (pred x < y)" 
proof (induct x) 
case 0 then show ?case by simp 
next 
case (Suc x) then show ?case by simp 
qed 

lemma less_n_pred [simp]: "∀n::nat. (n ≠ 0) ⟶ (pred n < n)" 
proof 
fix n::nat show "n ≠ 0 ⟶ pred n < n" by (induct n) simp_all 
qed 

lemma less_resta [simp]: "(m > 0 ∧ n > 0) ⟶ (resta m n < m)" 
proof (induct n) 
case 0 then show ?case by simp_all 
next 
case (Suc x) then show ?case by force 
qed 

fun divi::"nat ⇒ nat ⇒ nat" where 
"divi m n = (if n = 0 then 
       undefined 
      else 
       if m = 0 
       then 0 
       else Suc (divi (resta m n) n))" 

fun modulo::"nat ⇒ nat ⇒ nat" where 
"modulo m n = (if n = 0 then 
       undefined 
      else 
       if m < n 
       then m 
       else modulo (resta m n) n)" 

definition divide::"nat ⇒ nat ⇒ bool" where 
"divide m n = (modulo n m = 0)" 

primrec numTo :: "nat ⇒ nat list" where 
"numTo 0 = []" | 
"numTo (Suc x) = (Suc x)#(numTo x)" 

primrec filter:: "'a list ⇒ ('a ⇒ bool) ⇒ 'a list" where 
"filter [] p = []" | 
"filter (x#xs) p = (if p x then x#(filter xs p) else filter xs p)" 

definition divisores::"nat ⇒ nat list" where 
"divisores n = (filter (numTo n) (λm. divide m n))" 

definition is_prime::"nat ⇒ bool" where 
"is_prime n = (length (divisores n) = 2)" 

primrec all_prime::"nat list ⇒ bool" where 
"all_prime [] = True" | 
"all_prime (x#xs) = (is_prime x ∧ all_prime xs)" 

primrec prod_list::"nat list ⇒ nat" where 
"prod_list [] = 1" | 
"prod_list (x#xs) = mult x (prod_list xs)" 

lemma mult_num: "∀n::nat. n>1 ∧ ¬ is_prime n ⟶ (∃x y::nat. x < n ∧ y < n ∧ mult x y = n)" 
proof 
fix n::nat 
(* This lemma might be useful? *) 

theorem exists_prime_factor: "∀n::nat. (n > 1 ⟶ (∃xs::nat list. prod_list xs = n ∧ all_prime xs))" 
proof 
    fix n::nat 
    show "(n > 1 ⟶ (∃xs::nat list. prod_list xs = n ∧ all_prime xs))" 
    proof (induct n rule: less_induct) 
(* How can i prove this? *) 

Как я могу доказать теорему exists_prime_factor: ∀n::nat. (n > 1 ⟶ (∃xs::nat list. prod_list xs = n ∧ all_prime xs))?

Заранее благодарю вас за помощь.

Answer 1

Один короткий ответ заключается в том, что вы начали с основной ошибки в своем определении suma. Должно быть это (я думаю):

primrec suma::"nat ⇒ nat ⇒ nat" where 
    "suma 0 n = n" | 
    "suma (Suc x) n = Suc (suma x n)" 

Мой длинный ответ должен делать с тем, как использовать value, nitpick и sledgehammer, чтобы увидеть, если вы находитесь на правильном пути.

Если вы не можете что-то доказать, быстро попробуйте sledgehammer. Если sledgehammer ничего не возвращает, тогда попробуйте nitpick.

Если nitpick находит контрпример, это хороший индикатор, что ваша гипотеза неверна, хотя никакой гарантии нет. Уточненные определения, вызванные undefined, THE и SOME, могут вызывать это или не определять все случаи для primrec.

Используйте value, чтобы сделать быструю проверку ваших функций

Использование value был конечный результат меня пытаются понять вещи, не полностью перебирая всю свою логику.

value "mult 2 2" (* Suc (Suc 0) *) 

Оттуда это было просто, наконец, увидев очевидное.

Используйте value, чтобы узнать, работают ли ваши функции правильно, хотя для этого необходимо, чтобы генераторы кода упрощали входы value.

Использование nitpick, это бесплатно

Для таких вещей, как это, я хотел бы видеть, если sledgehammer может работать волшебство.

Во-первых, это лучше, чтобы избавиться от внешних кванторов, как это:

theorem exists_prime_factor: 
    "n > 1 --> (∃xs::nat list. prod_list xs = n ∧ all_prime xs)" 
    apply(induct n, auto) 
    sledgehammer 
    oops 

Когда sledgehammer возвращает вообще ничего, то гипотеза не является ложным, или вам нужно, чтобы помочь его.

придираться дал мне контрпример n = 2, но говорят, что это потенциально поддельной, и вы используете undefined в определениях, которые могут испортить nitpick.

В конце концов, я побежал nitpick на ваш lemma mult_num, и он дал мне контрпример от n = 4.

Одна вещь, чтобы попытаться доказать отрицание вашей теоремы, что определенно доказывает, что ваша теорема неверна. Я пытался доказать это:

theorem 
    "(x >= 4) | (y >= 4) | ~(mult x y = 4)" 

Наконец, я сказал: «Хм, позволяет попробовать что-то просто»:

value "mult 2 2" 

Это было возвращение 2, который, наконец, помогли мне увидеть очевидное.

Неопределенное не может быть то, что вы думаете, это

Я специально искал то, что беспорядок nitpick вверх, один из них является использование undefined, таких как ваша функция здесь:

fun divi::"nat ⇒ nat ⇒ nat" where 
    "divi m n = (if n = 0 then undefined 
       else if m = 0 then 0 
       else Suc (divi (resta m n) n))" 

Это пример того, где value не поможет вам. Он не может упростить это:

value "divi 3 0" (* divi (Suc (Suc (Suc 0))) 0 *) 

Если вы будете следовать в прошлом обсуждение терминологии Isabelle/HOL, некоторые эксперты предпочли бы, чтобы undefined называться underspecified.

Вот эта теорема не может быть доказана:

theorem "divi n 0 ~= (1::nat)" 
    apply(induct n, auto) 
oops 

придираться находит контрпример:

theorem "divi n 0 ~= (1::nat)" 
    nitpick (* 
    Nitpick found a counterexample: 

    Free variable: 
    n = 1 
*) 
oops 

Но потом, это же контрпример, как для этого:

theorem "divi n 0 = (1::nat)" 
    nitpick 
oops 

Почему все это? Потому что undefined::nat является nat. Если вы никогда не определяете его, например, с аксиомой, то вы не можете сказать, что nat равно, хотя оно должно быть равно некоторому уникальному nat.

Как насчет 44?

theorem "(divi n 0 = 44) <-> undefined = (44::nat)" 
    by(simp) 

Кажется, есть бесконечно малая вероятность того, что n = 1023456.

theorem "(divi n 0 = 1023456) <-> undefined = (1023456::nat)" 
    by(simp) 

Последствие? Бесконечно много шуток, которые можно было бы сделать об этом, бесконечно малого юмора.