The Pieuvre™ Proof Assistant

Ne vous êtes jamais vous dit que votre quotidien était morose ? Que tout ce que vous pourriez prouver dans votre vie ne serait que vain ? C'est que vous avez besoin du réconfort de Pieuvre™ !

Pieuvre™ est un assistant de preuve à votre service. Lorsque vous doutez, que vous êtes effrayés par l'incurable finitude de votre esprit, l'ineffable efficacité de Pieuvre™ saura vous réconforter en vous assurant des preuves complètes et sans accroc.

Bien plus efficace que d'autres gallinacés, l'interface CLI de Pieuvre™ saura convenir à petits et grands. Son design entre post-modernisme et romantisme baroque néo-mérovingien rappellera aux utilisateur·ices les plus avertis les plus grandes heures de l'humanité.

Allez, tous à vos pieuvres !

L'équipe de Pieuvre™ n'est pas responsable des dommages occasionnés par les réalisations philosophiques causées aux utilisateur·ices de par l'utilisation du programme

Utilisation

Pieuvre génère automatiquement un fichier log.8pus contenant la preuve venant d'être faite. Attention, le fichier log.8pus ne doit jamais être donné en entrée de Pieuvre™ !

Option typecheck

L'option typecheck vérifie si un lambda-terme est bien typé. Elle s'utilise de la manière suivante :

./pieuvre -typecheck tests/typecheck/right-type
./pieuvre -typecheck tests/typecheck/wrong-type

Option alpha

L'option alpha vérifie si deux lambda-termes sont alpha-équivalents. Elle s'utilise de la manière suivante :

./pieuvre -alpha tests/lambda-terms/alpha-eq.lams
./pieuvre -alpha tests/lambda-terms/alpha-not-eq.lams

Option reduce

L'option alpha vérifie si deux lambda-termes sont alpha-équivalents. Elle s'utilise de la manière suivante :

./pieuvre -reduce tests/lambda-terms/lambda.lam

Notes d'implémentation

• Les λ-termes à trous sont représentés par leurs fonctions de remplissage. À la liste des λ-termes à mettre dans les trous, on associe le λ-terme complété.

Découpage des fichiers

• lexer.mll et parser.mly sont les fichiers pour le parser ocamlyacc
• main.ml contient le code gérant la ligne de commande, la construction du lambda-terme en appelant les fonctions de pieuvre.ml
• pieuvre.ml contient toutes les fonctions de manipulation de λ-termes.
• structs.ml contient l'ensemble des structures de données : λ-terme, environnements, types
• tactic.ml contient la structure de définition des tactiques.

Répartition du travail

Adrien

• Interface interactive (avec le parsage des formules, des tactiques, ...), lecture des fichiers
• Construction d'un lambda-terme à partir de la preuve (sans et / ou )
• Tactiques élémentaires (intro, intros, assumption, apply, elim)
• Options alpha, reduce, typecheck, ... : partie interactive appelant les fonctions écrites par Samy
• Écriture de tests (irréfutabilité du tiers exclus, de la formule de Peirce, ...)

Samy

• Introduction du README
• Fonctions de manipulation des λ-termes (pieuvre.ml)
• Typecheck
• Erreurs lors des tactiques.
• \/ et /\
• Parsing des λ-termes
• True et exact
• Option -computetype
• Écriture de tests