tp_pfm_2019.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# <span style=\"color: blue\">Cours et exercices de la découverte de Coq</span>"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## <span style=\"color: blue\">__Un langage fonctionnel pur (et même plus)__</span>"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Module nat_bool. (* Pour ne pas masquer les lemmes et définitions de la bibliothèque \n",
    "standard sur nat et bool, nous ouvrons un module. *)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### __Type algébrique de données__\n",
    "\n",
    "• Un type défini par les différents cas possibles, les constructeurs\n",
    "\n",
    "• Les constructeurs sont des objets à part entière\n",
    "\n",
    "• Existe en OCaml, ≈ type enum en C"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Voici un exemple :"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Inductive route : Type :=\n",
    "| departementale : route\n",
    "| nationale : route\n",
    "| autoroute : route."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Check route. (* route : Type *)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Check autoroute. (* autoroute : route *)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Pour examiner un terme dont le type est inductif, on utilise le\n",
    "__pattern-matching__ (filtrage)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Definition agrandir (r : route) := \n",
    "  match r with\n",
    "  | departementale => nationale\n",
    "  | nationale => autoroute\n",
    "  | autoroute => autoroute\n",
    "  end."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Check agrandir. (* agrandir : route -> route *)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Eval compute in (agrandir (agrandir nationale))."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Les constructeurs peuvent prendre des arguments."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Inductive terrain : Type :=\n",
    "| t_terre : terrain\n",
    "| t_route : route -> terrain\n",
    "| t_batiment : terrain."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Check (t_route nationale). (* terrain *)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Definition agrandir_terrain (t : terrain) := match t with\n",
    "| t_terre    => t_batiment\n",
    "| t_route r  => t_route (agrandir r)\n",
    "| t_batiment => t_batiment\n",
    "end."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Check agrandir_terrain. (* : terrain -> terrain *)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "A retenir ! - <span style=\"color:red\">__Contraintes sur le pattern-matching__ : Exhaustif et non-redondant. </span>"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### __Des types plus communs__\n",
    "\n",
    "Booléens - le type bool est prédéfini de la façon suivante :"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Inductive bool : Type :=\n",
    "| true : bool\n",
    "| false : bool."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Check true. (* true : bool *)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Check false. (* false : bool *)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Print bool."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Definition negb b :=\n",
    "match b with\n",
    "| true  => false\n",
    "| false => true\n",
    "end."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Check negb. (* negb : bool → bool *)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "A vous de jouer !\n",
    "\n",
    "Exercice 1. : Définir les fonctions [andb] et [orb] sur les boolénns."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Definition andb b1 b2 :=\n",
    "  match b1 with\n",
    "  | true  => b2\n",
    "  | false => false\n",
    "  end."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Definition orb b1 b2 :=\n",
    "  match b1 with\n",
    "  | true  => true\n",
    "  | false => b2\n",
    "  end."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "On peut définir des types récursifs, comme les entiers de Peano :"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Inductive nat : Type :=\n",
    "| O : nat        (* lettre O, interprété comme 0 *)\n",
    "| S : nat -> nat (* successeur *)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Check O. (* O : nat *)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Check S. (* S : nat -> nat *)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Notation \"0\" := O.\n",
    "Notation \"1\" := (S O)."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Les listes de booléens"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Inductive list_bool : Type :=\n",
    "| nilb : list_bool\n",
    "| consb : bool -> list_bool -> list_bool."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Check nilb. (* nil : list_bool *)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Check consb. (* cons : bool -> list_bool -> list_bool *)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Definition example := consb true (consb false (consb true nilb))."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Check example."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### __Fonctions récursives__\n",
    "\n",
    "On peut définir des fonctions récursives sur des types récursifs."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Fixpoint plus n m :=\n",
    "match n with\n",
    "| O => m\n",
    "| S n’ => S (plus n’ m)\n",
    "end.\n",
    "(*\n",
    "plus is defined\n",
    "plus is recursively defined (decreasing on 1st argument)\n",
    "*)\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Eval compute in (plus 3 4)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Notation \"n + m\" := (plus n m)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Eval compute in (0 + 1)."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "A retenir - <span style=\"color:red\"> __Terminaison__ : \n",
    "La fonction doit terminer ! </span>\n",
    "    \n",
    "<span style=\"color:red\"> Cas détecté automatiquement par Coq : récurrence structurelle </span>"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Concaténation de listes de booléens"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [
    {
     "ename": "SyntaxError",
     "evalue": "invalid syntax (<ipython-input-7-38d048c4e9c4>, line 1)",
     "output_type": "error",
     "traceback": [
      "\u001b[0;36m  File \u001b[0;32m\"<ipython-input-7-38d048c4e9c4>\"\u001b[0;36m, line \u001b[0;32m1\u001b[0m\n\u001b[0;31m    Fixpoint appb l1 l2 :=\u001b[0m\n\u001b[0m                ^\u001b[0m\n\u001b[0;31mSyntaxError\u001b[0m\u001b[0;31m:\u001b[0m invalid syntax\n"
     ]
    }
   ],
   "source": [
    "Fixpoint appb l1 l2 :=\n",
    "match l1 with\n",
    "| nilb => l2\n",
    "| consb a l => consb a (appb l l2)\n",
    "end.\n",
    "(* appb is recursively defined (decreasing on 1st argument) *)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Check appb. (* list_bool -> list_bool -> list_bool *)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Alors que si vous lancez cet exemple, Coq ne l'accepte pas !"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "(* Fixpoint appb_inc l1 l2 :=\n",
    "  match l1 with\n",
    "  | nilb => l2\n",
    "  | consb a l => consb a (appb_inc l1 l2)\n",
    "    end. \n",
    "*)\n",
    "(* Error: Cannot guess decreasing argument of fix. *)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Autres remarques sur les fonctions"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "• Fonctions comme valeurs de première classe"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Definition apply_neg (f:_-> _-> bool) b1 b2 :=\n",
    "f (negb b1) (negb b2)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Check apply_neg. \n",
    "(* apply_neg : (bool -> bool -> bool) -> bool -> bool -> bool *)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "• Applications partielles"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Definition nor := apply_neg andb."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Check nor. (* nor : bool -> bool -> bool *)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "• Fonctions anonymes"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Definition norb := \n",
    "   apply_neg (fun b1 => fun b2 => b2)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Eval compute in (norb true false)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Definition idb : bool -> bool := fun b => b.\n",
    "(* identique à\n",
    " Definition idb (b : bool) := b.\n",
    "*)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Definition my_first := apply_neg (fun b1 => fun b2 => b1)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Eval compute in (my_first true false)."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Type polymorphique"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Les types peuvent être paramétrés par d’autres types.\n",
    "\n",
    "Exemple le plus classique : les listes."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Inductive list (A:Type) : Type :=\n",
    "| nil : list A\n",
    "| cons : A -> list A -> list A."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Check list. (* list : Type -> Type *)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Check nil. (* nil : forall A : Type, list A *)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Check cons. (* cons : forall A : Type, A -> list A -> list A *)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Eval compute in (cons nat 1 (cons nat (S 1) (nil nat)))."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Eval compute in (cons bool true (cons bool false (nil bool)))."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Fonctions polymorphiques"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Les fonctions peuvent aussi être paramétrés par des types.\n",
    "\n",
    "Un exemple un peu artificiel."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Definition id (A:Type) (x:A) := x."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Check id. (* id : forall A : Type, A -> A *)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Un exemple sur les listes."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Fixpoint length (A:Type) (l:list A) :=\n",
    "  match l with\n",
    "  | nil _ => 0\n",
    "  | cons _ _ t => S (length A t)\n",
    "  end. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Eval compute in (length bool \n",
    "   (cons bool true \n",
    "         (cons bool false (nil bool))))."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Fixpoint app (A:Type) l1 l2 :=\n",
    "  match l1 with\n",
    "  | nil _      => l2\n",
    "  | cons _ a l => cons A a (app A l l2)\n",
    "    end. "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Retour sur un ancien exemple :"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Definition apply_neg (f:_-> _-> bool) b1 b2 :=\n",
    " f (negb b1) (negb b2)."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Pourquoi se limiter à bool ?"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Definition apply_neg_gen (A:Type) (f:_->_->A) b1 b2 :=\n",
    "  f (negb b1) (negb b2)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Definition nor2 := apply_neg_gen bool  andb.\n",
    "Check nor2. \n",
    "(* nor2 : forall A : Type, (bool -> bool -> A) -> bool -> bool -> A *)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Definition toto (b1 b2 : bool) := 0. \n",
    "\n",
    "Eval compute in apply_neg_gen  nat toto true false."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Lisibilité"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "On peut améliorer la lisibilité des termes manipulés."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "• Avec des paramètres implicites\n",
    "\n",
    "Si un argument peut toujours être inféré à partir d’un autre,\n",
    "on peut le rendre implicite."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Definition apply_neg_gen2 {A:Type} (f:_->_-> A) b1 b2 :=\n",
    "  f (negb b1) (negb b2)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Definition nor3 := apply_neg_gen2 andb.\n",
    "(* au lieu de apply_neg_gen bool andb\n",
    "ou apply_neg_gen _ andb *)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "• Avec des notations"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Notation \"x = y\" := ..."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Notation \"[ ]\" := nil."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## <span style=\"color:blue\"> Logique </span>"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Précédemment, tous nos objets étaient dans Type. \n",
    "\n",
    "Les énoncés sont dans un autre type : <span style=\"color:red\"> Prop </span>"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Check True. (* True : Prop *)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Check True -> False. (* True -> False : Prop *)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "__Énoncé d’un théorème__"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "• Un premier théorème"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Theorem negb_true_false : negb true = false."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "• Plus intéressant ?"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Theorem app_nil_l : forall {A : Type} (l : list A), app [] l = l."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "• Mais peut-on exprimer autre chose que des égalités ?"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "__Constantes, connecteurs, quantificateurs__"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "• Constantes : True, False\n",
    "\n",
    "• Connecteurs : ~ (non), ∧ (et), ∨ (ou), → (implique)\n",
    "\n",
    "• Quantificateurs : forall, exists"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    " A retenir ! - <span style=\"color:red\"> Logique intuitionniste : p → q n'est pas équivalent à : ~ p ∨ q </span>"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "• Logique d’ordre supérieur : on peut quantifier sur des\n",
    "fonctions et des prédicats"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Lemma bool_trivial : forall (P : bool -> Prop) b, P b -> P b.\n",
    "Admitted."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "__Remarque importante__ :\n",
    "Comme pour les fonctions qui reçoivent leurs arguments un par un\n",
    "et non un couple, les énoncés à plusieurs hypothèses utilisent\n",
    "plusieurs implications, plutôt que la conjonction."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Lemma bool_ext : forall (P : bool -> Prop), P true /\\ P false ->\n",
    "  forall b, P b.\n",
    "Admitted."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Lemma bool_ext2 : forall (P : bool -> Prop), P true -> P false ->\n",
    "  forall b, P b.\n",
    "Admitted."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Les prédicats inductifs"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "On a vu comment définir des types inductifs. De la même manière,\n",
    "on peut définir des prédicats inductifs (à la Prolog).\n",
    "\n",
    "Un peu de patience ...."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## <span style=\"color:blue\"> Preuve </span>"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Comment écrire la preuve d’un théorème ?\n",
    "\n",
    "• De manière interactive !\n",
    "\n",
    "• En s’appuyant sur un langage de tactiques permettant de\n",
    "transformer successivement le but actuel en un ou des buts plus simples à résoudre\n",
    "\n",
    "• Certaines tactiques de base ont une correspondance évidente dans le calcul des séquents ou en déduction naturelle (par ex. intros, split)\n",
    "\n",
    "• L’utilisateur peut définir des tactiques (par exemple une tactique qui enchaîne plusieurs tactiques de base)\n",
    "\n",
    "Prenons un exemple !"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Lemma andb_prop : forall b1 b2,\n",
    "  andb b1 b2 = true -> b1 = true /\\ b2 = true.\n",
    "Proof."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "intros b1 b2 H. (* introduit les hypothèses *)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "split. (* sépare le but en deux sous-buts *)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "  - destruct b1. (* raisonnement par cas *)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "    + reflexivity. (* true = true *)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "    + simpl in H. discriminate H. (* false <> true *)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "  - destruct b2. (* raisonnement par cas *)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "    + reflexivity. (* true = true *)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "    + destruct b1 .  (* raisonnement par cas *)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "      * simpl in H. discriminate H. (* false <> true *)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "      * simpl in H. discriminate H. (* false <> true *)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Qed."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Petite optimisation :"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Lemma andb_prop : forall b1 b2,\n",
    "andb b1 b2 = true -> b1 = true ∧ b2 = true.\n",
    "Proof.\n",
    "intros b1 b2 H. (* introduit les hypothèses *)\n",
    "split. (* sépare le but en deux sous-buts *)\n",
    "− destruct b1. (* raisonnement par cas *)\n",
    "+ reflexivity. (* true = true *)\n",
    "+ simpl in H. discriminate H. (* false <> true *)\n",
    "− destruct b2. (* raisonnement par cas *)\n",
    "+ reflexivity. (* true = true *)\n",
    "+ destruct b1; simpl in H; discriminate H.\n",
    "Qed."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Remarque : Au moins pour certaines preuves qui n’utilisent que des tactiques\n",
    "correspondant à des règles de logique (intuitionniste), on peut\n",
    "construire un arbre de preuve."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "__A vous de jouer maintenant !__"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Les prédicats inductifs"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "On a vu comment définir des types inductifs. De la même manière,\n",
    "on peut définir des prédicats inductifs (à la Prolog)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Inductive even : nat → Prop :=\n",
    "| even_0 : even 0 (* 0 est pair *)\n",
    "| even_SS : forall n, even n → even (S (S n)).\n",
    "(* si n est pair, n+2 est pair *)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "even_0 et even_SS sont les constructeurs de la définition\n",
    "inductive : ce sont des axiomes. On peut s’en servir pour prouver\n",
    "d’autres théorèmes.\n",
    "On peut alors exprimer d’autres théorèmes"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Theorem multiple_2_even : forall n, even (2 ∗ n)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Les prédicats inductifs (2/2)\n",
    "Autre exemple.\n",
    "Inductive In {A : Type} : A → list A → Prop :=\n",
    "| In_first : forall (x : A) (l : list A), In x (x :: l)\n",
    "| In_later : forall (x y : A) (l : list A), In x l → In x (y::l).\n",
    "Lemma In_app : forall {A : Type} (x : A) (l1 l2 : list A),\n",
    "In x (app l1 l2) → In x l1 ∨ In x l2.\n",
    "Paramètre et indice\n",
    "Dans la famille de types In A x l :\n",
    "• A est un paramètre, il est global aux constructeurs\n",
    "• x et l sont des indices, ils peuvent être instanciés\n",
    "différemment dans chaque constructeur"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Preuve et prédicat inductif\n",
    "Lemma even_4 : even 4.\n",
    "Proof.\n",
    "apply even_SS. apply even_SS. apply even_0.\n",
    "Qed.\n",
    "(* ou avec une syntaxe fonctionnelle*)\n",
    "Theorem even_4’ : even 4.\n",
    "Proof. apply (even_SS 2 (even_SS 0 even_0)).\n",
    "Qed.\n",
    "Theorem even_plus4 : forall n, even n → even (4 + n).\n",
    "Proof.\n",
    "intros n. simpl. intros Hn.\n",
    "apply even_SS. apply even_SS. apply Hn.\n",
    "Qed."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Inversion\n",
    "Supposons que l’on ait en hypothèse que n est un nombre pair\n",
    "( H : even n).\n",
    "Comment tirer partie de cette hypothèse ?\n",
    "Si on regarde la définition de even, cela peut vouloir dire 2 choses :\n",
    "• soit n est nul,\n",
    "• soit il existe un p tel que n est de la forme S (S p) et p est\n",
    "lui-même pair (hypothèse Hp)\n",
    "Analyse de cas : inversion H as [ p Hp].|"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Induction\n",
    "Theorem ev_minus2 : forall n,\n",
    "even n → even (pred (pred n)).\n",
    "Proof.\n",
    "intros n H.\n",
    "inversion H as [| p Hp].\n",
    "− (* H = even_0 *) simpl. apply even_0.\n",
    "− (* E = even_SS p Hp *) simpl. apply Hp.\n",
    "Qed.\n",
    "Theorem even5_nonsense :\n",
    "even 5 → 2 + 2 = 9.\n",
    "Proof.\n",
    "intro H.\n",
    "inversion H.\n",
    "inversion H1.\n",
    "inversion H3.\n",
    "Qed."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Induction\n",
    "Prouvons qu’ une propriété P n est vraie pour tous les entiers pairs.\n",
    "forall n, even n → P n.\n",
    "On peut faire cette preuve par induction sur (even n). Pour cela il\n",
    "faut montrer 2 choses qui correspondent aux 2 façons de former\n",
    "des nombres pairs.\n",
    "• 1er cas : n est nul (l’hypothèse a été construite avec even_0) :\n",
    "il faut montrer P 0.\n",
    "• 2ème cas : n est de la forme S (S k) avec k un nombre pair\n",
    "(l’hypothèse a été construite avec even_SS) : Il faut alors\n",
    "montrer P( S (S k)) avec l’hypothèse d’induction que la\n",
    "propriété P k est vraie."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Induction - exemple\n",
    "Lemma ev_even : forall n,\n",
    "even n → exists k, n = 2 ∗ k.\n",
    "Proof.\n",
    "intros n E.\n",
    "induction E as [|k Hk IH].\n",
    "− (* E = even_0 *)\n",
    "exists 0. reflexivity.\n",
    "− (* E = even_SS k Hk\n",
    "with IH : exists k’, n’ = double k’ *)\n",
    "destruct IH as [k’ Hk’].\n",
    ".....\n",
    "Qed."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "(** Exercice 2 *)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "(*\n",
    "   [andb_true_iff : forall b1 b2, andb b1 b2 = true <-> b1 = true /\\ b2 = true]\n",
    "    Montrer [orb_true_iff], un rÃ©sultat similaire sur [orb].  \n",
    " *)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Lemma plus_0_n : forall n, 0 + n = n.\n",
    "Proof.\n",
    "intro n. simpl. reflexivity.\n",
    "Qed."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Lemma plus_n_0 : forall n, n + O = n.\n",
    "Proof.\n",
    "induction n.\n",
    "+  simpl. reflexivity.\n",
    "+ simpl. rewrite IHn. reflexivity.\n",
    "Qed."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "(** Ecrire la multiplication pour les entiers *)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Fixpoint mult (n m : nat) :  nat :=\n",
    "  match n with\n",
    "  | O    => 0\n",
    "  | S n' => m + (mult n' m)\n",
    "  end."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Notation \"n * m\" := (mult n m)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "(** Prouver les lemmes suivants. *)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Lemma mult_0_n : forall n : nat, 0*n=0.\n",
    "Proof.\n",
    "intros. simpl. reflexivity.\n",
    "Qed."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Lemma mult_n_0 : forall n, n*0= 0.\n",
    "Proof.\n",
    "induction n.\n",
    "+  apply mult_0_n.\n",
    "+  simpl. exact IHn.\n",
    " (* ou assumption*)\n",
    "Qed."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Lemma plus_assoc : forall n m p,\n",
    "  n+(m+p) = n+m+p.\n",
    "Proof.\n",
    "induction n ; intros m p.\n",
    "+ simpl. reflexivity. \n",
    "+ simpl. rewrite IHn. reflexivity.\n",
    "Qed."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Lemma plus_n_Sm : forall n m,\n",
    "  n + S m = S (n + m).\n",
    "Proof.\n",
    "induction n ; intro m ; simpl.\n",
    "+ reflexivity.\n",
    "+ rewrite IHn. reflexivity.\n",
    "Qed."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Lemma plus_comm : forall n m, n+m=m+n.\n",
    "Proof.\n",
    "induction n ; intros m0.\n",
    "+ simpl. rewrite plus_n_0. reflexivity.\n",
    "+ simpl. rewrite IHn. rewrite plus_n_Sm. reflexivity.\n",
    "Qed."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Lemma mult_n_Sm : forall n m, n*S m=n+n*m.\n",
    "Proof.\n",
    "induction n ; intros m0 ; simpl.\n",
    "+ reflexivity.\n",
    "+ rewrite IHn.\n",
    "  do 2 (rewrite plus_assoc).\n",
    "  rewrite plus_comm with (n:=n) (m := m0). reflexivity.\n",
    "Qed."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Lemma mult_comm : forall n m, n *m=m*n.\n",
    "Proof.\n",
    "induction n ; intros m0 ; simpl.\n",
    "+ rewrite mult_n_0. reflexivity.\n",
    "+ rewrite IHn. rewrite mult_n_Sm.  reflexivity.\n",
    "Qed."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Lemma mult_plus_distr_r : forall n m p,\n",
    "  (n+m)*p = n*p+m*p.\n",
    "Proof.\n",
    "induction n ; intros m p; simpl.\n",
    "+ reflexivity.\n",
    "+ rewrite IHn. apply plus_assoc.\n",
    "Qed."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Lemma mult_assoc : forall n m p, n*(m*p) = (n*m)*p.\n",
    "Proof.\n",
    "induction n ; intros m p; simpl.\n",
    "+ reflexivity.\n",
    "+ rewrite IHn. rewrite mult_plus_distr_r. reflexivity. \n",
    "Qed."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "(* Prouver directement *)\n",
    "Lemma mult_plus_distr_l : forall n m p,\n",
    "  n*(m+p)=n*m+n*p.\n",
    "Proof.\n",
    "induction n; intros m p ; simpl.\n",
    "+ reflexivity.\n",
    "+ rewrite IHn. \n",
    "    rewrite plus_comm with (n:=p) (m:=n*p).\n",
    "    rewrite <- plus_assoc with (n:=m) (m:=n*m) (p:=n*p+p).\n",
    "    rewrite plus_comm with (n:=m) (m:=n*m + (n*p + p)).\n",
    "    do 2 (rewrite plus_assoc).\n",
    "    rewrite plus_comm with (n:=m) (m:=p).\n",
    "    rewrite <- plus_assoc with (n:=p + m) (m:=n*m) (p:=n*p).\n",
    "    rewrite plus_comm with (n:=p + m) (m:=n*m + n*p).\n",
    "    rewrite plus_assoc. reflexivity.\n",
    "Qed."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "(* Prouver en utilisant les lemmes precedents\n",
    "   (mais bien sur pas [mult_plus_distr_l]) *)\n",
    "Lemma mult_plus_distr_l_bis : forall n m p,\n",
    "  n*(m+p)=n*m+n*p.\n",
    "Proof.\n",
    "intros n m p.\n",
    "rewrite mult_comm with (n := n) (m := m).\n",
    "rewrite mult_comm with (n := n) (m := p).\n",
    "rewrite <- mult_plus_distr_r.\n",
    "apply mult_comm.\n",
    "Qed."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "End nat_bool.\n",
    "\n",
    "\n",
    "(* On ferme le module.  nat_bool est de nouveau par defaut le type des entiers naturels de la bibliotheque standard de Coq. *)\n",
    "\n",
    "(** Remarque : tous les resultats demontres dans cet exercice sont disponibles\n",
    "    dans la bibliotheque [Arith], ([Require Import Arith]) *)\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "(** * Exercice 3. *)\n",
    "(** Prouver les resultats suivants. *)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Lemma impl_and : forall P Q R : Prop, (P->Q->R) -> (P /\\ Q -> R).\n",
    "Proof.\n",
    "intros P Q R Hyp1 Hyp2.\n",
    "destruct Hyp2 as [Hp Hq].\n",
    "apply Hyp1 ; assumption.\n",
    "Qed."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Lemma and_impl : forall P Q R : Prop, (P /\\ Q -> R) -> (P -> Q -> R).\n",
    "Proof.\n",
    "intros P Q R Hyp1 H1 H2.\n",
    "apply Hyp1.\n",
    "split ; assumption.\n",
    "Qed."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Lemma and_impl_iff : forall P Q R : Prop, (P /\\ Q -> R) <-> (P -> Q -> R).\n",
    "Proof.\n",
    "split.\n",
    "+ apply and_impl.\n",
    "+ apply impl_and.\n",
    "Qed."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Lemma impl_not : forall P : Prop, P -> ~ ~ P.\n",
    "Proof.\n",
    "intros P Hyp.\n",
    "unfold not.\n",
    "intro Hyp1.\n",
    "apply Hyp1.\n",
    "assumption.\n",
    "Qed."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Lemma modus_ponens : forall P Q : Prop, P -> (P -> Q) -> Q.\n",
    "Proof.\n",
    "intros P Q H1 H2.\n",
    "apply H2.\n",
    "assumption.\n",
    "Qed."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "(* en utilisant [modus_ponens] *)\n",
    "Lemma impl_not_bis : forall P : Prop, P -> ~ ~ P.\n",
    "Proof.\n",
    "intro P. unfold not.\n",
    "apply modus_ponens.\n",
    "Qed."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "(* a partir de [impl_not] *)\n",
    "Lemma P_notP_contradiction : forall P : Prop, ~ (P /\\ ~ P).\n",
    "Proof.\n",
    "intro P.\n",
    "unfold not .\n",
    "(*apply impl_and.\n",
    "apply modus_ponens.*)\n",
    "intro H1.\n",
    "destruct H1 as [HH1 HH2].\n",
    "apply HH2. assumption.\n",
    "Qed."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Lemma not_and : forall P Q : Prop, P \\/ Q -> ~(~ P /\\ ~Q).\n",
    "Proof.\n",
    "Admitted."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Lemma exists_not_forall : forall P : nat -> Prop, \n",
    "(exists n, P n) ->  ~(forall n,~ (P n)).\n",
    "Proof.\n",
    "intros P H H1. \n",
    "destruct H as [n0 H0].\n",
    "specialize (H1 n0).\n",
    "contradiction.\n",
    "Qed."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "(** * Exercice 4. *)\n",
    "Module Liste. (*idem pour définir les listes san cacher celles de la \n",
    "bibliothèque standard *)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Variable A : Set. (* A est ici un type abstrait *)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "(* on définit le type des listes dont les éléments sont de types A*)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Inductive list : Set :=\n",
    "| nil : list \n",
    "| cons : A -> list -> list."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Check list."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Notation \"[]\" := nil."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Notation \"[ x ]\" := (cons x nil)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Notation \"[ x ; y ; .. ; z ]\" := (cons x (cons y .. (cons z nil) ..)).\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "(* Définir la fonction length qui compte les éléments d'une liste\n",
    "\tet la fonction app qui concatene deux listes- montrer que le\n",
    "\tnombre d'elements de la concatenation de deux listes est la somme\n",
    "\tdes nombres des éléments de chacune *)\n",
    "\n",
    "(* Définir la fonction qui renverse une liste (on utilisera la fonction prÃ©cÃ©dente app)\n",
    " et  montrer que reverse(reverse l) = l pour tout l, par induction sur l*)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "End Liste."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Require Import List.\n",
    "Require Import Arith."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Check list.\n",
    "Print list. (* on retrouve les listes et les naturels de la bibliothèque standard*)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "(** Exercice 5 *)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Definition is_even n := exists p, n = 2 * p."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Lemma zero_is_even : is_even 0.\n",
    "Proof.\n",
    "unfold is_even.\n",
    "exists 0. simpl. reflexivity.\n",
    "Defined."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Lemma is_even_plus : forall n p, \n",
    "   is_even n -> is_even p -> is_even (n + p).\n",
    "Proof.\n",
    "intros n p Hn Hp.\n",
    "unfold is_even in Hn.\n",
    "destruct Hn as [k Hk].\n",
    "destruct Hp as [t Ht].\n",
    "unfold is_even.\n",
    "exists (k + t).\n",
    "rewrite  mult_plus_distr_l.\n",
    "rewrite Hk.  rewrite Ht. reflexivity.\n",
    "Qed. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "(** * Exercice 5. *)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "(** On rappelle la définition de [even] sous forme d'un predicat inductif . *)\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Inductive even : nat -> Prop :=\n",
    "| even_0 : even 0\n",
    "| even_SS : forall n, even n -> even (S (S n))."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Lemma even_4 : even 4.\n",
    "Proof.\n",
    "apply even_SS. apply even_SS. apply even_0.\n",
    "Qed."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "(* ou avec une syntaxe fonctionnelle*)\n",
    "Theorem even_4' : even 4.\n",
    "Proof. exact (even_SS 2 (even_SS 0 even_0)).\n",
    "Qed."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Theorem even_plus4 : forall n, even n -> even (4 + n).\n",
    "Proof.\n",
    "  intros n. simpl. intros Hn.\n",
    "  apply even_SS. apply even_SS. assumption.\n",
    "Qed."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Theorem ev_minus2 : forall n,\n",
    "  even n -> even (pred (pred n)).\n",
    "Proof.\n",
    "  intros n H.\n",
    "  inversion H  as [| p Hp].\n",
    "  - (* H = even_0 *) simpl. apply even_0.\n",
    "  - (* H = even_SS p Hp *) simpl. exact Hp (* ou assumption*).\n",
    "Qed."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Theorem even5_nonsense :\n",
    "  even 5 -> 2 + 2 = 9.\n",
    "Proof.\n",
    "  intro H.\n",
    "  inversion H. \n",
    "  inversion H1.\n",
    "  inversion H3.\n",
    "Qed."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Lemma ev_even : forall n,\n",
    "  even n -> exists k, n = 2 * k.\n",
    "Proof.\n",
    "  intros n E.\n",
    "  induction E as [|k Hk IH].\n",
    "  - (* E = even_0 *)\n",
    "    exists 0. reflexivity.\n",
    "  - (* E = even_SS k Hk\n",
    "       with IH : exists k', n' = double k' *)\n",
    "    destruct IH as [k' Hk'].\n",
    "    rewrite Hk'. exists (S k'). simpl.\n",
    "    Search plus.\n",
    "    rewrite <- plus_n_Sm.\n",
    "    replace (k' + 0) with k'. reflexivity.\n",
    "    apply plus_n_O.\n",
    "Qed."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "(** Prouver les lemmes suivants. *)\n",
    "\n",
    "Lemma even_n_or_Sn : forall n, even n \\/ even (S n).\n",
    "Proof.\n",
    "Admitted."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Lemma even_n_not_Sn : forall n, even n -> ~ even (S n).\n",
    "Proof.\n",
    "Admitted."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Lemma even_dec : forall n, even n \\/ ~ even n.\n",
    "Proof.\n",
    "Admitted."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "(** Induction de 2 en 2. *)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Lemma two_steps_induction : forall P : nat -> Prop, P 0 -> P 1 ->\n",
    "  (forall n, P n -> P (S (S n))) ->\n",
    "  forall n, P n.\n",
    "Proof.\n",
    "  intros P H0 H1 IHn.\n",
    "  assert (forall n, P n /\\ P (S n)) as Hn.\n",
    "Admitted."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "(** DÃ©finir [evenb : nat -> bool] qui teste si un entier est pair. *)\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Fixpoint evenb (n:nat) : bool.\n",
    "Admitted."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "(** Prouver les lemmes suivants. Si vous avez besoin de résultats sur les\n",
    "    booléens, vous pouvez les trouver dans [Bool]\n",
    "    (utiliser [Require Import Bool.]).\n",
    "*)\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Lemma evenb_correct : forall n, evenb n = true -> even n.\n",
    "Proof.\n",
    "Admitted."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Lemma evenb_complete : forall n, even n -> evenb n = true.\n",
    "Proof.\n",
    "Admitted."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Definition evenb_spec : forall n, evenb n = true <-> even n.\n",
    "Proof.\n",
    "Admitted."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "(** Prouver [even_dec_bis : forall n, even n \\/ ~ even n]\n",
    "    en utilisant [evenb_spec]. *)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Lemma even_dec_bis : forall n, even n \\/ ~ even n.\n",
    "Proof.\n",
    "Admitted."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "(** Exercice 6 *)\n",
    "(** retour des listes *)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Variable A : Type."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Inductive mem : A -> list A -> Prop :=\n",
    "  mem_head : forall x l, mem x (cons x l)\n",
    "| mem_tail : forall x y l, \n",
    "   mem x l -> mem x (cons y l).\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Check app."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Print app."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Lemma app_left : forall l1 l2 x,\n",
    "mem x l1 -> mem x (app l1 l2).\n",
    "Proof.\n",
    "Admitted."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Lemma app_or : forall l1 l2 x, mem x (app l1 l2) -> mem x l1 \\/ mem x l2.\n",
    "Proof.\n",
    "Admitted."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "__Tactiques pour manipuler les types inductifs__\n",
    "\n",
    "• destruct x pour une analyse par cas de x\n",
    "\n",
    "• discriminate pour utiliser la disjonction des constructeurs\n",
    "\n",
    "• injection H pour utiliser l’injection des constructeurs dans H\n",
    "\n",
    "• inversion H ' destruct H, mais plus pour les prédicats\n",
    "\n",
    "• induction H ' destruct H avec hypothèse d’induction\n",
    "\n",
    "• constructor pour appliquer un constructeur du type de la\n",
    "conclusion"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "__Pour manipuler la logique__\n",
    "\n",
    "• intros pour introduire les variables quantifiées universellement\n",
    "\n",
    "• exists x pour donner la valeur témoin attendue\n",
    "\n",
    "• split pour détruire un but en plusieurs sous-buts\n",
    "\n",
    "• left, right pour choisir une branche d’une disjonction\n",
    "\n",
    "• reflexivity pour utiliser la réflexivité de l’égalité\n",
    "\n",
    "• symmetry pour utiliser la symétrie de l’égalité\n",
    "\n",
    "• contradiction si les hypothèses contiennent False ou P et ~P"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "__Autres__\n",
    "\n",
    "• exact H lorsque l’hypothèse H et le but actuel sont identiques\n",
    "\n",
    "• assumption pour chercher dans les hypothèses\n",
    "\n",
    "• apply H pour appliquer H dont la conséquence est la\n",
    "conclusion actuelle\n",
    "\n",
    "• rewrite [← ] H pour récrire en utilisant l’égalité H\n",
    "\n",
    "• replace x with y pour remplacer x par y en prouvant x=y\n",
    "\n",
    "• subst x pour éliminer x en utilisant les égalités disponibles\n",
    "\n",
    "• assert H as Ha pour introduire un lemme intermédiaire H\n",
    "pendant la preuve\n",
    "\n",
    "• specialize (H x) pour appliquer partiellement une hypothèse\n",
    "\n",
    "• pose proof lem as H pour ajouter un théorème aux hypothèses\n",
    "\n",
    "• simpl pour simplifier des termes\n",
    "\n",
    "• unfold f pour remplacer f par sa définition"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.7.3"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 4
}