Consider the following minimal working example of Isabelle, where I defined two different functions, func1 and func2, that should emulate Eulers Totient function.
Oddly, the obivious definition is false and changing the definition only slightly by introducing ∈ℕ leads to correct, but yet unprovable definition.
(The exact questions I interspersed with the code, as that makes it probably clearer to what I'm referring).
theory T
imports
Complex_Main
"~~/src/HOL/Number_Theory/Number_Theory"
begin
(* Part I*)
definition func1 :: "nat ⇒ nat"
where "func1 n = card {m. m≤n ∧ coprime n m}"
lemma func1_equals : "func1 1 = 2" (* This equation is obviously false...*)
by (auto simp: func1_def)
(* Question 1: Why is this proof correct according to Isabelle? *)
(* Part II*)
definition func2 :: "nat ⇒ nat"
where "func2 n = card {m. m∈ℕ ∧ m≤n ∧(coprime n m)}"
(* Slightly changed definition by incorporating ∈ℕ*)
lemma func2_equals : "func2 1 = 1"
apply (auto simp: func2_def)
(* Unproved subgoal <<card {m ∈ ℕ. m ≤ Suc 0} = Suc >> looks more promising *)
oops
(* Question 2: Which proof method should I use to prove the last lemma?
Interestingly, sledgehammer runs out of time...*)
Question 3: Analogous to Q2 but for func2 4 = 2 ? The difference now is that
the preliminary <<apply (auto simp: func2_def)>> rewrites to a slightly
different subgoal. *)
end
Are there perhaps any more elegant ways to define the Euler totient function ?
Your two definitions are equivalent:
lemma "func1 n = func2 n"
by (simp add: func1_def func2_def Nats_def)
The reason why you get 2 instead of 1 is a subtle one and a perfect example of the kind of problems you run into when you formalise mathematical definitions: The natural numbers in Isabelle contain 0, so if you evaluate func1 1, you look at the numbers no greater than 1 – 0 and 1 – and check which of them are coprime to 1. Since gcd 0 n = n for all n, you find that both 0 and 1 are coprime to 1 and therefore the result is 2.
Euler's totient function only counts the positive integers less than n that are coprime to n, so your definition should look more like this:
definition totient :: "nat ⇒ nat" where
"totient n = card {k ∈ {0<..n}. coprime k n}"
If you want code generation to work, you can use the following code equation:
lemma totient_code [code]: "totient n = card (Set.filter (λk. coprime k n) {0<..n})"
by (simp add: totient_def Set.filter_def)
Then you can do this:
value "map (int ∘ totient) [1..<10]"
(* Output: "[1, 1, 2, 2, 4, 2, 6, 4, 6]" :: "int list" *)
Note that while I think the totient function would be very nice to have in Isabelle, I'm not sure it's the best think for a beginner to explore, since the proofs involving cardinalities of sets and these things might get a bit involved. A good way to get to know the system is the free bok Concrete Semantics by Nipkow and Klein. The examples and exercises in that book are more computer science/programming-oriented, but the material is more geared towards beginners and more amenable to interactive theorem proving in the sense that the proofs tend to get less messy and require less experience with the system.
And, by the way, the reason why sledgehammer fails to prove func2 1 = 1 is because the result is 2 and not 1. You can prove that by unfolding the definition of ℕ (which, for natural numbers, is basically just UNIV) as I did above, either by doing unfolding Nats_def or adding Nats_def to the simp set with simp add:.
