{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "e5a72e1c",
   "metadata": {},
   "source": [
    "# ALL TP3. Arithmétique de Presburger avec Walnut\n",
    "\n",
    "[Walnut](https://cs.uwaterloo.ca/~shallit/walnut.html) est un logiciel utilisé par des chercheurs de combinatoire des mots pour explorer les arithmétiques de Büchi (une extension de l'arithmétique de Presburger). Il met en œuvre l'algorithme de décision des formules du premier ordre de la logique associée en utilisant les automates finis.\n",
    "\n",
    "Dans ce TP, nous allons apprendre la syntaxe (un peu baroque) de Walnut, observer les automates finis produits et résoudre quelques problèmes simples exprimables dans l'arithmétique de Presburger."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "4db025fc",
   "metadata": {},
   "source": [
    "## 1. Un peu de syntaxe\n",
    "\n",
    "### 1.1 Des commandes"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "3d1258c7",
   "metadata": {},
   "source": [
    "Walnut fonctionne avec des commandes. Une commande est un mot-clé, suivi d'éventuels arguments, éventuellement sur plusieurs lignes, et terminé obligatoirement par un symbole de fin de commande :\n",
    " - `;` est le symbole le plus courant, il exécute la commande silencieusement ;\n",
    " - `:` affiche quelques informations statistiques sur les automates construits ;\n",
    " - `::` affiche davantage d'informations (utile pour les très grosse formules).\n",
    " \n",
    "Ce notebook transmet à l'interprète tout ce que vous tapez dans une cellule de code. Si vous oubliez le symbole de fin de commande, les contenus envoyés vont s'accumuler. En cas de souci, n'hésitez pas à réexécuter la cellule."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "36f5c3c6",
   "metadata": {},
   "source": [
    "Voici les principales commandes que nous utiliserons dans ce TP :\n",
    " - `help` fournit une aide minimaliste sur une commande passée en paramètre ;\n",
    " - `eval` permet de compiler un prédicat, décrit par une formule, en un automate fini ;\n",
    " - `def` fonctionne comme `eval` en donnant un nom au prédicat pour l'utiliser dans de futures formules ;\n",
    " - `reg` permet de définir directement un prédicat à partir d'une expression régulière ;\n",
    " - `inf` teste si un prédicat est validé par une infinité de valeurs ;\n",
    " - `test` génère des valeurs qui valident le prédicat."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "ba9f6fe6",
   "metadata": {},
   "source": [
    "Nous utiliserons aussi la commande magique `%showme` pour afficher les automates dans ce notebook. Ce n'est pas une commande Walnut, c'est une commande du noyau Jupyter."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "c4ff4bdd",
   "metadata": {},
   "outputs": [],
   "source": [
    "help inf;"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "c9c62f73",
   "metadata": {
    "scrolled": false
   },
   "outputs": [],
   "source": [
    "help eval;"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "b0afd512",
   "metadata": {},
   "source": [
    "### 1.2 Des formules"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "04ff4d46",
   "metadata": {},
   "source": [
    "Walnut représente les prédicats par des automates finis qui lisent en entrée des tuples d'entiers, par défaut en binaire avec le bit de poids fort en tête. Ces prédicats sont compilés à partir de formules de l'arithmétique de Presburger."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "495ff277",
   "metadata": {},
   "source": [
    "### 1.2.1 Formules atomiques\n",
    "\n",
    "Les formules atomiques sont construites à partir de constantes entières, de variables, de l'opération d'addition et des relations d'égalité et de comparaison. Les commandes `eval` et `def` prennent en argument un nom de prédicat suivi d'une formule entre guillemets.\n",
    "\n",
    "✏️✏️✏️ Évaluez les cellules ci-dessous. N'hésitez pas à les modifier pour voir ce qui se passe."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "04e7891b",
   "metadata": {},
   "outputs": [],
   "source": [
    "eval tadam \"1+1=2\";"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "3fadac09",
   "metadata": {},
   "outputs": [],
   "source": [
    "eval tadam \"2+2<3\";"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "92e5b432",
   "metadata": {},
   "source": [
    "Les prédicats sans variables libres s'évaluent à `TRUE` ou `FALSE`. Lorsqu'il y a des variables libres, le prédicat est compilé en un automate qui acceptent les tuples de valeurs pour les variables (par ordre lexicographique de leurs noms) qui satisfont le prédicat.\n",
    "\n",
    "✏️✏️✏️ Évaluez les cellules ci-dessous. N'hésitez pas à les modifier pour voir ce qui se passe."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "f359ef5b",
   "metadata": {
    "scrolled": true
   },
   "outputs": [],
   "source": [
    "eval essai \"x=6\":"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "1b0232ef",
   "metadata": {
    "scrolled": false
   },
   "outputs": [],
   "source": [
    "%showme essai"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "fd9d8797",
   "metadata": {},
   "outputs": [],
   "source": [
    "eval somme \"x+y=4\":"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "362704c8",
   "metadata": {},
   "outputs": [],
   "source": [
    "%showme somme"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "001f6670",
   "metadata": {},
   "outputs": [],
   "source": [
    "eval addition \"x+y=z\":"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "4b88168b",
   "metadata": {
    "scrolled": true
   },
   "outputs": [],
   "source": [
    "%showme addition"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "0bc92ea6",
   "metadata": {},
   "outputs": [],
   "source": [
    "eval pair \"n=2*q\":"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "1e346bcd",
   "metadata": {},
   "outputs": [],
   "source": [
    "%showme pair"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "963f5adb",
   "metadata": {},
   "source": [
    "### 1.2.2 Connecteurs logiques\n",
    "\n",
    "Les formules atomiques peuvent être combinées entre elles avec des connecteurs :\n",
    " - `~` la négation (NON)\n",
    " - `&` la conjonction (ET)\n",
    " - `|` la disjonction (OU)\n",
    " - `^` la disjonction exclusive (XOR)\n",
    " - `=>` l'implication\n",
    " - `<=>` l'équivalence\n",
    " - `E` le quantificateur existentiel `Ex` ou encore `Ex,y,z`\n",
    " - `A` le quantificateur universel `Ay` ou encore `Ai,j,k`\n",
    " \n",
    " ✏️✏️✏️ Évaluez les cellules ci-dessous. N'hésitez pas à les modifier pour voir ce qui se passe."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "746c3d46",
   "metadata": {},
   "outputs": [],
   "source": [
    "eval estpair \"Eq n=2*q\":"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "7b421cf5",
   "metadata": {},
   "outputs": [],
   "source": [
    "%showme estpair"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "0bb0f1f4",
   "metadata": {},
   "outputs": [],
   "source": [
    "eval blop \"Ax,y (n=x+y & x<y & (Eq y=2*q)) => (Er n+x = 2*r)\":"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "8989389e",
   "metadata": {
    "scrolled": true
   },
   "outputs": [],
   "source": [
    "%showme blop"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "d933a9d5",
   "metadata": {},
   "source": [
    "### 1.2.3 Réutiliser des définitions, créer des prédicats autrement\n",
    "\n",
    "La commande `def` permet de mémoriser un prédicat pour le réutiliser. Une fois le prédicat `canard` défini, il est utilisé dans une formule en ajoutant le symbole `$` devant son nom `$canard(x,2)`.\n",
    "\n",
    "La commande `reg` permet de définir des prédicats directement à partir d'une expression régulière.\n",
    "\n",
    "Walnut permet aussi d'écrire directement un automate dans une fichier et de l'utiliser comme prédicat.\n",
    "\n",
    " ✏️✏️✏️ Évaluez les cellules ci-dessous. N'hésitez pas à les modifier pour voir ce qui se passe."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "b8e4159d",
   "metadata": {},
   "outputs": [],
   "source": [
    "help def;"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "e60a1aec",
   "metadata": {},
   "outputs": [],
   "source": [
    "def pair \"Eq n=2*q\":\n",
    "def impair \"Eq n=2*q+1\":"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "0831ac61",
   "metadata": {
    "scrolled": true
   },
   "outputs": [],
   "source": [
    "eval decomp \"An $impair(n) => Ei,j (i+j=n & $pair(i) & $impair(j))\":"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "df40628c",
   "metadata": {},
   "outputs": [],
   "source": [
    "help reg;"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "d0957aef",
   "metadata": {},
   "outputs": [],
   "source": [
    "reg pow2 msd_2 \"0*10*\";"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "1e05d79d",
   "metadata": {},
   "outputs": [],
   "source": [
    "eval ok \"$pow2(4) & $pow2(8) & $pow2(256) & ~ $pow2(127)\";\n",
    "eval yep \"An $pow2(n) => $pow2(2*n)\";\n",
    "eval ind \"$pow2(1) & An (n>1 & $pow2(n) => ($pair(n) & $pow2(n/2)))\";"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "66e40bd1",
   "metadata": {},
   "source": [
    "La création d'automates demande d'aller créer des fichiers au bon endroit."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "5ebed67e",
   "metadata": {},
   "outputs": [],
   "source": [
    "%%file ../Automata Library/poulpe.txt\n",
    "msd_2\n",
    "\n",
    "0 1\n",
    "0 -> 0\n",
    "1 -> 1\n",
    "\n",
    "1 0\n",
    "0 -> 2\n",
    "1 -> 0\n",
    "\n",
    "2 0\n",
    "0 -> 1\n",
    "1 -> 2"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "d99abfbd",
   "metadata": {
    "scrolled": false
   },
   "outputs": [],
   "source": [
    "help draw;"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "e7c34925",
   "metadata": {},
   "outputs": [],
   "source": [
    "draw $poulpe;"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "0855dc1f",
   "metadata": {},
   "outputs": [],
   "source": [
    "%showme poulpe"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "730a9101",
   "metadata": {},
   "outputs": [],
   "source": [
    "eval mod3 \"An (Eq n=3*q) <=> $poulpe(n)\":"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "a68ca008",
   "metadata": {},
   "source": [
    "## 2. Coller des timbres et manger des Nuggets"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "7217c3dd",
   "metadata": {},
   "source": [
    "Une marque de fastfood propose des boîtes de nuggets en trois tailles : 6, 9 et 20 pièces.\n",
    "\n",
    "En achetant différentes boîtes et en combinant leurs contenus, il est possible d'acheter certaines quantités de nuggets. Ainsi, on peut acheter 15 nuggets avec 1 boîte de 6 et une boîte de 9 ; ou encore 32 nuggets avec 2 boîtes de 6 et une boîte de 20.\n",
    "\n",
    "Certaines quantités ne sont pas accessibles de cette manière. Par exemple, il n'est pas possible d'acheter 7 nuggets ou encore 13 nuggets.\n",
    "\n",
    "✏️✏️✏️ Définissez un prédicat `nuggets` à un argument qui est vrai si et seulement si la quantité de nuggets passée en arguments peut être obtenue en combinant des boîtes de 6, 9 et 20 pièces. Affichez l'automate obtenu."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "666357c9",
   "metadata": {
    "scrolled": true
   },
   "outputs": [],
   "source": [
    "def nuggets \"TODO ICI MON PREDICAT\";"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "5cb34613",
   "metadata": {
    "scrolled": false
   },
   "outputs": [],
   "source": [
    "%showme nuggets"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "c685faa3",
   "metadata": {},
   "source": [
    "✏️✏️✏️ Vérifiez qu'à partir d'un certain nombre, on peut acheter n'importe quelle quantité de nuggets. Puis, calculez la plus grande quantité qu'il n'est pas possible d'acheter. On pourra l'afficher avec `%showme` ou à l'aide de la commande `test`. Vérifiez votre valeur décimale avec une commande `eval`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "7aba6efd",
   "metadata": {
    "scrolled": true
   },
   "outputs": [],
   "source": [
    "eval all \"TODO ON PEUT TOUT OBTENIR A PARTIR D'UN CERTAIN RANG\";"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "e9722204",
   "metadata": {
    "scrolled": true
   },
   "outputs": [],
   "source": [
    "def petit \"TODO LE PLUS PETIT QU'ON NE PEUT PAS ACHETER\":"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "2e720a9e",
   "metadata": {},
   "outputs": [],
   "source": [
    "test petit 1;"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "425fa8b7",
   "metadata": {
    "scrolled": false
   },
   "outputs": [],
   "source": [
    "eval ok \"$petit(TODO VALEUR QUI VA BIEN)\";"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "9e07db79",
   "metadata": {},
   "source": [
    "## 3. Une histoire de calendrier\n",
    "\n",
    "Dans notre calendrier, une année est bissextile si elle est multiple de 4 et ou bien qu'elle n'est pas multiple de 100 ou bien qu'elle est multiple de 400. Dans ce cas, l'année est composée de 366 jours au lieu de 365.\n",
    "\n",
    "✏️✏️✏️ À vous de jouer :\n",
    " 1. Définissez une formule qui teste si une année donnée est bissextile.\n",
    " 2. Puis définissez une formule qui compte le nombre d'années bissextiles dans un intervalle entre deux années données.\n",
    " 3. Validez votre prédicat en vérifiant qu'il y a eu 31 années bissextiles de 1900 à 2024 et 58 de 2001 à 2243. \n",
    " 4. En déduire une formule qui teste si le jour de l'An d'une année postérieure à 1900 donnée tombe un lundi.\n",
    " 5. Validez votre prédicat en vérifiant qu'entre 2000 et 2024, les seules années où le jour de l'an était un lundi ont été les années 2001, 2007, 2018 et 2024."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "a7708d21",
   "metadata": {
    "scrolled": true
   },
   "outputs": [],
   "source": [
    "def bissextile \"TODO\";\n",
    "eval verif \"$bissextile(2024) & ~$bissextile(2100) & ~$bissextile(2025) & $bissextile(2000)\";"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "262c6e24",
   "metadata": {
    "scrolled": true
   },
   "outputs": [],
   "source": [
    "def compte \"TODO\"::"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "cf43e54e",
   "metadata": {
    "scrolled": true
   },
   "outputs": [],
   "source": [
    "eval check \"$compte(2001,2243,58)\";\n",
    "eval check \"$compte(1900,2024,31)\";"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "ba06ddcd",
   "metadata": {
    "scrolled": true
   },
   "outputs": [],
   "source": [
    "def jalun \"TODO LE JOUR DE L'AN EST UN LUNDI\":"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "bc4a00fe",
   "metadata": {
    "scrolled": false
   },
   "outputs": [],
   "source": [
    "eval ok \"An (n>2000 & n<2025 & $jalun(n)) => (n=2001 | n=2007 | n=2018 | n=2024)\";"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "0bfbf288",
   "metadata": {},
   "source": [
    "## 4. SEND + MORE = MONEY\n",
    "\n",
    "Un célèbre puzzle demande de retrouver les chiffres, tous distincts, associés aux variables de l'équation suivante avec $M$ différent de 0.\n",
    "$$\n",
    "\\begin{array}{cccccc}\n",
    "&&S&E&N&D\\\\\n",
    "+&&M&O&R&E\\\\\\hline\n",
    "&M&O&N&E&Y\n",
    "\\end{array}\n",
    "$$\n",
    "\n",
    "✏️✏️✏️ Résoudre ce problème avec l'aide de Walnut !"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "e7318715",
   "metadata": {},
   "outputs": [],
   "source": [
    "TODO ALL"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "24c3172a",
   "metadata": {},
   "source": [
    "## 5. Nombres de Cantor\n",
    "\n",
    "Un entier est un nombre de Cantor si son écriture en base 3 ne contient pas le chiffre 1.\n",
    "\n",
    "Un entier est un nombre de Cantor alternatif si son écriture en base 3 ne contient pas le chiffre 2.\n",
    "\n",
    "✏️✏️✏️ Définissez ces deux types de nombre avec Walnut. Pour passer en base $3$ il faut ajouter `?msd_3` au début des formules et utilser `msd_3` comme ensemble de définition pour les expressions régulières. Démontrez ensuite les deux propriétés suivantes :\n",
    " 1. tout entier pair est la somme de deux nombres de Cantor ;\n",
    " 2. tout entier est la somme de deux nombres alternatifs de Cantor ;\n",
    " 2. tout nombre de Cantor est le double d'un nombre de Cantor alternatif ;\n",
    " 3. tout entier à partir de 7 est la somme de deux nombres qui ne sont pas des nombres alternatifs de Cantor ;"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "d503b2d8",
   "metadata": {
    "scrolled": true
   },
   "outputs": [],
   "source": [
    "TODO ALL"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Walnut",
   "language": "walnut",
   "name": "walnut"
  },
  "language_info": {
   "codemirror_mode": "null",
   "file_extension": ".walnut",
   "language": "walnut",
   "mimetype": "text/x-walnut",
   "name": "walnut",
   "version": "0.3.2"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}