Prouver la commutativité d'ajouter, Prendre 2

Question

Cette question est un suivi à la question suivante isabelle proving commutativity for add, mon suivi était trop long pour être un commentaire. Le problème comme indiqué était de montrer la commutativité de la fonction d'ajout défini comme suit:

fun add :: "nat ⇒ nat ⇒ nat" where 
    "add 0 n = n" | 
    "add (Suc m) n = Suc(add m n)" 

Essayer

theorem "add m n = add n m" 
apply(induct_tac m) 
apply(auto) 

se coince (le cas inductif) en raison d'un manque lemme. Je me suis intéressé à ce problème et j'étudiais une autre méthode (quoique moins efficace) pour le prouver. Supposons que nous avons défini le Lemme

lemma Lemma1 [simp]: "add n (Suc 0) = Suc n 

qu'Isabelle peut se révéler automatiquement par induction Ensuite, l'étape inductive est de prouver

Suc (add k m) = add m (Suc k) 

que nous pourrions faire à la main comme suit

Suc (add k m) 
= Suc (add m k) by the IH 
= add (add m k) (Suc 0) by Lemma1 <-- 
= add m (add k (Suc 0)) by associativity (already proved) 
= add m (Suc k) by the Lemma1 --> 

Cependant , Isabelle est incapable de le prouver, et il semble que le simplificateur soit bloqué à la 2ème ligne. Cependant, en utilisant le plus évident

lemma Lemma2 [simp]: "add m (Suc n) = Suc (add m n)" 

au lieu de Lemma1, la preuve réussit. Il semble pouvoir utiliser Lemma2 dans les deux directions mais pas Lemma1 I défini ci-dessus. Est-ce que quelqu'un sait pourquoi? Je me sens comme je donne sur quelque chose d'évident, quelque part ..

Remarques: Je me rends compte du fait simplificateur applique uniquement les définitions dans un sens, mais utilise des heuristiques pour tenter de réduire les deux côtés de l'équation au même terme

Answer 1

Lemma2 n'est pas utilisé dans les deux sens, comme vous pouvez le voir quand vous essayez de faire la preuve manuellement à l'aide subst étapes:

theorem commutativity2: 
"add n m = add m n" 
apply (induct n) 
apply (subst Lemma0) 
apply (subst add.simps(1)) 
apply (rule refl) 

(* ⋀n. add n m = add m n ⟹ add (Suc n) m = add m (Suc n) *) 
apply (subst add.simps(2)) 
(* ⋀n. add n m = add m n ⟹ Suc (add n m) = add m (Suc n) *) 
apply (erule ssubst) 
(* ⋀n. Suc (add m n) = add m (Suc n) *) 
apply (subst Lemma2) 
(* ⋀n. Suc (add m n) = Suc (add m n) *) 
apply (rule refl) 
done 

Il est en train de travailler le côté droit de l'objectif équation, mais toujours en utilisant Lemma1 de de gauche à droite.

Si vous voulez faire la preuve que dans votre preuve manuelle, vous pouvez aussi le faire facilement Isabelle:

theorem commutativity: 
"add m n = add n m" 
proof (induct m) 
    show "add 0 n = add n 0" using Lemma0 by simp 
next case (Suc k) 
    have  "add (Suc k) n 
       = Suc (add k n)" by simp 
    also have "... = Suc (add n k)" using Suc.hyps by simp 
    also have "... = add (add n k) (Suc 0)" using Lemma1 by simp 
    also have "... = add n (add k (Suc 0))" using associativity by simp 
    also have "... = add n (Suc k)" using Lemma1 by simp 
    finally show ?case . 
qed 

EDIT:

Une preuve manuelle montrant pourquoi cela ne fonctionne pas avec Lemma1: Dans la première réécriture Lemme 1 doit être utilisé de droite à gauche (en utilisant [symmetric]). Pour faciliter le travail sans relâcher Isabelle, pouvez-vous également coller l'état de preuve au point où les preuves échouent, p. Ex.,

theorem commutativity3: 
"add n m = add m n" 
apply (induct n) 
apply (subst Lemma0) 
apply (subst add.simps(1)) 
apply (rule refl) 

(* ⋀n. add n m = add m n ⟹ add (Suc n) m = add m (Suc n) *) 
apply (subst Lemma1[symmetric]) back 
(* ⋀n. add n m = add m n ⟹ add (Suc n) m = add m (add n (Suc 0)) *) 
apply (subst associativity) 
(* ⋀n. add n m = add m n ⟹ add (Suc n) m = add (add m n) (Suc 0) *) 
apply (subst Lemma1) 
(* ⋀n. add n m = add m n ⟹ add (Suc n) m = Suc (add m n) *) 
apply (erule subst) 
(* ⋀n. add (Suc n) m = Suc (add n m) *) 
apply (subst add.simps(2)) 
(* ⋀n. Suc (add n m) = Suc (add n m) *) 
apply (rule refl) 
done