Prouvant une identité de base Isabelle

Question

par la définition suivante qui suit definition phi :: "nat ⇒ nat" where "phi n = card {k∈{0<..n}. coprime n k}" (voir aussi ce answer)

Comment puis-je puis prouver un fait très basique, comme phi (p) = p-1 pour un premier p? Voici une formalisation possible de ce lemme, bien que je ne suis pas sûr que c'est le meilleur:

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

(prime_elem est défini dans Factorial_Ring.thy)

aide try resp. try0 ne mène nulle part. (Une preuve à la main est immédiate cependant, puisque le GCD entre tout m inférieur à p et p est de 1. Mais piquer autour de divers fichiers ne s'est pas avéré très utile, j'imagine que je dois deviner un lemme intelligent que j'ai pour donner auto pour que la preuve réussisse.)

Answer 1

Tout d'abord, true n'existe pas. Isabelle interprète cela comme une variable booléenne libre (comme vous pouvez le voir par le fait qu'elle est imprimée en bleu). Vous voulez dire True. En outre, l'écriture prime_elem p = True est quelque peu unidiomatic; il suffit d'écrire prime_elem p. Puis, je suggère d'utiliser prime p. C'est équivalent à prime_elem sur les naturels; pour les autres types, la différence est que prime requiert également que l'élément soit "canonique", c'est-à-dire 2 :: int est premier, mais -2 :: int ne l'est pas.

Ainsi, votre lemme ressemble à ceci:

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

Ensuite, vous devez prouver les éléments suivants:

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

Si vous jetez auto à cela, vous aurez deux objectifs secondaires, et peut sledgehammer Résolvez-les tous les deux, alors vous avez terminé. Cependant, la preuve obtenue est un peu laid:

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

Vous pouvez alors simplement prouver votre objectif général avec ceci:

thus ?thesis by (simp add: phi_def) 

Une façon plus raisonnable et solide serait cette preuve Isar:

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 

D'ailleurs, je recommande la restructuration de vos définitions de la manière suivante:

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

Ensuite, vous pouvez prouver de beaux lemmes auxiliaires pour rel_primes. (Vous en aurez besoin pour des propriétés plus compliquées de la fonction totient)