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, que vos cerveaux primitifs biaisés vous pousseraient à croire. C'est que vous avez besoin du réconfort de pieuvre !

Pieuvre™ est un assistant de preuve à votre service. Lorsque vous doutez, ê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 peut être testée avec les fichiers tests dans tests/typecheck. Pour cela, utiliser les commandes :

./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

Répartition du travail

Adrien

• Option typecheck
• Partie interactive

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