{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Ensembles héréditairement finis (I)\n",
    "\n",
    "Marc Lorenzi\n",
    "\n",
    "3 novembre 2021"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "import matplotlib.pyplot as plt\n",
    "import math"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**Notations.** Nous utiliserons dans ce notebook les notations pas tout à fait standard suivantes.\n",
    "\n",
    "- Pour tout ensemble fini $A$, $|A|$ dénote le cardinal de $A$.\n",
    "- Étant donnés deux ensembles $A$ et $B$, on note $A\\subseteq B$ si $A$ est inclus dans $B$. On note $A\\subset B$ si $A$ est inclus dans $B$ *et* différent de $B$.\n",
    "- Étant donnés un ensemble $A$ et une propriété $P$, $\\{x\\in A:P(x)\\}$ est l'ensemble des éléments de $A$ qui vérifient $P$.\n",
    "- Étant donnés un ensemble $A$ et une fonction $f$, $\\{f(x):x\\in A\\}$ est l'ensemble des images par $f$ des éléments de $A$."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**Avertissement.** Nous allons manipuler dans ce notebook des ensembles d'ensembles d'ensembles, etc. Pour des raisons de clarté et de simplicité, nous représenterons ces objets en Python par des listes de listes de listes, etc. Les fonctions qui en résulteront auront parfois une complexité (en nombre d'opérations à effectuer) qui pourrait être grandement améliorée, au prix d'un obscurcissement du code. Dans la suite, je me contenterai par-ci par-là de quelques remarques sur la complexité des fonctions écrites, sans pour autant entrer dans les détails."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## 1. Introduction"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 1.1 Ensembles héréditairement finis"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "On pose $V_0=\\emptyset$ et pour tout $n\\in\\mathbb N$, $V_{n+1}=\\mathcal P(V_n)$, l'ensemble des parties de $V_n$. On définit enfin\n",
    "\n",
    "$$V=\\bigcup_{n\\in\\mathbb N}V_n$$\n",
    "\n",
    "Les ensembles appartenant à $V$ sont les ensembles *héréditairement finis*.\n",
    "\n",
    "Par exemple, $\\emptyset$, $\\{\\emptyset\\}$, $\\{\\emptyset, \\{\\emptyset\\}\\}$, $\\{\\{\\{\\emptyset\\}\\}\\}$, sont des ensembles héréditairement finis.\n",
    "\n",
    "**L'objet de ce notebook et des suivants est l'étude des propriétés de $V$ et de ses éléments.**"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**Remarque.** Pour tout $n\\in\\mathbb N$, $V_n\\subseteq V_n$, donc $V_n\\in\\mathcal P(V_{n})=V_{n+1}\\subseteq V$. Ainsi, $V_n\\in V$ est un ensemble héréditairement fini.\n",
    "\n",
    "**Mise en garde.** *Dans ce qui va suivre, on demande au le lecteur de faire encore plus attention que d'habitude à la différence entre $\\in$ et $\\subseteq$.*"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 1.2 Le cardinal de $V_n$"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Pour tout $x\\in\\mathbb R$, définissons par récurrence sur $n$ le réel $x^{\\uparrow n}$ en posant $x^{\\uparrow 0}=0$ et pour tout $n\\in\\mathbb N$, $x^{\\uparrow n+1}=x^{\\left(x^{\\uparrow^n}\\right)}$. On a ainsi $x^{\\uparrow 1}=1$, $x^{\\uparrow 2}=x$, $x^{\\uparrow 3}=x^x$, etc. Plus généralement, pour tout $n\\ge 2$,\n",
    "\n",
    "$$x^{\\uparrow n}=x^{x^{x^{}\\ldots{{}^ x}}}$$\n",
    "\n",
    "où le nombre $x$ apparaît $n-1$ fois dans l'expression. \n",
    "\n",
    "**Proposition.** Pour tout $n\\in\\mathbb N$, $V_n$ est un ensemble fini et son cardinal est $|V_n|=2^{\\uparrow n}$.\n",
    "\n",
    "**Démonstration.** C'est une récurrence facile. Il suffit d'écrire que $|V_{n+1}|=|\\mathcal P(V_n)|=2^{|V_n|}$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def ppow(a, n):\n",
    "    p = 0\n",
    "    for k in range(n):\n",
    "        p = a ** p\n",
    "    return p"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Voici le cardinal des premiers ensembles $V_n$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "for k in range(6):\n",
    "    print(k, ppow(2, k))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Remarquons que $|V_6|=2^{65536}\\simeq 10^{19728}$ et que personne ne verra donc jamais $V_6$."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**Remarque.** Pour tout $n\\in \\mathbb N$, $2^n\\ge n+1$. De là,\n",
    "\n",
    "$$|V_{n+1}|=2^{|V_n|}\\ge |V_n|+1$$\n",
    "\n",
    "d'où\n",
    "\n",
    "$$|V_{n+1}|>|V_n|$$\n",
    "\n",
    "La suite $(|V_n|)_{n\\in\\mathbb N}$ est ainsi strictement croissante. La croissance de $|V_n|$ est extrêmement rapide : une récurrence montre que pour tout $n\\in\\mathbb N$, $|V_n|\\ge n$. De là, pour tout $n\\ge 1$,\n",
    "\n",
    "$$|V_n|=2^{|V_{n-1}|}\\ge 2^{n-1}$$\n",
    "\n",
    "et donc, pour tout $n\\ge 2$, \n",
    "\n",
    "$$|V_n|=2^{|V_{n-1}|}\\ge 2^{2^{n-2}}$$\n",
    "\n",
    "etc.\n",
    "\n",
    "En corollaire, $V$ est un ensemble infini puisqu'il contient des sous-ensembles de cardinaux non majorés. Nous verrons plus loin que l'ensemble $V$ est *dénombrable*, en écrivant une bijection explicite de $V$ sur $\\mathbb N$."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**Proposition.** Pour tout $n\\in\\mathbb N$, $V_n\\subset V_{n+1}$.\n",
    "\n",
    "**Démonstration.** Montrons cette propriété par récurrence sur $n$. \n",
    "\n",
    "- C'est clair pour $n=0$, puisque $V_0=\\emptyset\\subset V_1=\\{\\emptyset\\}$.\n",
    "- Soit $n\\in\\mathbb N$. Supposons $V_n\\subset V_{n+1}$. Soit $A\\in V_{n+1}$. On a donc $A\\in\\mathcal P(V_n)$, c'est à dire $A\\subseteq V_n$. Ainsi, pour tout $x\\in A$, $x\\in V_n$ et, par l'hypothèse de récurrence, $x\\in V_{n+1}$. De là, $A\\subseteq V_{n+1}$ et donc $A\\in\\mathcal P(V_{n+1})=V_{n+2}$. \n",
    "\n",
    "Enfin, $V_{n+1}\\ne V_{n+2}$ car ces deux ensembles ont des cardinaux distincts. $\\square$"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**Corollaire.** Soit $n\\in\\mathbb N$. Soit $A\\in V_n$. Alors, $A\\subseteq V_n$.\n",
    "\n",
    "**Démonstration.** Comme $V_n\\subset V_{n+1}$, on a $A\\in V_{n+1}=\\mathcal P(V_{n})$ et donc $A\\subseteq V_n$. $\\square$\n",
    "\n",
    "Nous reviendrons dans le prochain notebook sur cette propriété de $V_n$ qui s'appelle la *transitivité*.\n",
    "\n",
    "**Corollaire.** Soit $A\\in V$. Pour tout $x\\in A$, $x\\in V$.\n",
    "\n",
    "Dit autrement, les éléments d'un ensemble héréditairement fini sont des ensembles héréditairement finis. Et donc, en réutilisant cette propriété, les éléments des éléments d'un ensemble héréditairement fini sont des ensembles héréditairement finis, etc."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 1.3 Rang d'un ensemble héréditairement fini"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**Définition.** Pour tout $A\\in V$, le *rang* de $A$ est le plus petit entier $n$ tel que $A\\in V_{n+1}$. \n",
    "\n",
    "Par exemple, $\\text{rg }\\emptyset=0$, $\\text{rg }\\{\\emptyset\\}=1$, $\\text{rg }\\{\\emptyset,\\{\\emptyset\\}\\}=\\text{rg }\\{\\{\\emptyset\\}\\}=2$.\n",
    "\n",
    "Comme $V_0\\subseteq V_1\\subseteq V_2\\subseteq\\ldots$, si $n=\\text{rg }A$ alors\n",
    "\n",
    "- Pour tout $k\\le n$, $A\\not\\in V_k$.\n",
    "- Pour tout $k\\ge n+1$, $A\\in V_k$.\n",
    "\n",
    "Le rang de $A$ est donc l'unique entier naturel $n$ tel que $A\\in V_{n+1}$ et $A\\not\\in V_n$.\n",
    "\n",
    "**Proposition.** Pour tout ensemble $A\\in V$ non vide, $\\text{rg }A =\\max\\{\\text{rg }x: x\\in A\\}+1$.\n",
    "\n",
    "**Démonstration.** Soit $A\\in V$. Soit $n=\\text{rg }A$. On a $A\\in V_{n+1}=\\mathcal P(V_n)$ donc $A\\subseteq V_n$. Ainsi, pour tout $x\\in A$, $x\\in V_n$ et donc $\\text{rg }x\\le n-1$. De plus, $A\\not\\in V_n$, donc $A\\not \\subseteq V_{n-1}$. Il existe donc $x\\in A$ tel que $x\\not \\in V_{n-1}$, c'est à dire tel que $\\text{rg }x\\ge n-1$. $\\square$\n",
    "\n",
    "**Corollaire.** Soient $A,B\\in V$ tels que $A\\in B$. On a $\\text{rg }A<\\text{rg }B$.\n",
    "\n",
    "**Proposition.** Soit $A$ un ensemble. On a $A\\in V$ si et seulement si $A$ est fini et $A\\subseteq V$.\n",
    "\n",
    "**Démonstration.** Supposons $A\\in V$. Soit $n=\\text{rg A}$. Alors $A\\in V_{n+1}=\\mathcal P(V_n)$ donc $A\\subseteq V_n\\subseteq V$. De plus, comme $V_n$ est fini, $A$ l'est aussi.\n",
    "\n",
    "Inversement, supposons $A$ fini et inclus dans $V$. Soit $n=\\max\\{\\text{rg }x:x\\in A\\}$. Pour tout $x\\in A$, $x\\in V_{n+1}$ donc $A\\subseteq V_{n+1}$, donc $A\\in \\mathcal P(V_{n+1})=V_{n+2}\\subseteq V$. Ainsi, $A\\in V$. $\\square$"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**Remarque.** Soit $n\\ge 1$. Soient $A_1,\\ldots,A_n\\in V$. Supposons $A_1\\in A_2\\ldots\\in A_n$. On a alors\n",
    "\n",
    "$$\\text{rg }A_1<\\ldots<\\text{rg }A_n$$\n",
    "\n",
    "et donc $A_n\\not\\in A_1$. La relation d'appartenance ne comporte pas de « cycles ». En particulier, en prenant $n=1$ et $n=2$, on obtient que\n",
    "\n",
    "- Pour tout $A\\in V$, $A\\not\\in A$.\n",
    "- Pour tous $A,B\\in V$, $A\\in B\\implies B\\not\\in A$.\n",
    "\n",
    "La relation $\\in$ est donc *irréflexive* et *asymétrique* sur $V$. Il ne lui manque que la *transitivité* pour être une relation d'ordre strict. Nous reviendrons sur ce sujet dans le notebook suivant."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**Proposition.** Pour tout $n\\in\\mathbb N$, $\\text{rg }V_n=n+1$.\n",
    "\n",
    "**Démonstration.** On a $V_n\\in V_{n+1}$ et $V_n\\not\\in V_n$. $\\square$"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 1.4 Une bijection de $V$ sur $\\mathbb N$"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "La bijection que nous allons décrire ici est due à Wilhelm Ackermann.\n",
    "\n",
    "Soit $\\varphi:V\\longrightarrow \\mathbb N$ définie pour tout $A\\in V$ par \n",
    "\n",
    "$$\\varphi(A)=\\sum_{x\\in A}2^{\\varphi(x)}$$\n",
    "\n",
    "Une récurrence forte sur $\\text{rg }A$ montre que cette fonction est bien définie.\n",
    "\n",
    "**Proposition.** Pour tout $n\\in\\mathbb N$, $\\varphi$ est une bijection de $V_n$ sur $[\\![0,2^{\\uparrow n}-1]\\!]$.\n",
    "\n",
    "**Démonstration.** Faisons une récurrence sur $n$. \n",
    "\n",
    "- C'est clair pour $n=0$ puisque $V_0=\\emptyset$. \n",
    "- Soit $n\\in\\mathbb N$. Supposons la propriété vérifiée pour $n$. \n",
    "\n",
    "Montrons tout d'abord que $\\varphi$ envoie $V_{n+1}$ dans $[\\![0,2^{\\uparrow n+1}-1]\\!]$. Soit $A\\in V_{n+1}$. On a  $\\text{rg }A\\le n$. Les éléments de $A$ sont donc de rang inférieur ou égal à $n-1$, et appartiennent ainsi à $V_n$. De là,\n",
    "\n",
    "$$\\varphi(A)=\\sum_{x\\in A}2^{\\varphi(x)}\\le \\sum_{x\\in V_n} 2^{\\varphi(x)}$$\n",
    "\n",
    "Par l'hypothèse de récurrence, $\\varphi$ est une bijection de $V_n$ sur $[\\![0,2^{\\uparrow n}-1]\\!]$. On a donc\n",
    "\n",
    "$$\\sum_{x\\in V_n} 2^{\\varphi(x)}=\\sum_{k=0}^{2^{\\uparrow n}-1}2^k=2^{2^{\\uparrow n}}-1=2^{\\uparrow n+1}-1$$\n",
    "\n",
    "Montrons maintenant l'injectivité de $\\varphi$. Soient $A, B\\in V_{n+1}$. Supposons $\\varphi(A)=\\varphi(B)$. On a donc\n",
    "\n",
    "$$\\sum_{x\\in A}2^{\\varphi(x)}=\\sum_{x\\in B}2^{\\varphi(x)}$$\n",
    "\n",
    "Par les propriétés de l'écriture des entiers en base 2, les exposants des deux membres sont les mêmes :\n",
    "\n",
    "$$\\{\\varphi(x):x\\in A\\}=\\{\\varphi(x):x\\in B\\}$$\n",
    "\n",
    "Les éléments de $A$ et $B$ appartiennent à $V_n$ et $\\varphi$ est, par l'hypothèse de récurrence, injective sur $V_n$.  On a donc\n",
    "\n",
    "$$\\{x:x\\in A\\}=\\{x:x\\in B\\}$$\n",
    "\n",
    "Bref, $A=B$.\n",
    "\n",
    "Pour conclure, $\\varphi$ envoie injectivement $V_{n+1}$ dans $[\\![0,2^{\\uparrow n+1}-1]\\!]$. Or, ces deux ensembles ont le même cardinal. Il y a donc aussi surjectivité. $\\square$"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**Corollaire.** $\\varphi$ est une bijection de $V$ sur $\\mathbb N$.\n",
    "\n",
    "**Démonstration.** Montrons l'injectivité. Soient $A, B\\in V$. Supposons $\\varphi(A)=\\varphi(B)$. Soit $n=\\max(\\text{rg }A, \\text{rg }B)$. On a $A,B\\in V_{n+1}$. Or, $\\varphi$ est injective sur $V_{n+1}$, donc $A=B$.\n",
    "\n",
    "Montrons la surjectivité. Soit $n\\in\\mathbb N$. Il existe un entier $r\\in\\mathbb N$ tel que $2^{\\uparrow r}>n$ (par exemple, $r=n$). Comme $\\varphi$ est une surjection de $V_r$ sur $[\\![0,2^{\\uparrow r}-1]\\!]$, il existe $A\\in V_r$ tel que $n=\\varphi(A)$. $\\square$"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**Proposition.** Pour tout $n\\in\\mathbb N$, $\\varphi(V_n)=2^{n+1}-1$.\n",
    "\n",
    "**Démonstration.** On a\n",
    "\n",
    "$$V_n=\\{x\\in V:\\varphi(x)\\le 2^{\\uparrow n}-1\\}$$\n",
    "\n",
    "\n",
    "De là,\n",
    "\n",
    "$$\\varphi(V_n)=\\sum_{x\\in V_n}2^{\\varphi(x)}=\\sum_{k=0}^{2^{\\uparrow n}-1}2^{k}=2^{2^{\\uparrow n>}}-1=2^{\\uparrow n+1}-1$$"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Une convention Python"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**Convention.** Nous représenterons un élément de $V$ en Python par la liste de ses éléments, **ordonnés dans l'ordre croissant de leurs images par $\\varphi$.**"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Remarquons que par cette convention il est facile d'obtenir le rang d'un ensemble. En effet, pour tout $A\\in V$ non vide, on a \n",
    "\n",
    "$$\\text{rg }A =\\max\\{\\text{rg }x: x\\in A\\}+1$$\n",
    "\n",
    "Avec notre convention, $\\text{rg }\\{x_1,\\ldots,x_n\\}=1+\\text{rg }x_n$. Il est donc immédiat d'écrire une fonction `rang` qui renvoie le rang d'un ensemble $A\\in V$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def rang(A):\n",
    "    k = 0\n",
    "    while A != []:\n",
    "        A = A[-1]\n",
    "        k = k + 1\n",
    "    return k"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "La fonction `phi` ci-dessous renvoie $\\varphi(A)$ pour tout $A\\in V$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def phi(A):\n",
    "    n = 0\n",
    "    for x in A:\n",
    "        n = n + 2 ** phi(x)\n",
    "    return n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Avant de faire des tests, décrivons la réciproque de $\\varphi$."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 1.5 La réciproque de $\\varphi$"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Nous noterons $\\psi$ la réciproque de $\\varphi$.\n",
    "\n",
    "**Proposition.** Pour tout $n\\in\\mathbb N$, $\\psi(n)=\\{\\psi(m):m\\prec n\\}$ où $m\\prec n$ si et seulement si le $m$ième chiffre de $n$ en base 2 est un 1. \n",
    "\n",
    "**Démonstration.** Soit $n\\in\\mathbb N$. Soit $A=\\psi(n)$. On a\n",
    "\n",
    "$$n=\\varphi(A)=\\sum_{x\\in A}2^{\\varphi(x)}$$\n",
    "\n",
    "Par ailleurs,\n",
    "\n",
    "$$n=\\sum_{m\\prec n}2^{m}$$\n",
    "\n",
    "Par unicité de l'écriture de $n$ en base 2, on a donc pour tout $x\\in V$, $x\\in A\\iff \\varphi(x)\\prec n$. Ainsi, pour tout $m\\in\\mathbb N$, $\\psi(m)\\in A\\iff m\\prec n$, d'où\n",
    "\n",
    "$$A=\\{\\psi(m): m\\prec n\\}\\ \\square$$"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def psi(n):\n",
    "    s = []\n",
    "    m = 0 \n",
    "    while n != 0:\n",
    "        if n % 2 == 1: s.append(psi(m))\n",
    "        n = n // 2\n",
    "        m = m + 1\n",
    "    return s"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Nous pouvons maintenant effectuer quelques tests sur les fonctions $\\varphi$ et $\\psi$. Listons d'abord les premiers ensembles héréditairement finis."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "for n in range(10):\n",
    "    print(n, psi(n))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Vérifions que $\\varphi$ et $\\psi$ sont bien réciproques l'une de l'autre."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(phi(psi(123456789123456789)))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Comme $\\varphi(V_n)=2^{\\uparrow n+1}-1$, il est maintenant facile d'obtenir $V_n$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def V(n):\n",
    "    return psi(ppow(2, n + 1) - 1)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Voici $V_4$, qui a 16 éléments."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(V(4))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "$V_5$ a déjà $2^{16}=65536$ éléments. Ce ne serait pas une bonne idée de demander à Python de l'afficher."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 1.6 Une relation d'ordre sur $V$"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Définissons une relation $\\le$ sur $V$ en posant, pour tous $A,B\\in V$,\n",
    "\n",
    "$$A\\le B\\iff \\varphi(A)\\le \\varphi(B)$$\n",
    "\n",
    "On note évidemment $A< B$ si $A\\le B$ et $A\\ne B$. Comme $\\varphi$ est bijective et que $(\\mathbb N, \\le)$ est bien ordonné, la relation $\\le$ est elle-même un bon ordre sur $V$.\n",
    "\n",
    "Remarquons que notre convention pour représenter les ensembles héréditairement finis en Python devient : **on représente les éléments de $V$ en Python par la liste de leurs éléments dans l'ordre strictement croissant.**"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**Proposition.** Soient $A, B\\in V$ non vides. On a \n",
    "\n",
    "$$A\\le B\\iff (\\max A < \\max B)\\lor(\\max A=\\max B\\land A\\setminus\\{\\max A\\}\\le B\\setminus\\{\\max B\\})$$\n",
    "\n",
    "**Démonstration.** Notons $x=\\max A$ et $y=\\max B$. On a\n",
    "\n",
    "$$\\varphi(A)=2^{\\varphi(x)}+ \\sum_{t\\in A, t\\ne x}2^{\\varphi(t)}$$\n",
    "\n",
    "et\n",
    "\n",
    "$$\\varphi(B)=2^{\\varphi(y)}+ \\sum_{t\\in B, t\\ne y}2^{\\varphi(t)}$$\n",
    "\n",
    "- Si $\\varphi(x)<\\varphi(y)$, les propriétés de la représentation des entiers en base 2 montrent que $\\varphi(A)<\\varphi(B)$.\n",
    "- Si $\\varphi(x)>\\varphi(y)$, on a de même $\\varphi(B)<\\varphi(A)$.\n",
    "- Si $\\varphi(x)=\\varphi(y)$, on a $\\varphi(A)\\le \\varphi(B)$ si et seulement si\n",
    "\n",
    "$$\\sum_{t\\in A, t\\ne x}2^{\\varphi(t)}\\le \\sum_{t\\in B, t\\ne y}2^{\\varphi(t)}$$\n",
    "\n",
    "c'est à dire si et seulement si $A\\setminus\\{x\\}\\le B\\setminus\\{y\\}$. $\\square$"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "La fonction `inferieur_strict` prend en paramètres deux ensembles $A,B\\in V$. Elle renvoie `True` si $A<B$ et `False` sinon."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def inferieur_strict(A, B):\n",
    "    if A == []: return B != []\n",
    "    elif B == []: return False\n",
    "    else:\n",
    "        return inferieur_strict(A[-1], B[-1]) or (A[-1] == B[-1] and inferieur_strict(A[:-1], B[:-1]))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "inferieur_strict(psi(12345), psi(12344))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "inferieur_strict(psi(12344), psi(12345))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## 2 Deux familles d'éléments de $V$ "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 2.1 Les entiers de von Neumann"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "On définit par récurrence sur $n$ le $n$ième *entier de von Neumann* en posant \n",
    "\n",
    "- $\\overline 0=\\emptyset$\n",
    "- Pour tout $n\\in\\mathbb N$, $\\overline{n+1}=\\overline n\\cup\\{\\overline n\\}$. \n",
    "\n",
    "On a donc pour tout $n\\in\\mathbb N$, $\\overline n=\\{\\overline 0,\\ldots,\\overline{n-1}\\}$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def neumann(n):\n",
    "    u = []\n",
    "    for k in range(n):\n",
    "        u = u + [u]\n",
    "    return u"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "for n in range(5):\n",
    "    print(n, neumann(n))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**Proposition.** Pour tout $n\\in\\mathbb N$, $|\\overline n|=\\text{rg }\\overline n=n$.\n",
    "\n",
    "**Démonstration.** Récurrence facile. $\\square$"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(rang(neumann(20)))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Définissons par récurrence forte sur $n$ une suite $(\\nu_n)_{n\\in\\mathbb N}$ en posant pour tout $n\\in\\mathbb N$, \n",
    "\n",
    "$$\\nu_n=\\sum_{k=0}^{n-1}2^{\\nu_k}$$\n",
    "\n",
    "Remarquons que l'on a $\\nu_0=0$ et pour tout $n\\ge 1$, \n",
    "\n",
    "$$\\nu_{n+1}=2^{\\nu_n}+\\nu_n$$\n",
    "\n",
    "**Proposition.** Pour tout $n\\in\\mathbb N$, $\\varphi(\\overline n)=\\nu_n$.\n",
    "\n",
    "**Démonstration.** On fait une récurrence forte sur $n$. La propriété est vraie pour $n=0$. Soit $n\\ge 1$. Supposons que pour tout $k<n$, $\\varphi(\\overline k)=\\nu_k$. On a alors\n",
    "\n",
    "$$\\varphi(\\overline n)=\\sum_{x\\in \\overline n}2^{\\varphi(x)}=\\sum_{k=0}^{n-1}2^{\\varphi(\\overline k)}=\\sum_{k=0}^{n-1}2^{\\nu_k}=\\nu_n$$"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def nu(n):\n",
    "    s = 0\n",
    "    for k in range(n):\n",
    "        s = 2 ** s + s\n",
    "    return s"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "for k in range(6):\n",
    "    print(k, nu(k))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Remarquons la valeur de $\\nu_5$. Il serait absurde d'essayer de calculer $\\nu_6$."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 2.2 Les ensembles $\\sigma_n$ et $\\tau_n$"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "On définit par récurrence sur $n$ les ensembles $\\sigma_n$ et $\\tau_n$ en posant\n",
    "\n",
    "- $\\sigma_0=\\tau_0=\\emptyset$\n",
    "- Pour tout $n\\in\\mathbb N$, $\\sigma_{n+1}=\\{\\sigma_n\\}$.\n",
    "- Pour tout $n\\in\\mathbb N$, $\\tau_{n+1}=\\tau_n\\cup\\{\\sigma_n\\}$.\n",
    "\n",
    "Remarquons que pour tout $n\\ge 1$, $\\tau_n=\\{\\sigma_0,\\ldots,\\sigma_{n-1}\\}$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def sigma(n):\n",
    "    s = []\n",
    "    for k in range(n): s = [s]\n",
    "    return s"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def tau(n):\n",
    "    return [sigma(k) for k in range(n)]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "for n in range(5):\n",
    "    print(n, tau(n))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**Proposition.** Pour tout $n\\in\\mathbb N$, \n",
    "\n",
    "- Si $n\\ne 0$, $|\\sigma_n|=1$. \n",
    "- $\\text{rg }\\sigma_n=n$.\n",
    "- $|\\tau_n|=\\text{rg }\\tau_n=n$.\n",
    "\n",
    "**Démonstration.** Récurrence sur $n$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "for k in range(10):\n",
    "    print(len(sigma(k)), rang(sigma(k)), len(tau(k)), rang(tau(k)))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**Proposition.** Pour tout $n\\in\\mathbb N$,\n",
    "\n",
    "$$\\varphi(\\sigma_n)=2^{\\uparrow n}$$\n",
    "\n",
    "et\n",
    "\n",
    "$$\\varphi(\\tau_n)=\\sum_{k=1}^{n}2^{\\uparrow k}$$\n",
    "\n",
    "**Démonstration.** Récurrence facile pour $\\varphi(\\sigma_n)$. De là, comme $\\tau_n=\\{\\sigma_0,\\ldots,\\sigma_{n-1}\\}$,\n",
    "\n",
    "$$\\varphi(\\tau_n)=\\sum_{k=0}^{n-1}2^{\\varphi(\\sigma_k)}=\\sum_{k=0}^{n-1}2^{2^{\\uparrow k}}=\\sum_{k=0}^{n-1}2^{\\uparrow k+1}=\\sum_{k=1}^{n}2^{\\uparrow k}$$"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def phi_tau(n):\n",
    "    s = 0\n",
    "    for k in range(1, n + 1):\n",
    "        s = s + ppow(2, k)\n",
    "    return s"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "for n in range(6):\n",
    "    print(n, phi_tau(n))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 2.3 Afficher les éléments de $V$ de façon plus compacte"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Avouons-le, lire les éléments de $V$ sous leur forme standard (crochets, virgules) n'est pas facile. Maintenant que nous avons mis en évidence des éléments de $V$ particuliers ($\\overline n$, $\\sigma_n$, $\\tau_n$), nous pouvons les utiliser pour représenter de façon plus compacte les ensembles héréditairement finis. La fonction `tostr` fait le travail. Elle prend en paramètre un ensemble $A\\in V$ et renvoie une représentation de $A$ sous forme de chaîne de caractères.\n",
    "\n",
    "- S'il existe $n\\in\\mathbb N$ tel que $A=\\overline n$, la fonction renvoie la chaîne qui représente l'entier $n$.\n",
    "- S'il existe $n\\in\\mathbb N$ tel que $A=\\tau_n$, la fonction renvoie $\\tau n$.\n",
    "- S'il existe $n\\in\\mathbb N$ tel que $A=\\sigma_n$, la fonction renvoie $\\sigma n$.\n",
    "- Sinon, la fonction se rappelle récursivement sur les éléments de $A$.\n",
    "\n",
    "Remarquons que $\\overline 0=\\sigma_0=\\tau_0=\\emptyset$ et $\\overline 1=\\sigma_1=\\tau_1=\\{\\emptyset\\}$ et $\\overline 2=\\tau_2$. Il n'y aura donc jamais dans la chaîne renvoyée $\\sigma 0$, $\\sigma 1$, $\\tau 0$, $\\tau 1$ et $\\tau 2$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def tostr(A):\n",
    "    n = rang(A)\n",
    "    if A == neumann(n): return str(n) # 'ν' + \n",
    "    elif A == sigma(n): return 'σ' + str(n)\n",
    "    elif A == tau(n): return 'τ' + str(n)\n",
    "    else:\n",
    "        s = '{'\n",
    "        l = len(A)\n",
    "        for k in range(l):\n",
    "            s = s + tostr(A[k])\n",
    "            if k < l - 1: s = s + ','\n",
    "        s = s + '}'\n",
    "        return s"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Les éléments de $V$ s'écrivent maintenant de façon beaucoup plus compacte."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "for k in range(20):\n",
    "    print('%3d %-35s %-15s' % (k, psi(k), tostr(psi(k))))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Voici, avec nos nouvelles notations, l'ensemble $V_4$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "A = V(4)\n",
    "print(tostr(A))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## 3. Arbre d'un ensemble héréditairement fini"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 3.1 Introduction"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Nous n'entrerons pas ici dans les détails de la notion d'*arbre*. Disons qu'un arbre possède une *racine*, qui peut être *étiquetée*, et un ensemble fini de *fils*, qui sont eux-mêmes des arbres. La *hauteur* d'un arbre $T$ est définie récursivement comme suit.\n",
    "\n",
    "- Si $T$ n'a pas de fils, $h(T)=0$.\n",
    "- Sinon, $h(T)=1+\\max\\{h(T'): T'\\text{ fils de }T\\}$.\n",
    "\n",
    "Soit $A\\in V$. On peut associer à $A$ un arbre $T(A)$ comme suit :\n",
    "\n",
    "- La racine de $T(A)$ est étiquetée par $A$.\n",
    "- Les fils de $T(A)$ sont les arbres $T(x)$, où $x\\in A$.\n",
    "\n",
    "On vérifie facilement que pour tout $A\\in V$, on a $h(T(A))=\\text{rg }A$.\n",
    "\n",
    "**Proposition.** Soient $A, B\\in V$. On a $A=B\\iff T(A)=T(B)$.\n",
    "\n",
    "**Démonstration.** Le sens direct est évident. Pour la réciproque, on procède par récurrence forte sur $\\max(\\text{rg }A,\\text{rg }B)$."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 3.2 Tracer l'arbre"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Nous ne commenterons pas les détails de la fonction `tracer0` ci-dessous. Elle prend en paramètres\n",
    "\n",
    "- Un ensemble $A\\in V$.\n",
    "- Des bornes `xmin`, `xmax`, `y` et `d`.\n",
    "\n",
    "Elle trace l'arbre de $A$ dans le rectangle $[x_{min},x_{max}]\\times[y-d,y]$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def tracer0(A, bornes):\n",
    "    xmin, xmax, y, d = bornes\n",
    "    xm = (xmin + xmax) / 2\n",
    "    if A == []:\n",
    "        plt.plot([xm], [y], 'or')\n",
    "    else:\n",
    "        n = len(A)\n",
    "        dx = (xmax - xmin) / n\n",
    "        xm = (xmin + xmax) / 2\n",
    "        for k in range(n):\n",
    "            x1 = xmin + k * dx\n",
    "            x2 = xmin + (k + 1) * dx\n",
    "            xm2 = (x1 + x2) / 2\n",
    "            plt.plot([xm, xm2], [y, y - d], color=[0.5, 0.5, 0.5])\n",
    "            tracer0(A[k], (x1, x2, y - d, d))\n",
    "        plt.plot([xm], [y], 'og')"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "La fonction `tracer_arbre` prend en paramètre un ensemble $A\\in V$. Elle trace l'arbre $\\mathcal T(A)$. Nous n'affichons pas les étiquettes des noeuds."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def tracer_arbre(A):\n",
    "    plt.rcParams['figure.figsize'] = (14, 5)\n",
    "    r = rang(A)\n",
    "    tracer0(A, (0, 1, r, 1))\n",
    "    plt.xticks([])\n",
    "    plt.yticks(range(r + 1))\n",
    "    plt.grid()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 3.3 Quelques exemples"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Voici l'arbre de $\\tau_6$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "A = tau(6)\n",
    "tracer_arbre(A)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Et voici celui de $\\overline 6$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "A = neumann(6)\n",
    "tracer_arbre(A)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Et enfin l'arbre de $V_4$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "A = V(4)\n",
    "tracer_arbre(A)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Ci-dessous, un espace de libre expression 😀."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "A = psi(31415926)\n",
    "tracer_arbre(A)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 3.4 Une propriété d'unicité"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Étant donné un arbre $T$, les *noeuds* de $T$ sont sa racine et les noeuds de ses fils. Un *réétiquetage* de $T$ est un « renommage » des noeuds de $T$. Si $T$ et $T'$ sont deux arbres et que par un réétiquetage de $T$ on obtient $T'$, nous noterons $T\\simeq T'$. Pour ne pas alourdir ce notebook, nous ne serons pas plus précis que cela. \n",
    "\n",
    "**Proposition.** Soit $T$ un arbre. Il existe un unique ensemble $A\\in V$ tel que $T\\simeq T(A)$.\n",
    "\n",
    "**Démonstration.** Voici une idée de la preuve, qui se fait par récurrence forte sur la hauteur de $T$.\n",
    "\n",
    "- Si $T$ est de hauteur 0, il possède un seul noeud (sa racine) et aucun fils. Clairement, le seul étiquetage possible est d'étiqueter sa racine par $\\emptyset$.\n",
    "- Soit $n\\in\\mathbb N^*$. Supposons la propriété vérifiée pour tous les arbres de hauteur strictement inférieure à $n$. Soit $T$ un arbre de hauteur $n$. Soient $x$ sa racine et $T_1,\\ldots,T_m$ les fils de $x$. Les $T_i$ étant de hauteur strictement inférieure à $n$ il existe un unique $x_i\\in V$ tel que par $T_i\\simeq T(x_i)$. Le seul étiquetage de $T$ possible est l'étiquetage de la racine de $T$ par $A=\\{x_1,\\ldots,x_m\\}$. On a alors $T\\simeq T(A)$. $\\square$\n",
    "\n",
    "Ce que nous dit ce théorème, c'est que le fait de ne pas afficher les étiquettes n'amène aucune ambiguïté : on peut retrouver les valeurs des étiquettes, uniquement à partir de la « forme » de l'arbre. Prenons un exemple."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "A = psi(13)\n",
    "tracer_arbre(A)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "- Le fils « gauche » de la racine est clairement $T(\\emptyset)$.\n",
    "- Le fils du « milieu » est $T(x)$ où $x$ a un unique élément, cet élément ayant un unique élément, qui est $\\emptyset$. Ainsi, $x=\\{\\{\\emptyset\\}\\}=\\sigma_2$.\n",
    "- Le fils « droit » de la racine a deux éléments. Celui de « gauche » est $\\emptyset$, celui de droite est $\\{\\emptyset\\}$. Ce fils droit est donc $T(\\{\\emptyset,\\{\\emptyset\\}\\})=T(\\overline 2)$.\n",
    "\n",
    "Ainsi, $T=T(\\{\\overline 0, \\sigma_2, \\overline 2\\})$. Vérifions ..."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "A = psi(13)\n",
    "print(A)\n",
    "print(tostr(A))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## 4. Énumérer $V$"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 4.1 Successeur"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Pour tout $A\\in V$, notons $A^+$ le *successeur* de $A$, défini par $\\varphi(A^+)=\\varphi(A)+1$.\n",
    "\n",
    "**Proposition.** Soit $m$ le plus petit ensemble héréditairement fini (au sens de la relation $\\le$ définie sur $V$) tel que $m\\not\\in A$. On a alors\n",
    "\n",
    "$$A^+=\\{m\\}\\cup\\{x\\in A:x>m\\}$$\n",
    "\n",
    "**Démonstration.** Par définition de $m$, on a la réunion disjointe\n",
    "\n",
    "$$A=A'\\cup A''=\\{x\\in V:x<m\\}\\cup\\{x\\in A: m<x\\}$$\n",
    "\n",
    "De là,\n",
    "\n",
    "$$\\varphi(A)=\\varphi(A')+\\varphi(A'')=\\sum_{k\\in\\mathbb N, k<\\varphi(m)} 2^k+\\sum_{x\\in A, x>m}2^{\\varphi(x)}$$\n",
    "\n",
    "Remarquons que\n",
    "\n",
    "$$1+\\sum_{k<\\varphi(m)} 2^k=2^{\\varphi(m)}$$\n",
    "\n",
    "De là,\n",
    "\n",
    "$$\\varphi(A^+)=2^{\\varphi(m)}+\\sum_{x\\in A, x>m}2^{\\varphi(x)}\\ \\square$$\n",
    "\n",
    "La fonction `succ` prend un ensemble $A\\in V$ en paramètre. Elle renvoie $A^+$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def succ(A):\n",
    "    k = 0\n",
    "    B = []\n",
    "    while k < len(A) and A[k] == B:\n",
    "        B = succ(B)\n",
    "        k = k + 1\n",
    "    return [B] + A[k:]"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Voici un exemple d'ensemble pour lequel la fonction `succ` donne une réponse immédiate, alors que l'image par $\\varphi$ de cet ensemble est un entier colossalement grand."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "A = sigma(100)\n",
    "print(tostr(A))\n",
    "print(tostr(succ(A)))\n",
    "print(tostr(succ(succ(A))))\n",
    "print(tostr(succ(succ(succ(A)))))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 4.2 Itérer sur les ensembles héréditairement finis"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "La fonction `HF0` est un itérateur. Il prend en paramètres un ensemble $A\\in V$ et un entier $n$ puis énumère $n$ ensembles héréditairement finis à partir de $A$ inclus."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def HF0(A, n):\n",
    "    for k in range(n):\n",
    "        yield A\n",
    "        if k < n: A = succ(A)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Dans l'exemple ci-dessous, on affiche 10 ensembles de $V$ à partir de $\\psi(123456)$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "for A in HF0(psi(123456), 10):\n",
    "    print(phi(A), tostr(A))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 4.3 Prédécesseur"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Pour tout $A\\in V$ non vide, notons $A^-$ le *prédécesseur* de $A$, c'est à dire l'ensemble tel que $(A^-)^+=A$.\n",
    "\n",
    "**Proposition.** Soit $x=\\min A$.\n",
    "\n",
    "- Si $x=\\emptyset$, alors $A^-=A\\setminus\\{\\emptyset\\}$.\n",
    "- Sinon, $A^-=\\{\\emptyset,\\emptyset^+,\\emptyset^{++},\\ldots, x^-\\}\\cup (A\\setminus\\{x\\})$.\n",
    "\n",
    "**Démonstration.** Soit $B=\\{\\emptyset,\\emptyset^+,\\emptyset^{++},\\ldots, x^-\\}\\cup (A\\setminus\\{x\\})$. Le plus petit $m\\in V$ tel que $m\\not\\in B$ est $m=x$. On a donc\n",
    "\n",
    "$$B^+=\\{x\\}\\cup\\{y\\in A: x<y\\}=\\{x\\}\\cup(A\\setminus\\{x\\})=A\\ \\square$$"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def pred(A):\n",
    "    X = A[0]\n",
    "    B = []\n",
    "    y = []\n",
    "    while inferieur_strict(y, X):\n",
    "        B = B + [y[:]]\n",
    "        y = succ(y)\n",
    "    return B + A[1:]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "A = psi(123456)\n",
    "print(tostr(A))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "A = pred(A)\n",
    "print(tostr(A))\n",
    "print(phi(A))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "A = sigma(123)\n",
    "print(pred(succ(A)) == A)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**Remarque.** Contrairement à la fonction `succ`, la fonction `pred` peut renvoyer (ou plutôt ne renvoie pas) un ensemble de taille gigantesque. Par exemple, nous ne pourrions pas demander le prédécesseur de $\\sigma_{10}$ parce que $\\sigma_{10}^-=V_9$, un ensemble de taille ... $2^{<9>}$ !"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "La fonction `HF` est une généralisation de l'itérateur `HF0` défini un peu plus haut. Il permet d'énumérer $|n|$ éléments de $V$ à partir de $A$ dans l'ordre croissant ou dans l'ordre décroissant, selon que $n\\ge 0$ ou $n<0$. La remarque ci-dessus incite à la prudence quant au choix de l'ensemble $A$ de départ."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def HF(A, n):\n",
    "    if n >= 0:\n",
    "        for k in range(n):\n",
    "            yield A\n",
    "            if k < n: A = succ(A)\n",
    "    else:\n",
    "        for k in range(-n):\n",
    "            yield A\n",
    "            if k < -n: A = pred(A)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "for A in HF(psi(123456), -10):\n",
    "    print(phi(A), tostr(A))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "for A in HF(psi(123456), 10):\n",
    "    print(phi(A), tostr(A))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## 5. Opérations ensemblistes"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Étant donnés deux ensemble s $A,B\\in V$, a-t-on $A\\cup B\\in V$ ? Si oui, que vaut $\\text{rg } A\\cup B$ ? Que dire pour les autres opérations ensemblistes, intersection, ensemble des parties, etc ?"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 5.1 Appartenance, inclusion"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Étant donnés deux ensembles $x,A\\in V$, il suffit évidemment de l'instruction `x in A` pour décider si $x\\in A$. Cette instruction cache un algorithme qui demande $O(|A|)$ tests d'égalité de listes. On peut faire mieux en exploitant le fait que nous représentons l'ensemble $A$ par une *liste triée*. La fonction `appartient` ci-dessous effectue $O(\\lg A)$ tests d'égalités de listes. Elle effectue une recherche dichotomique de $x$ dans la liste triée $A$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def appartient(x, A):\n",
    "    n = len(A)\n",
    "    if n == 0: return False\n",
    "    elif inferieur_strict(x, A[0]) or inferieur_strict(A[n - 1], x): return False\n",
    "    else:\n",
    "        i = 0\n",
    "        j = n\n",
    "        while j - i > 1:\n",
    "            k = (i + j) // 2\n",
    "            if x == A[k]: return True\n",
    "            elif inferieur_strict(x, A[k]): j = k\n",
    "            else: i = k\n",
    "        return A[i] == x"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "A = neumann(17)\n",
    "x = neumann(14)\n",
    "print(appartient(x, A))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**Proposition.** Soit $B\\in V$. Soit $A$ un ensemble tel que $A\\subseteq B$. Alors, $A\\in V$ et $\\text{rg }A\\le \\text{rg }B$.\n",
    "\n",
    "**Démonstration.** Rappelons qu'un ensemble est dans $V$ si et seulement si il est fini et inclus dans $V$. On a $A\\subseteq B\\subseteq V$, donc $A$ est fini (car inclus dans l'ensemble fini $B$) et inclus dans $V$. Ainsi, $A\\in V$.\n",
    "\n",
    "Passons au rang de $A$. Si $A=\\emptyset$, c'est évident. Sinon, $\\text{rg }A=\\max\\{\\text{rg }x:x\\in A\\}+1 \\le \\max\\{\\text{rg }x:x\\in B\\}+1=\\text{rg }B$. $\\square$"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def inclus(A, B):\n",
    "    for x in A:\n",
    "        if not appartient(x, B): return False\n",
    "    return True"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 5.2 Intersection"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**Proposition.** Soient $A,B\\in V$. On a $A\\cap B\\in V$ et $\\text{rg }A\\cap B\\le \\min(\\text{rg }A,\\text{rg }B)$.\n",
    "\n",
    "**Démonstration.** En effet, $A\\cap B\\subseteq A$ et $A\\cap B\\subseteq B$.  $\\square$\n",
    "\n",
    "**Corollaire.** Soit $n\\ge 1$. Soient $A_1,\\ldots,A_n$ $n$ ensembles héréditairement finis. Alors, $\\bigcap_{k=1}^n A_k\\in V$ et $\\text{rg }\\bigcap_{k=1}^n A_k\\le \\min\\{\\text{rg }A_k:k\\in [\\![1,n]\\!]\\}$.\n",
    "\n",
    "**Démonstration.** Récurrence sur $n$."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Les ensembles ayant une représentation dans laquelle leurs éléments sont triés, il est facile de calculer une intersection.\n",
    "\n",
    "On initialise la future intersection $C$ à la liste vide.\n",
    "\n",
    "Tant que $A$ et $B$ sont non vides :\n",
    "\n",
    "- Si $\\min A<\\min B$, alors $\\min A\\not\\in B$. On retire $\\min A$ de $A$.\n",
    "- Si $\\min A>\\min B$, alors $\\min B\\not\\in A$. On retire $\\min B$ de $B$.\n",
    "- Si $\\min A=\\min B$, alors $\\min B\\in A\\cap B$. On retire $\\min A$ de $A$ et $\\min B$ de $B$, et on rajoute la valeur commune à la liste $C$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def intersection(A, B):\n",
    "    C = []\n",
    "    while A != [] and B != []:\n",
    "        if inferieur_strict(A[0], B[0]):\n",
    "            A = A[1:]\n",
    "        elif inferieur_strict(B[0], A[0]):\n",
    "            B = B[1:]\n",
    "        else:\n",
    "            C.append(A[0])\n",
    "            A = A[1:]\n",
    "            B = B[1:]\n",
    "    return C"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "A = psi(123456)\n",
    "B = psi(1234567)\n",
    "print('A            : ', tostr(A))\n",
    "print('B            : ', tostr(B))\n",
    "print('Intersection : ', tostr(intersection(A, B)))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 5.3 Réunion"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**Proposition.** Soient $A,B\\in V$. On a $A\\cup B\\in V$ et $\\text{rg }A\\cup B=\\max(\\text{rg }A,\\text{rg }B)$.\n",
    "\n",
    "**Démonstration.** $A\\cup B$ est fini et inclus dans $V$, donc $A\\cup B\\in V$. Passons au calcul du rang.\n",
    "\n",
    "Si $A$ ou $B$ est vide le résultat est évident. Supposons donc $A$ et $B$ non vides. \n",
    "\n",
    "On a $A\\subseteq A\\cup B$, donc $\\text{rg }A\\le\\text{rg } A\\cup B$. de même, $\\text{rg }B\\le\\text{rg } A\\cup B$, et donc $\\max(\\text{rg }A,\\text{rg }B)\\le\\text{rg } A\\cup B$.\n",
    "\n",
    "Pour tout $x\\in A$, $\\text{rg }x\\le \\text{rg }A-1$. Pour tout $x\\in B$, $\\text{rg }x\\le \\text{rg }B-1$. De là, pour tout $x\\in A\\cup B$, \n",
    "\n",
    "$$\\text{rg }x\\le \\max(\\text{rg }A-1,\\text{rg }B-1)=\\max(\\text{rg }A,\\text{rg }B)-1$$\n",
    "\n",
    "On en déduit que $\\text{rg }A\\cup B\\le \\max(\\text{rg }A,\\text{rg }B)$.  $\\square$\n",
    "\n",
    "**Corollaire.** Soit $n\\ge 1$. Soient $A_1,\\ldots,A_n$ $n$ ensembles héréditairement finis. Alors, $\\bigcup_{k=1}^n A_k\\in V$ et $\\text{rg }\\bigcup_{k=1}^n A_k=\\max\\{\\text{rg }A_k:k\\in [\\![1,n]\\!]\\}$.\n",
    "\n",
    "**Démonstration.** Récurrence sur $n$."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Voici la fonction `reunion`. Elle prend en paramètres deux ensembles $A,B\\in V$ et renvoie leur réunion. Elle fonctionne comme la fonction `intersection`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def reunion(A, B):\n",
    "    C = []\n",
    "    while A != [] and B != []:\n",
    "        if inferieur_strict(A[0], B[0]):\n",
    "            C.append(A[0])\n",
    "            A = A[1:]\n",
    "        elif inferieur_strict(B[0], A[0]):\n",
    "            C.append(B[0])\n",
    "            B = B[1:]\n",
    "        else:\n",
    "            C.append(A[0])\n",
    "            A = A[1:]\n",
    "            B = B[1:]\n",
    "    C = C + B[:]\n",
    "    C = C + A[:]\n",
    "    return C"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "A = psi(123456)\n",
    "B = psi(1234567)\n",
    "print('A            : ', tostr(A))\n",
    "print('B            : ', tostr(B))\n",
    "print('Intersection : ', tostr(intersection(A, B)))\n",
    "print('Réunion      : ', tostr(reunion(A, B)))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 5.4 Différence"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**Proposition.** Soient $A,B\\in V$. Alors, $A\\setminus B\\in V$ et $\\text{rg }A\\setminus B\\le\\text{rg }A$.\n",
    "\n",
    "**Démonstration.** En effet, $A\\setminus B\\subseteq A$."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "De même que pour l'intersection et la réunion, la différence de deux ensembles se calcule sans difficulté."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def difference(A, B):\n",
    "    C = []\n",
    "    while A != [] and B != []:\n",
    "        if inferieur_strict(A[0], B[0]):\n",
    "            C.append(A[0])\n",
    "            A = A[1:]\n",
    "        elif inferieur_strict(B[0], A[0]):\n",
    "            B = B[1:]\n",
    "        else:\n",
    "            A = A[1:]\n",
    "            B = B[1:]\n",
    "    if B == []:\n",
    "        C = C + A[:]\n",
    "    return C"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "A = psi(123456)\n",
    "B = psi(1234567)\n",
    "print('A            : ', tostr(A))\n",
    "print('B            : ', tostr(B))\n",
    "print('Intersection : ', tostr(intersection(A, B)))\n",
    "print('Réunion      : ', tostr(reunion(A, B)))\n",
    "print('Différence   : ', tostr(difference(A, B)))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 5.5 Parties"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**Proposition.** Soit $A\\in V$. On a $\\mathcal P(A)\\in V$ et $\\text{rg }\\mathcal P(A)=\\text{rg }A+1$.\n",
    "\n",
    "**Démonstration.** Pour tout $X\\in\\mathcal P(A)$, $X\\subseteq A$ et donc $\\text{rg }X\\le \\text{rg }A$. On en déduit que\n",
    "\n",
    "$$\\text{rg }\\mathcal P(A)=\\max\\{\\text{rg }X,X\\in\\mathcal P(A)\\}+1\\le \\text{rg }A+1$$\n",
    "\n",
    "De plus, $A\\in \\mathcal P(A)$, donc $\\text{rg }\\mathcal P(A)\\ge \\text{rg }A+1$. $\\square$"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "La fonction `parties` ci-dessous fait appel à la fonction `reunion` pour garantir que les ensembles renvoyés sont bien triés dans l'ordre croissant de leurs éléments. Elle fonctionne comme suit.\n",
    "\n",
    "Soit $A\\in V$.\n",
    "\n",
    "- Si $A=\\emptyset$, alors $\\mathcal P(A)=\\{\\emptyset\\}$.\n",
    "- Sinon, soit $x=\\min A$. Soit $A'=A\\setminus \\{x\\}$. Soit $P=\\mathcal P(A')$. On a\n",
    "\n",
    "$$\\mathcal P(A)=P\\cup\\{y\\cup\\{x\\}: y\\in P\\}$$"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def parties(A):\n",
    "    if A == []: return [[]]\n",
    "    else:\n",
    "        P = parties(A[1:])\n",
    "        P1 = [reunion([A[0]], X) for X in P]\n",
    "        return reunion(P, P1)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "A = parties(neumann(4))\n",
    "print(tostr(A))\n",
    "print(len(A), rang(A))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "tracer_arbre(parties(neumann(4)))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 5.6 Couples"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Nous utilisons ici une définition de couple due à von Neumann. \n",
    "\n",
    "**Définition.** Étant donnés deux ensembles $A,B\\in V$, le *couple* $(A,B)$ est\n",
    "\n",
    "$$(A,B)=\\{\\{A\\},\\{A,B\\}\\}$$\n",
    "\n",
    "**Proposition.** Soient $A,B,C,D\\in V$. On a $(A,B)=(C,D)\\iff A=C\\land B=D$.\n",
    "\n",
    "**Démonstration.** Laissée en exercice. Considérer deux cas, $A=B$ et $A\\ne B$."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**Proposition.** Soient $A,B\\in V$. On a $(A,B)\\in V$ et $\\text{rg }(A,B)=\\max(\\text{rg }A,\\text{rg }B)+2$.\n",
    "\n",
    "**Démonstration.** Soient $m=\\text{rg }A$ et $n=\\text{rg }B$. On a $\\text{rg }\\{A\\}=m+1$ et $\\text{rg }\\{A,B\\}=\\max(m, n)+1$. De là,\n",
    "\n",
    "$$\\text{rg }(A,B)=\\max(m+1, \\max(m, n)+1)+1=\\max(m,n)+2\\ \\square$$"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "La fonction `couple` renvoie le couple de von Neumann $(A,B)$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def couple(A, B):\n",
    "    if A == B: \n",
    "        return [[A]]\n",
    "    elif inferieur_strict(A, B): \n",
    "        return [[A], [A, B]]\n",
    "    else:\n",
    "        return [[A], [B, A]]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "jupyter": {
     "outputs_hidden": true
    }
   },
   "outputs": [],
   "source": [
    "C = couple(neumann(4), tau(5))\n",
    "print(tostr(C))\n",
    "tracer_arbre(C)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "C = couple(tau(5), neumann(4))\n",
    "print(tostr(C))\n",
    "tracer_arbre(C)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Comment récupérer les ensembles $A$ et $B$ lorsqu'on possède le couple $C=(A,B)$ ? \n",
    "\n",
    "- Tout d'abord, $\\{A\\}=\\min C$ et donc $A=\\min\\min C$.\n",
    "- Si $\\min C=\\max C$, alors $B=A$.\n",
    "- Snon, $\\max C\\setminus\\min C=\\{A,B\\}\\setminus\\{A\\}=\\{B\\}$ et donc $B=\\min (\\max C\\setminus\\min C)$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def composantes(C):\n",
    "    A = C[0][0]\n",
    "    if len(C) == 1:\n",
    "        return (A, A)\n",
    "    else:\n",
    "        B = difference(C[1], C[0])[0]\n",
    "        return (A, B)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "C = couple(psi(123456789), psi(987654321))\n",
    "A, B = composantes(C)\n",
    "print(A == psi(123456789), B == psi(987654321))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "La fonction `est_couple` prend en paramètre un ensemble $A\\in V$. Elle renvoie `True` si $A$ est un couple et `False`\n",
    " sinon."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def est_couple(A):\n",
    "    if len(A) == 1 and len(A[0]) == 1: return True\n",
    "    elif len(A) == 2 and len(A[0]) == 1 and len(A[1]) == 2 and inclus(A[0], A[1]): return True\n",
    "    else: return False"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Parmi les $2^{16}$ premiers ensembles de $V$ (c'est à dire parmi les éléments de $V_4$), lesquels sont des couples ?"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "for A in HF([], 65536):\n",
    "    if est_couple(A): print(phi(A), tostr(A))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Profitons de ce que nous avons un nouveau type d'ensemble dans $V$, les couples, pour réécrire la fonction `tostr`. Notre nouvelle fonction, `tostring`, détecte si l'ensemble $A$ est un couple $(x, y)$. Elle renvoie dans ce cas une représentation correcte pour l'ensemble, sous la forme $<x,y>$ (les crochets se distinguent plus facilement des accolades que les parenthèses).\n",
    "\n",
    "Remarquons que \n",
    "\n",
    "- $\\overline n$ et $\\tau_n$ ne sont jamais des couples, comme il est facile de le vérifier. \n",
    "- Enn revanche, pour tout $n\\ge 2$, $\\sigma_n$ est un couple. En effet,\n",
    "\n",
    "$$\\sigma_n=\\{\\{\\sigma_{n-2}\\}\\}=(\\sigma_{n-2},\\sigma_{n-2})$$"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def tostring(A):\n",
    "    n = rang(A)\n",
    "    if A == neumann(n): return str(n) # 'ν' + \n",
    "    elif A == sigma(n): return 'σ' + str(n)\n",
    "    elif A == tau(n): return 'τ' + str(n)\n",
    "    elif est_couple(A):\n",
    "        x, y = composantes(A)\n",
    "        return '<' + tostring(x) + ',' + tostring(y) + '>'\n",
    "    else:\n",
    "        s = '{'\n",
    "        l = len(A)\n",
    "        for k in range(l):\n",
    "            s = s + tostring(A[k])\n",
    "            if k < l - 1: s = s + ','\n",
    "        s = s + '}'\n",
    "        return s"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "A = couple(psi(123), psi(321))\n",
    "print(tostring(A))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Quels sont les éléments de $V_5$ qui sont des couples ? Il y en a 16."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "for A in HF([], 65536):\n",
    "    if est_couple(A): print(phi(A), tostring(A))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Peut-on définir la notion de triplet, de quadruplet, etc ? Oui, bien sûr.\n",
    "\n",
    "**Définition.** On définit par récurrence sur $n$ le *$n$-uplet* $(A_1,\\ldots,A_n)$ en posant pour tout $n\\ge 2$,\n",
    "\n",
    "$$(A_1,\\ldots,A_{n+1})=(A_1,(A_2,\\ldots, A_{n+1}))$$\n",
    "\n",
    "Le lecteur consciencieux montrera que deux $n$-uplets sont égaux si et seulement si leurs composantes sont égales. On peut sans difficulté écrire des fonctions manipulant des $n$-uplets. Par exemple,"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def triplet(A, B, C):\n",
    "    return couple(A, couple(B, C))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def est_triplet(A):\n",
    "    return est_couple(A) and est_couple(composantes(A)[1])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def composantes3(T):\n",
    "    A, U = composantes(T)\n",
    "    B, C = composantes(U)\n",
    "    return (A, B, C)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Quels sont les éléments de $V_5$ qui sont des triplets ? Il y en a 4."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "for A in HF([], 65536):\n",
    "    if est_triplet(A): print(phi(A), tostring(A))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 5.7 Produit cartésien"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**Définition.** Le *produit cartésien* des ensembles $A$ et $B$ est $A\\times B=\\{(x,y):x\\in A,y\\in B\\}$."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**Proposition.** Soient $A, B\\in V$. On a $A\\times B\\in V$. Si $A$ et $B$ sont non vides, alors $\\text{rg }A\\times B=\\max(\\text{rg }A,\\text{rg }B)+2$.\n",
    "\n",
    "**Démonstration.** Soient $m$ et $n$ les rangs respectifs de $A$ et $B$. Pour tout $x\\in A$, $\\text{rg }x\\le m-1$ et pour tout $y\\in B$, $\\text{rg }y\\le n-1$. De là, $\\text{rg }(x,y)\\le \\max(m-1,n-1)+2=\\max(m, n)+1$. On en déduit que $\\text{rg }A\\times B\\le \\max(m, n)+2$.\n",
    "\n",
    "De plus, il existe $x\\in A$ de rang $m-1$ et $y\\in B$ de rang $n-1$. On a alors $\\text{rg }(x,y)=\\max(m, n)+1$ donc $\\text{rg }A\\times B\\ge \\max(m, n)+2$. $\\square$"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def produit(A, B):\n",
    "    C = []\n",
    "    for x in A:\n",
    "        for y in B:\n",
    "            C = reunion(C, [couple(x, y)])\n",
    "    return C"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "A = produit(tau(2), tau(3))\n",
    "print(tostring(A))\n",
    "tracer_arbre(A)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "A = produit(tau(3), tau(2))\n",
    "print(tostring(A))\n",
    "tracer_arbre(A)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  }
 ],
 "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.8.5"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 4
}