Quantification universelle dans Isabelle/HOL

Question

Il m'est venu à l'esprit qu'il y a plusieurs façons de traiter la quantification universelle en travaillant avec Isabelle/HOL Isar. J'essaie d'écrire des preuves dans un style qui convient aux étudiants de premier cycle à comprendre et à reproduire (c'est pourquoi j'utilise Isar!) Et je suis confus sur la façon d'exprimer la quantification universelle d'une manière agréable.

Dans Coq par exemple, je peux écrire forall x, P(x) et ensuite je peux dire «induction x» et cela générera automatiquement des objectifs selon le principe d'induction correspondant. Cependant, Isabelle/HOL Isar, si je veux appliquer directement un principe d'induction, je dois énoncer le théorème sans quantification, comme ceci:

lemma foo: P(x) 
proof (induct x) 

Et cela fonctionne très bien x est alors traitée comme une variable schématique, comme si elle était universellement quantifiée. Cependant, il manque la quantification universelle dans la déclaration qui n'est pas très éducative. Une autre façon dont j'ai fonds est en utilisant \<And> et \<forall>. Cependant, je ne peux pas appliquer directement le principe d'induction si je déclare le lemme de cette façon, je dois d'abord fixer les variables quantifiées universellement ... qui semble encore peu pratique d'un point de vue pédagogique:

lemma foo: \<And>x. P(x) 
proof - 
fix x 
show "P(x)" 
proof (induct x) 

Qu'est-ce que est un bon modèle de preuve pour exprimer une quantification universelle qui ne nécessite pas de fixer explicitement des variables avant l'induction?

Answer 1

Vous pouvez utiliser induct_tac, case_tac, etc. Ce sont les variantes héritées des méthodes induct/induction et cases utilisés dans bon Isar. Ils peuvent fonctionner sur des variables méta-universellement quantifiés liés à l'état de but, comme le x dans votre deuxième exemple:

lemma foo: "⋀x. P(x :: nat)" 
proof (induct_tac x) 

Un inconvénient de induct_tac sur induction est qu'il ne fournit pas les cas, vous ne pouvez pas écrire case (Suc x) puis from Suc.IH et show ?case dans votre épreuve. Un autre inconvénient est que l'adressage des variables liées est, en général, plutôt fragile, puisque leurs noms sont souvent générés automatiquement par Isabelle et peuvent changer quand Isabelle change. (pas dans le cas que vous avez montré ci-dessus, bien sûr)

C'est l'une des raisons pour lesquelles les épreuves Isar sont préférées ces jours-ci. Je déconseille vivement de montrer à vos élèves la «mauvaise» Isabelle avec l'intention qu'il leur soit plus facile de la comprendre. Les faits sont les suivants: les variables libres dans une déclaration de théorème d'Isabelle sont logiquement équivalentes à des variables quantifiées universellement et Isabelle les convertit automatiquement en variables schématiques après que vous l'ayez prouvé. Cette convention n'est pas unique à Isabelle; il est commun en mathématiques et en logique, et il aide à réduire l'encombrement. Isar tente en particulier d'éviter l'utilisation explicite de l'opérateur ⋀ dans les énoncés d'objectifs (c'est-à-dire have/show, ils apparaissent toujours dans assume). Or, en résumé: les variables libres dans les théorèmes sont universellement quantifiées par défaut. Je doute que les étudiants trouveront cela difficile à comprendre; Je ne l'ai certainement pas fait quand j'ai commencé avec Isabelle en tant qu'étudiante en BSc. En fait, j'ai trouvé beaucoup plus naturel d'énoncer un théorème comme xs @ (ys @ zs) = (xs @ ys) @ zs au lieu de ∀xs ys zs. xs @ (ys @ zs) = (xs @ ys) @ zs.