质因数分解的存在证明（教育）
Proof of existence of prime factorization (Educational)
我正在尝试写一个数字素因数分解存在的证明。它是为了教育，所以每个函数都被定义，我们尽量不使用 Isabelle 内置函数。这是我的代码：
(* 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))?
预先感谢您的帮助。
一个简短的回答是，您在开始定义 suma 时犯了一个基本错误。应该是这个（我猜的）：
primrec suma::"nat ⇒ nat ⇒ nat" where
"suma 0 n = n" |
"suma (Suc x) n = Suc (suma x n)"
我的长篇回答是关于如何使用 value、nitpick 和 sledgehammer 来查看您是否在正确的轨道上。
如果您无法证明某事，可以快速尝试 sledgehammer。如果 sledgehammer returns 什么都没有，那么尝试 nitpick 是个好主意。
如果nitpick找到一个反例，这很好地表明你的猜想是错误的，虽然没有gua运行tee。 Underspecified 由于 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 returns什么都没有时，则猜想不成立，或者需要你帮忙
Nitpick 给了我 n = 2 的反例，但它说它 可能是虚假的 ，而你在定义中使用了 undefined，这可以搞砸了 nitpick.
最终，我 运行 nitpick 在你的 lemma mult_num 上，它给了我 n = 4.
的反例
要尝试的一件事是证明你的定理的否定，这肯定证明你的定理是错误的。我试图证明这一点：
theorem
"(x >= 4) | (y >= 4) | ~(mult x y = 4)"
最后，我说，"Hmmm, lets try something simple":
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)
后果？可以开出无限多的笑话，微不足道的幽默。
我正在尝试写一个数字素因数分解存在的证明。它是为了教育，所以每个函数都被定义，我们尽量不使用 Isabelle 内置函数。这是我的代码：
(* 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))?
预先感谢您的帮助。
一个简短的回答是，您在开始定义 suma 时犯了一个基本错误。应该是这个（我猜的）：
primrec suma::"nat ⇒ nat ⇒ nat" where
"suma 0 n = n" |
"suma (Suc x) n = Suc (suma x n)"
我的长篇回答是关于如何使用 value、nitpick 和 sledgehammer 来查看您是否在正确的轨道上。
如果您无法证明某事，可以快速尝试 sledgehammer。如果 sledgehammer returns 什么都没有，那么尝试 nitpick 是个好主意。
如果nitpick找到一个反例，这很好地表明你的猜想是错误的，虽然没有gua运行tee。 Underspecified 由于 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 returns什么都没有时，则猜想不成立，或者需要你帮忙
Nitpick 给了我 n = 2 的反例，但它说它 可能是虚假的 ，而你在定义中使用了 undefined，这可以搞砸了 nitpick.
最终，我 运行 nitpick 在你的 lemma mult_num 上，它给了我 n = 4.
要尝试的一件事是证明你的定理的否定，这肯定证明你的定理是错误的。我试图证明这一点：
theorem
"(x >= 4) | (y >= 4) | ~(mult x y = 4)"
最后，我说，"Hmmm, lets try something simple":
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)
后果？可以开出无限多的笑话，微不足道的幽默。