Isabelle : question banale : "Max (S::nat set) = 0" implique que tous les éléments de S sont nuls

Question

J'essayais de prouver l'implication suivante :

lemma Max_lemma:
  fixes s::nat and S :: "nat set"
  shows " ((Max S) = (0::nat))  ( s  S . (s = 0))"
sorry
(* 
  Note: I added additional parentheses just to be sure.*)

Je pensais que cela serait plutôt trivial, c'est pourquoi j'ai essayé d'obtenir une preuve à l'aide de sledgehammer. Malheureusement, cela a échoué. Soit ma définition est fausse, soit il y a des difficultés avec les preuves automatiques impliquant de gros opérateurs comme Max.

J'ai essayé de mieux comprendre Max et max en regardant leurs définitions ainsi que toute documentation que j'ai pu trouver. Comme je l'ai fait précédemment, j'ai rencontré un problème avec Isabelle qui, en fin de compte, s'est avéré nécessiter beaucoup d'expérience malgré son apparence triviale (" Pourquoi Isabelle ne simplifie-t-elle pas le corps de ma construction "if _ then _ else" ? "), j'ai décidé de poster cette question ici.

Answer 1

Le théorème en tant que tel ne sera pas prouvable, car Max est défini par fold1 qui, à son tour, est une définition qui (à ma connaissance) ne fonctionne qu'avec des ensembles finis. Pour les ensembles finis, sledgehammer est un succès :

lemma Max_lemma:
  fixes s::nat and S :: "nat set"
  assumes "finite S"
  shows " ((Max S) = (0::nat))  ( s  S . (s = 0))"
using assms by (metis Max_ge le_0_eq)

La gestion des fonctions partielles par Isabelle est un peu malheureuse, et le fait que

"(n  {1::nat..}. n) = 0"

est un théorème (le marteau-pilon le trouve) rend probablement mal à l'aise les nouveaux venus à Isabelle. (Si seulement le résultat était -1/12 ...). Mais c'est une chose avec laquelle nous devons vivre.