Brute Force Computation · Beginner Questions

fun sumpow :: "nat ⇒ nat list ⇒ nat" where
  "sumpow p l = fold (+) (map (λx. x^p) l) 0"

definition is_sumpow :: "nat ⇒ nat ⇒ nat ⇒ bool"
  where "is_sumpow p n m ≡ ∃ l. length l = n ∧ m = sumpow p l"

lemma
  fixes n :: nat
  assumes "n ≤ 40000"
  shows "is_sumpow 3 9 n" and "n > 8042 ⟶ is_sumpow 3 6 n"

which, in plain english, states that the first 40,000 natural numbers can be expressed as the sum of 9 cubes, and furthermore that for 8042 < n ≤ 40000, it can be expressed as the sum of 6 cubes.

It seems to me that this should be done through some sort of brute force computation, however I'm not sure where to start when it comes to this kind of proof - I understand it has something to do with code generation, but I'm not sure how it should be used. If anybody could explain what the steps to proving something like this would look like, or if there are examples of similar brute force computations in the AFP I can learn from, that would be much appreciated, thanks!

Wolfgang Jeltsch (Dec 14 2023 at 15:31):

I would use the simplifier. For this, I would additionally phrase the problem in a computable way, which would perhaps include a list of numbers to check, and then prove by ordinary Isabelle means that the computable version is equivalent to the nice, declarative version that you gave above. The computable version would yield a boolean, which I would use as a fact statement (remember that saying lemma shows ⟨proposition⟩ or have ⟨proposition⟩ states that ⟨proposition⟩ is equal to True).

Wolfgang Jeltsch (Dec 14 2023 at 15:35):

Hmm, looking at your code in more detail, I realize that it already uses lists; so maybe it is already computable or is close to being so. The defining equation fun.simps is already registered as a simplification rule to be considered by default; you can achieve the same for the defining equation of is_sumpow by placing [simp]: in front of it.

Wenda Li (Dec 14 2023 at 21:39):

Here, your sumpow is computable but is_sumpow is not. We can quickly check the computability of the definitions using the value command:

value "sumpow 1 [1,2]" (*gives 3*)
value "is_sumpow 1 2 3" (*reports an error*)

To make is_sumpow computable, we can supply it with an alternative code equation:

lemma [code]: "is_sumpow p n m = undefined"
  oops

lemma
  fixes n :: nat
  assumes "n ≤ 40000"
  shows "is_sumpow 3 9 n" and "n > 8042 ⟶ is_sumpow 3 6 n"
proof -
  have "∀n≤40000. is_sumpow 3 9 n
            ∧ (n>8042 ⟶ is_sumpow 3 6 n)"
    sorry (*if the code equation works, we can use
    "by eval" to discharge this goal.*)
  then show "is_sumpow 3 9 n"
    "n > 8042 ⟶ is_sumpow 3 6 n"
    using assms by auto
qed

Manuel Eberl (Dec 14 2023 at 21:51):

Note that you'd probably want to optimise your search a bit more by not looking at all possible lists of 6 or 9 numbers but only some reasonable subset.

Manuel Eberl (Dec 14 2023 at 21:53):

If you only want to show existence and not not-existence you can also precompute values (e.g. in ML) and then only verify them in Isabelle (e.g. with the simplifier). That way you don't have to verify the entire search algorithm and all its optimisations.

Jamie Chen (Dec 26 2023 at 18:34):

Is there a preferred way of using precomputed values for this? The way I'm currently doing it is by having all 40,000 solutions as a list in a separate theory file, and importing that theory file into the file with the proof, but I was wondering if there's a better or more standard way of doing this.

Wenda Li (Dec 26 2023 at 21:54):

The sum-of-squares method (HOL/ex/SOS_Cert.thy) uses untrusted semidefinite programming solvers to find a proof certificate that is then checked by the Isabelle kernel. Here, the certificate is stored as a plain string in the current theory file. Not sure how large your certificate would be but I guess the Isabelle/ML infrastructure in HOL-Library.Sums_of_Squares could be relevant.

Stream: Beginner Questions

Topic: Brute Force Computation