Personnes présentes
- Thibaut Balabonski
- Chantal Keller
- Yakoub Nemouchi
- Hai Nguyen Van
- Frédéric Tuong
- Benoît Valiron
- Burkhart Wolff
- Lina Ye
Introduction (Burkhart)
Le but de ce groupe de travail est de présenter des objets de recherche actuels au sein des équipes VALS et MODHEL liés à Isabelle, selon trois critères :
- Pearls : présentation de développements élégants
- Problems : présentation de problèmes s'étant posés au cours d'un développement
- Projects : présentation de projets sur lesquels on a récemment travaillé
La périodicité sera de toutes les semaines ou d'une semaine sur deux (à définir), le mercredi à 14h.
Problème 1 (Thibaut)
Aucune tactique d'Isabelle ne sait prouver le but suivant :
have "0 ≤ 0"
Cela est dû au type inféré automatiquement par Isabelle pour cette expression :
term "0 ≤ 0"
{0::'a::{zero,ord}) <= {0::'a::{zero,ord}) :: bool
(avec
declare [[show_sorts]]
le system pretty printer peut etre configure de présenter pas seulement
types, mais aussi les sorts qui contraignent les variables de types. )
La classe de types choisie pour ≤ est ord, qui ne contient que le symbole. On ne sait donc pas qu'il s'agit d'une relation d'ordre, et donc que ce symbole est réflexif.
Pour résoudre le problème, on peut spécifier un type plus précis pour 0 comme pour ≤.
Démo : Thibaut
Problème 2 (Yakoub)
À quoi servent "using", "insert" et "obtain" ?
"using" est un mécanisme pour ajouter un théorème dans un "local one time context" d'Isar, qui peut utilisé juste une fois dans la prochaine application d'une Isar "method". L'avantage de using est qu'il prévoit aussi une instrumentation du theoreme pour la preuve, donc:
using X apply(auto)
et
apply(auto simp: X) ou bien apply(auto elim: X)
selon la forme du X. Cela permet de faire UNE istrumentation sans savoir trop sur simp, elim, dest, etc.
Par contre, "insert" va ajouter ce théorème comme meta-opremisse (donc comme le "A" dans "A ==> B") du but que l'on est en train de prouver.
"obtain" permet d'obtenir, à partir d'une propriété existentielle, un témoin pour cette propriété. obtain essaie apres simplification de construire un witness par elimination resulution (erule); le schema de l'emination est derivé automatiquement.
On a fait un example d'un obtain declaratif (blue style) and apply-style (red style).
Démo : Thibaut
Prochaine séance
La prochaine séance peut être soit le mercredi 16 septembre, animée par Frédéric Boulanger (Burkhart étant à Dagstuhl), soit le mercredi 23 septembre.