Proof of existence of prime factorization (Educational)

Question

I am trying to write a proof of the existence of the prime factorization of numbers. It is meant to be educational, so every function is defined, we try not to use Isabelle built in functions. Here is my code:

(* 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? *)

How can I prove theorem exists_prime_factor: ∀n::nat. (n > 1 ⟶ (∃xs::nat list. prod_list xs = n ∧ all_prime xs))?

Thank you in advance for your help.

Answer 1

One short answer is that you started with a basic mistake in your definition of suma. It should be this (I guess):

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

My long answer has to do with how to use value, nitpick, and sledgehammer to see if you're on the right track.

If you can't prove something, a quick thing to try is sledgehammer. If sledgehammer returns nothing at all, then it's a good idea to try nitpick.

If nitpick finds a counterexample, that's a good indicator that your conjecture is false, though no guarantee. Underspecified definitions due to undefined, THE, and SOME can cause that, or not defining all cases for primrec.

Use value to do quick checks of your functions

Using value was the end result of me trying to figure things out, without completely sorting out all your logic.

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

From there, it was just finally seeing the obvious.

Use value to see if your functions are working right, though that requires that value inputs can be simplified by the code generator.

Use nitpick, it's free

For things like this, I like to see if sledgehammer can work magic.

First, it's best to get rid of outer quantifiers, like this:

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

When sledgehammer returns nothing at all, then the conjecture is false, or you need to help it out.

Nitpick gave me the counterexample of n = 2, but it say it's potentially spurious, and you're using undefined in your definitions, which can mess up nitpick.

Eventually, I ran nitpick on your lemma mult_num, and it gave me a counterexample of n = 4.

One thing to try is to prove the negation of your theorem, which definitely proves that your theorem is false. I was trying to prove this:

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

Finally, I said, "Hmmm, lets try something simple":

value "mult 2 2"

That was returning 2, which finally helped me see the obvious.

Undefined may not be what you think it is

I was specifically looking for things that mess nitpick up, one of them being the use of undefined, such as your function here:

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))"

This is an example of where value is not going to help you out. It can't simplify this:

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

If you follow past discussion of Isabelle/HOL terminology, some experts would prefer that undefined be called underspecified.

Here, this theorem cannot be proved:

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

Nitpick finds a counterexample:

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

  Free variable:
    n = 1
*)
oops

But then, it's the same counterexample as for this:

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

Why all this? Because undefined::nat is a nat. If you never define it, such as with an axiom, then you can't say what nat is equal to, though it has to be equal to some unique nat.

How about 44?

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

It seems there's an infinitely small chance that n = 1023456.

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

The consequence? There are infinitely many jokes that could be made about this, of infinitesimal size humor.