CODEWITHSUNDEEP
isabelle
l7ll7
l7ll7

Reputation: 1329

Proving a basic identity in Isabelle

Consider the following following definition definition phi :: "nat ⇒ nat" where "phi n = card {k∈{0<..n}. coprime n k}" (see also this answer)

How can I then prove a very basic fact, like phi(p)=p-1 for a prime p ? Here is one possible formalization of this lemma, though I'm not sure it's the best one: 

lemma basic:
  assumes "prime_elem (p::nat) = true"
  shows "phi p = p-1"

(prime_elem is defined in Factorial_Ring.thy)

Using try resp. try0 doesn't lead anywhere. (A proof by hand is immediate though, since the GCD between any m less than p and p is 1. But poking around various file didn't turn out to be very helpful, I imagine I have to guess some clever lemma that I have to give auto for the proof to succeed.)

Upvotes: 1

Views: 187

Answers (1)

Manuel Eberl
Manuel Eberl

Reputation: 8298

First of all, true doesn't exist. Isabelle interprets this as a free Boolean variable (as you can see by the fact that it is printed blue). You mean True. Also, writing prime_elem p = True is somewhat unidiomatic; just write prime_elem p.

Next, I would suggest using prime p. It's equivalent to prime_elem on the naturals; for other types, the difference is that prime also requires the element to be ‘canonical’, i.e. 2 :: int is prime, but -2 :: int is not.

So your lemma looks like this:

lemma basic:
  assumes "prime_elem (p::nat)"
  shows "phi p = p - 1"
proof -

Next, you should prove the following:

from assms have "{k∈{0<..p}. coprime p k} = {0<..<p}"

If you throw auto at this, you'll get two subgoals, and sledgehammer can solve them both, so you're done. However, the resulting proof is a bit ugly:

apply auto
apply (metis One_nat_def gcd_nat.idem le_less not_prime_1)
by (simp add: prime_nat_iff'')

You can then simply prove your overall goal with this:

thus ?thesis by (simp add: phi_def)

A more reasonable and robust way would be this Isar proof:

lemma basic:
  assumes "prime (p::nat)"
  shows "phi p = p - 1"
proof -
  have "{k∈{0<..p}. coprime p k} = {0<..<p}"
  proof safe
    fix x assume "x ∈ {0<..p}" "coprime p x"
    with assms show "x ∈ {0<..<p}" by (cases "x = p") auto
  next
    fix x assume "x ∈ {0<..<p}"
    with assms show "coprime p x"  by (simp add: prime_nat_iff'')
  qed auto
  thus ?thesis by (simp add: phi_def)
qed

By the way, I would recommend restructuring your definitions in the following way:

definition rel_primes :: "nat ⇒ nat set" where
  "rel_primes n = {k ∈ {0<..n}. coprime k n}"

definition phi :: "nat ⇒ nat" where
  "phi n = card (rel_primes n)"

Then you can prove nice auxiliary lemmas for rel_primes. (You'll need them for more complicated properties of the totient function)

Upvotes: 2

Related Questions