KnightsnKnaves.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "d98f2a7e-c386-4d71-a703-cd697dce1ef8",
   "metadata": {},
   "source": [
    "# Preamble"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 27,
   "id": "f6292d91-3bd6-4015-b743-243e5fcf6eed",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "defined \u001b[32mtype\u001b[39m \u001b[36mOr\u001b[39m\r\n",
       "defined \u001b[32mtype\u001b[39m \u001b[36mAnd\u001b[39m\r\n",
       "defined \u001b[32mtype\u001b[39m \u001b[36mImplies\u001b[39m\r\n",
       "defined \u001b[32mtype\u001b[39m \u001b[36mFalse\u001b[39m\r\n",
       "defined \u001b[32mtype\u001b[39m \u001b[36mTrue\u001b[39m\r\n",
       "defined \u001b[32mtype\u001b[39m \u001b[36mNot\u001b[39m\r\n",
       "defined \u001b[32mtype\u001b[39m \u001b[36m<=>\u001b[39m"
      ]
     },
     "execution_count": 27,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "type Or[P, Q] = Either[P, Q]\n",
    "type And[P, Q] = Tuple2[P, Q]\n",
    "type Implies[P, Q] = P => Q\n",
    "type False = Nothing\n",
    "type True = Unit\n",
    "type Not[P] = P => Nothing\n",
    "type <=>[P, Q] = (P => Q, Q => P)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "57ed924c-f1f1-426b-9566-7503510f2816",
   "metadata": {},
   "source": [
    "__P1:__ $\\forall x. \\mathrm{Knight}(x) \\vee \\mathrm{Knave}(x)$, where $\\mathrm{Knave}(x) \\equiv \\neg \\mathrm{Knight}(x)$\n",
    "\n",
    "__P2:__ $\\forall x. \\mathrm{Knight}(x) \\rightarrow \\forall p. (\\mathrm{Says}(x, p) \\rightarrow p)$\n",
    "\n",
    "__P3:__ $\\forall x. \\mathrm{Knave}(x) \\rightarrow \\forall p. (\\mathrm{Says}(x, p) \\rightarrow \\neg p)$\n",
    "\n",
    "__Puzzle:__ $\\{\\mathrm{P1},\\;\\mathrm{P2},\\;\\mathrm{P3}\\} \\vdash \\forall x. \\neg \\mathrm{Says}(x, \\mathrm{Knave}(x))$\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 28,
   "id": "24be4df5-ad96-4192-b41c-29e22a930b2e",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "defined \u001b[32mtrait\u001b[39m \u001b[36mInhabitant\u001b[39m"
      ]
     },
     "execution_count": 28,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "trait Inhabitant:\n",
    "    type Knight\n",
    "    type Knave = Not[Knight]\n",
    "    type Says[_]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 29,
   "id": "8f5959c9-620a-4e62-8322-c0e09e4f99b8",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "defined \u001b[32mtrait\u001b[39m \u001b[36mKnightsAndKnaves\u001b[39m"
      ]
     },
     "execution_count": 29,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "trait KnightsAndKnaves:\n",
    "    // ∀ x. Inhabitant(x) 🠂 Knight(x) ∨ Knave(x)\n",
    "    val P1: (x: Inhabitant) => Either[x.Knight, x.Knave]\n",
    "    \n",
    "    // ∀ p. ∀ x. Knight(x) 🠂 Says(x, p) 🠂 p \n",
    "    val P2: [P] => (x: Inhabitant) => x.Knight => x.Says[P] => P\n",
    "\n",
    "    // ∀ p. ∀ x. Knave(x) 🠂 Says(x, p) 🠂 Not[p] \n",
    "    val P3: [P] => (x: Inhabitant) => x.Knave => x.Says[P] => Not[P]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 30,
   "id": "7f332451-b2e6-41d2-8dd5-8feba4c0184c",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "defined \u001b[32mfunction\u001b[39m \u001b[36mpuzzle1\u001b[39m"
      ]
     },
     "execution_count": 30,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "def puzzle1(KK: KnightsAndKnaves): (x: Inhabitant) => Not[x.Says[x.Knave]] = \n",
    "    (x: Inhabitant) => (s: x.Says[x.Knave]) => \n",
    "        KK.P1(x) match\n",
    "            case Left(xIsKnight: x.Knight) => \n",
    "                KK.P2[x.Knave](x)(xIsKnight)(s)(xIsKnight) : Nothing\n",
    "            case Right(xIsKnave) => \n",
    "                KK.P3[x.Knave](x)(xIsKnave)(s)(xIsKnave) : Nothing"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 31,
   "id": "ceec7c2b-a95f-4720-b06e-2e9cc92013ca",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "defined \u001b[32mobject\u001b[39m \u001b[36mSugar\u001b[39m"
      ]
     },
     "execution_count": 31,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "object Sugar:\n",
    "\n",
    "    implicit class NoOp[P](np: Not[P]):\n",
    "        def contradicts(p: P): Nothing = np(p)\n",
    "\n",
    "    def eitherKnightOrKnave[A](x: Inhabitant): KnightsAndKnaves ?=> (x.Knight ?=> A, x.Knave ?=> A) => A = \n",
    "        P ?=> (f, g) => P.P1(x).fold(a => f(using a), a => g(using a))\n",
    "\n",
    "    def knightsAreTruthful[A](x: Inhabitant): KnightsAndKnaves ?=> x.Knight ?=> x.Says[A] => A = \n",
    "        P ?=> xIsKnight ?=> xSaysA => P.P2(x)(xIsKnight)(xSaysA)\n",
    "\n",
    "    def knavesAreLiers[A](x: Inhabitant): KnightsAndKnaves ?=> x.Knave ?=> x.Says[A] => Not[A] = \n",
    "        P ?=> xIsKnave ?=> xSaysA => P.P3(x)(xIsKnave)(xSaysA)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 32,
   "id": "2666bd39-337c-497d-854c-48270338b1bd",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "\u001b[32mimport \u001b[39m\u001b[36mSugar._\r\n",
       "\u001b[39m"
      ]
     },
     "execution_count": 32,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "import Sugar._"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "7ca54308-96ff-43f3-9151-7be8c5d77ad8",
   "metadata": {},
   "source": [
    "### Puzzle 1\n",
    "\n",
    "You have met a group of 3 islanders. Their names are Bob, Wallace, and Joan.\n",
    "\n",
    "* Joan says: Wallace is a knight.\n",
    "* Wallace says: Bob never lies.\n",
    "* Joan says: Bob is my type.\n",
    "\n",
    "Answer: \n",
    "\n",
    "Bob, Wallace and Joan are all knights.\n",
    "\n",
    "Reasoning:\n",
    "\n",
    "* A knight or a knave will say they are the same type as a knight. So when Joan says they are the same type as Bob, we know that Bob is a knight.\n",
    "* All islanders will call one of their same kind a knight. So when Wallace says that Bob is a knight, we know that Bob and Wallace are the same type. Since Bob is a knight, then Wallace is a knight.\n",
    "* All islanders will call one of their same kind a knight. So when Joan says that Wallace is a knight, we know that Wallace and Joan are the same type. Since Wallace is a knight, then Joan is a knight."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 33,
   "id": "3dad0e0b-e230-4ac8-b4dd-c923cb9ede9c",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "defined \u001b[32mfunction\u001b[39m \u001b[36mdeMorgan\u001b[39m"
      ]
     },
     "execution_count": 33,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "def deMorgan[P, Q](n: Not[Either[P, Q]]): (Not[P], Not[Q]) = \n",
    "    (p => n(Left(p)), q => n(Right(q)))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 34,
   "id": "56d0fe4f-7c49-46d9-ac1a-08a12ee01cdb",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "defined \u001b[32mfunction\u001b[39m \u001b[36msaysSameTypeThenOtherKnight\u001b[39m"
      ]
     },
     "execution_count": 34,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "def saysSameTypeThenOtherKnight(using KnightsAndKnaves)(x: Inhabitant, y: Inhabitant): \n",
    "        x.Says[Either[(x.Knight, y.Knight), (x.Knave, y.Knave)]] => y.Knight = \n",
    "    xSays => eitherKnightOrKnave(x)(\n",
    "        xIsKnight ?=> \n",
    "            knightsAreTruthful(x)(xSays) match\n",
    "                case Left(xIsKnight, yIsKnight) => yIsKnight\n",
    "                case Right(xIsKnave, _) => xIsKnave contradicts xIsKnight,\n",
    "        xIsKnave ?=> \n",
    "            val l: (Not[(x.Knight, y.Knight)], Not[(x.Knave, y.Knave)]) = deMorgan(knavesAreLiers(x)(xSays))\n",
    "            eitherKnightOrKnave(y)(\n",
    "                yIsKnight ?=> yIsKnight , \n",
    "                yIsKnave ?=> l._2 contradicts (xIsKnave, yIsKnave)))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 35,
   "id": "9575f149-0f35-404d-b37b-0845f8ec7534",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "defined \u001b[32mfunction\u001b[39m \u001b[36msaysOtherKnightThenSameType\u001b[39m"
      ]
     },
     "execution_count": 35,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "def saysOtherKnightThenSameType(using KnightsAndKnaves)(x: Inhabitant, y: Inhabitant): \n",
    "        x.Says[y.Knight] => Either[(x.Knight, y.Knight), (x.Knave, y.Knave)] = \n",
    "    xSays => eitherKnightOrKnave(x)(\n",
    "        xIsKnight ?=> \n",
    "            Left(xIsKnight, knightsAreTruthful(x)(xSays)),\n",
    "        xIsKnave ?=> \n",
    "            Right(xIsKnave, knavesAreLiers(x)(xSays)))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 36,
   "id": "96ace4f4-7620-4eef-aa3f-2ee9bbbd5d0e",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "defined \u001b[32mfunction\u001b[39m \u001b[36msameTypeAndOtherKnightThenIsKnight\u001b[39m"
      ]
     },
     "execution_count": 36,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "def sameTypeAndOtherKnightThenIsKnight[P, Q]: (Either[(P, Q), (Not[P], Not[Q])], Q) => P = \n",
    "    case (Left(p, _),_) => p\n",
    "    case (Right(_, nq),q) => nq(q)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 37,
   "id": "b4491c9f-a5e0-4787-98de-0cabb2452a4a",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "defined \u001b[32mfunction\u001b[39m \u001b[36mpuzzle\u001b[39m"
      ]
     },
     "execution_count": 37,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "def puzzle(using KnightsAndKnaves)(\n",
    "    joan: Inhabitant, wallace: Inhabitant, bob: Inhabitant): \n",
    "    (joan.Says[wallace.Knight], \n",
    "     wallace.Says[bob.Knight], \n",
    "     joan.Says[Either[(joan.Knight, bob.Knight),(joan.Knave, bob.Knave)]]) => (joan.Knight, wallace.Knight, bob.Knight) = \n",
    "    (joanSays1, wallaceSays, joanSays2) => \n",
    "        // A knight or a knave will say they are the same type as a knight. \n",
    "        // So when Joan says they are the same type as Bob, we know that Bob is a knight.\n",
    "        val bobIsKnight: bob.Knight = saysSameTypeThenOtherKnight(joan, bob)(joanSays2)\n",
    "        // All islanders will call one of their same kind a knight. So when Wallace says that Bob is a knight, we know that \n",
    "        // Bob and Wallace are the same type. \n",
    "        val sameTypeWB: Either[(wallace.Knight, bob.Knight), (wallace.Knave, bob.Knave)] = saysOtherKnightThenSameType(wallace, bob)(wallaceSays)\n",
    "        // Since Bob is a knight, then Wallace is a knight.\n",
    "        val wallaceIsKnight: wallace.Knight = sameTypeAndOtherKnightThenIsKnight(sameTypeWB, bobIsKnight)\n",
    "        // All islanders will call one of their same kind a knight. So when Joan says that Wallace is a knight, \n",
    "        // we know that Wallace and Joan are the same type.\n",
    "        val sameTypeJW: Either[(joan.Knight, wallace.Knight), (joan.Knave, wallace.Knave)] = saysOtherKnightThenSameType(joan, wallace)(joanSays1)\n",
    "        //  Since Wallace is a knight, then Joan is a knight.\n",
    "        val joanIsKnight: joan.Knight = sameTypeAndOtherKnightThenIsKnight(sameTypeJW, wallaceIsKnight)\n",
    "        \n",
    "        (joanIsKnight, wallaceIsKnight, bobIsKnight)\n",
    "    \n"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "a94fc1ec",
   "metadata": {},
   "source": [
    "---"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "27248a90",
   "metadata": {},
   "source": [
    "### Puzzle 2\n",
    "\n",
    "You have met a group of 4 islanders. Their names are Quentin, Beatrix, Robert, and Nancy.\n",
    "\n",
    "* Robert says: Beatrix is a knave.\n",
    "* Robert says: Nancy is lying.\n",
    "* Quentin says: Robert is a knave and I am a knave.\n",
    "\n",
    "Answer: \n",
    "\n",
    "The knaves were Quentin, Nancy, and Beatrix, and the only knight was Robert.\n",
    "\n",
    "Reasoning:\n",
    "\n",
    "* Because Quentin said 'Robert is a knave and I am a knave,' we know Quentin is not making a true statement. (If it was true, the speaker would be a knight claiming to be a knave, which cannot happen.) Therefore, Quentin is a knave and Robert is a knight.\n",
    "* All islanders will call a member of the opposite type a knave. So when Robert says that Beatrix is a knave, we know that Beatrix and Robert are opposite types. Since Robert is a knight, then Beatrix is a knave.\n",
    "* All islanders will call a member of the opposite type a knave. So when Robert says that Nancy is a knave, we know that Nancy and Robert are opposite types. Since Robert is a knight, then Nancy is a knave."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 38,
   "id": "d68d23e3",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "defined \u001b[32mfunction\u001b[39m \u001b[36mdeMorgan2\u001b[39m\r\n",
       "defined \u001b[32mfunction\u001b[39m \u001b[36mcommutativeEither\u001b[39m\r\n",
       "defined \u001b[32mtrait\u001b[39m \u001b[36mDN\u001b[39m"
      ]
     },
     "execution_count": 38,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "def deMorgan2[P, Q](thirdMiddleP: Either[P, Not[P]])(n: Not[(P, Q)]): Either[Not[P], Not[Q]] = \n",
    "    thirdMiddleP.fold(\n",
    "            p => Right((q) => n((p, q)))\n",
    "            ,\n",
    "            np => Left((p) => np(p))\n",
    "        )\n",
    "\n",
    "def commutativeEither[A,B] : Either[A, B] => Either[B, A] =\n",
    "    case Left(a) => Right(a)\n",
    "    case Right(b) => Left(b)\n",
    "\n",
    "trait DN:\n",
    "    def left[P]: Not[Not[P]] => P\n",
    "    def right[P]: P => Not[Not[P]] =\n",
    "        p => np => np(p)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 39,
   "id": "483ce9e5",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "defined \u001b[32mfunction\u001b[39m \u001b[36msaysBothKnaveThenIsKnave\u001b[39m"
      ]
     },
     "execution_count": 39,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "def saysBothKnaveThenIsKnave(using KK : KnightsAndKnaves)(x: Inhabitant, y: Inhabitant):\n",
    "        x.Says[(x.Knave, y.Knave)] => x.Knave =\n",
    "        xSays => eitherKnightOrKnave(x)(\n",
    "                xIsKnight ?=>\n",
    "                        knightsAreTruthful(x)(xSays)._1 contradicts xIsKnight,\n",
    "                xIsKnave ?=>\n",
    "                        xIsKnave\n",
    "        )"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 40,
   "id": "22d68abf",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "defined \u001b[32mfunction\u001b[39m \u001b[36msaysBothKnaveThenIsKnaveAndOtherKnight\u001b[39m"
      ]
     },
     "execution_count": 40,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "def saysBothKnaveThenIsKnaveAndOtherKnight(using KK : KnightsAndKnaves)(using dn : DN)(x: Inhabitant, y: Inhabitant):\n",
    "        x.Says[(x.Knave, y.Knave)] => x.Knave => (x.Knave, y.Knight) =\n",
    "        xSays => xIsKnave => eitherKnightOrKnave(x)(\n",
    "                xIsKnight ?=>\n",
    "                        xIsKnave contradicts xIsKnight,\n",
    "                xIsKnave ?=>\n",
    "                        val lie : Not[(x.Knave, y.Knave)] = knavesAreLiers(x)(xSays)\n",
    "                        val knaveORnnknave : Either[x.Knave, Not[x.Knave]] = commutativeEither(KK.P1(x)).fold(v => Left(v), g => Right(dn.right(g)))\n",
    "                        val eitherLie: Either[Not[x.Knave], Not[y.Knave]] = deMorgan2(knaveORnnknave)(lie)\n",
    "                        eitherLie.fold(\n",
    "                                xNotKnave => xNotKnave contradicts xIsKnave,\n",
    "                                yNotKnave => (xIsKnave, dn.left(yNotKnave))\n",
    "                        )\n",
    "        )"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 41,
   "id": "f3ea3771",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "defined \u001b[32mfunction\u001b[39m \u001b[36msaysOtherKnaveThenDiffType\u001b[39m"
      ]
     },
     "execution_count": 41,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "def saysOtherKnaveThenDiffType(using KnightsAndKnaves)(using dn: DN)(x: Inhabitant, y: Inhabitant): \n",
    "    x.Says[y.Knave] => Either[(x.Knight, y.Knave), (x.Knave, y.Knight)] = \n",
    "    xSays => eitherKnightOrKnave(x)(\n",
    "        xIsKnight ?=> \n",
    "            Left((xIsKnight, knightsAreTruthful(x)(xSays))),\n",
    "        xIsKnave ?=> \n",
    "            Right((xIsKnave, dn.left(knavesAreLiers(x)(xSays))))\n",
    "    )"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 42,
   "id": "6f9f6232",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "defined \u001b[32mfunction\u001b[39m \u001b[36mdiffTypeAndIsKnightThenOtherKnave\u001b[39m"
      ]
     },
     "execution_count": 42,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "def diffTypeAndIsKnightThenOtherKnave[P, Q]: (Either[(P, Not[Q]), (Not[P], Q)], P) => Not[Q] = \n",
    "    case (Left(_, nq),_) => nq\n",
    "    case (Right(np, _),p) => np(p)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 43,
   "id": "87627417",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "defined \u001b[32mfunction\u001b[39m \u001b[36mpuzzle2\u001b[39m"
      ]
     },
     "execution_count": 43,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "def puzzle2(using KnightsAndKnaves)(\n",
    "    quentin: Inhabitant, beatrix: Inhabitant, robert: Inhabitant, nancy: Inhabitant)(using dn: DN):\n",
    "    (robert.Says[beatrix.Knave], \n",
    "     robert.Says[nancy.Knave], \n",
    "     quentin.Says[(quentin.Knave, robert.Knave)]) => (quentin.Knave, beatrix.Knave, robert.Knight, nancy.Knave) = \n",
    "    (robertSays1, robertSays2, quentinSays) => \n",
    "        // Because Quentin said 'Robert is a knave and I am a knave,' we know Quentin is not making a true statement. \n",
    "        // (If it was true, the speaker would be a knight claiming to be a knave, which cannot happen.)\n",
    "        val quentinIsKnave : quentin.Knave = saysBothKnaveThenIsKnave(quentin, robert)(quentinSays)\n",
    "        // Therefore, Quentin is a knave and Robert is a knight. \n",
    "        val quentinIsKnaverobertIsKnight: (quentin.Knave, robert.Knight) = saysBothKnaveThenIsKnaveAndOtherKnight(quentin, robert)(quentinSays)(quentinIsKnave)\n",
    "        val robertIsKnight : robert.Knight = quentinIsKnaverobertIsKnight._2\n",
    "        // All islanders will call a member of the opposite type a knave. \n",
    "        // So when Robert says that Beatrix is a knave, we know that Beatrix and Robert are opposite types. \n",
    "        val oppositeTypeRB: Either[(robert.Knight, beatrix.Knave), (robert.Knave, beatrix.Knight)] = saysOtherKnaveThenDiffType(robert, beatrix)(robertSays1)\n",
    "        // Since Robert is a knight, then Beatrix is a knave.\n",
    "        val beatrixIsKnave: beatrix.Knave = diffTypeAndIsKnightThenOtherKnave(oppositeTypeRB, robertIsKnight)\n",
    "        // All islanders will call a member of the opposite type a knave. \n",
    "        // So when Robert says that Nancy is a knave, we know that Nancy and Robert are opposite types. \n",
    "        val oppositeTypeRN: Either[(robert.Knight, nancy.Knave), (robert.Knave, nancy.Knight)] = saysOtherKnaveThenDiffType(robert, nancy)(robertSays2)\n",
    "        // Since Robert is a knight, then Nancy is a knave.\n",
    "        val nancyIsKnave: nancy.Knave = diffTypeAndIsKnightThenOtherKnave(oppositeTypeRN, robertIsKnight)\n",
    "        \n",
    "        (quentinIsKnave, beatrixIsKnave, robertIsKnight, nancyIsKnave)\n",
    "    \n"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "7c0a9322",
   "metadata": {},
   "source": [
    "---"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "a887bed6",
   "metadata": {},
   "source": [
    "### Puzzle 3\n",
    "\n",
    "You have met a group of 6 islanders. Their names are Bob, Neil, Francine, Zelda, Henry, and Wallace.   \n",
    "\n",
    "* Bob says: Francine always tells the truth.\n",
    "* Neil says: Bob never tells the truth.\n",
    "* Francine says: Neil is untruthful.\n",
    "* Francine says: Bob is my type.\n",
    "* Henry says: Wallace never lies.\n",
    "* Henry says: Zelda always lies.\n",
    "* Francine says: Wallace is not my type.\n",
    "\n",
    "Answer: \n",
    "\n",
    "The knaves were Neil, Henry, and Wallace, and the knights were Bob, Francine, and Zelda.\n",
    "\n",
    "Reasoning:\n",
    "\n",
    "* A knight or a knave will say they are the same type as a knight. So when Francine says they are the same type as Bob, we know that Bob is a knight.\n",
    "* Both knights and knaves will say they are not the same type as a knave. So when Francine says they are a different type than Wallace, we know that Wallace is a knave.\n",
    "* All islanders will call one of their same kind a knight. So when Bob says that Francine is a knight, we know that Francine and Bob are the same type. Since Bob is a knight, then Francine is a knight.\n",
    "* All islanders will call a member of the opposite type a knave. So when Neil says that Bob is a knave, we know that Bob and Neil are opposite types. Since Bob is a knight, then Neil is a knave.\n",
    "* All islanders will call one of their same kind a knight. So when Henry says that Wallace is a knight, we know that Wallace and Henry are the same type. Since Wallace is a knave, then Henry is a knave.\n",
    "* All islanders will call a member of the opposite type a knave. So when Henry says that Zelda is a knave, we know that Zelda and Henry are opposite types. Since Henry is a knave, then Zelda is a knight."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 44,
   "id": "cadaeee3",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "defined \u001b[32mfunction\u001b[39m \u001b[36msaysSameTypeThenOtherKnight\u001b[39m"
      ]
     },
     "execution_count": 44,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "def saysSameTypeThenOtherKnight(using KnightsAndKnaves)(x: Inhabitant, y: Inhabitant): \n",
    "        x.Says[Either[(x.Knight, y.Knight), (x.Knave, y.Knave)]] => y.Knight = \n",
    "    xSays => eitherKnightOrKnave(x)(\n",
    "        xIsKnight ?=> \n",
    "            knightsAreTruthful(x)(xSays) match\n",
    "                case Left(xIsKnight, yIsKnight) => yIsKnight\n",
    "                case Right(xIsKnave, _) => xIsKnave contradicts xIsKnight,\n",
    "        xIsKnave ?=> \n",
    "            val l: (Not[(x.Knight, y.Knight)], Not[(x.Knave, y.Knave)]) = deMorgan(knavesAreLiers(x)(xSays))\n",
    "            eitherKnightOrKnave(y)(\n",
    "                yIsKnight ?=> yIsKnight , \n",
    "                yIsKnave ?=> l._2 contradicts (xIsKnave, yIsKnave)))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 45,
   "id": "cabcbe6b",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "defined \u001b[32mfunction\u001b[39m \u001b[36msaysDiffTypeThenOtherKnave\u001b[39m"
      ]
     },
     "execution_count": 45,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "def saysDiffTypeThenOtherKnave(using KnightsAndKnaves)(x: Inhabitant, y: Inhabitant): \n",
    "        x.Says[Either[(x.Knight, y.Knave), (x.Knave, y.Knight)]] => y.Knave = \n",
    "    xSays => eitherKnightOrKnave(x)(\n",
    "        xIsKnight ?=> \n",
    "            knightsAreTruthful(x)(xSays) match\n",
    "                case Left(xIsKnight, yIsKnave) => yIsKnave\n",
    "                case Right(xIsKnave, _) => xIsKnave contradicts xIsKnight,\n",
    "        xIsKnave ?=> \n",
    "            val l: (Not[(x.Knight, y.Knave)], Not[(x.Knave, y.Knight)]) = deMorgan(knavesAreLiers(x)(xSays))\n",
    "            eitherKnightOrKnave(y)(\n",
    "                yIsKnight ?=> l._2 contradicts (xIsKnave, yIsKnight), \n",
    "                yIsKnave ?=> yIsKnave)\n",
    "        )"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 46,
   "id": "153d054d",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "defined \u001b[32mfunction\u001b[39m \u001b[36msaysOtherKnightThenSameType\u001b[39m"
      ]
     },
     "execution_count": 46,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "def saysOtherKnightThenSameType(using KnightsAndKnaves)(x: Inhabitant, y: Inhabitant): \n",
    "        x.Says[y.Knight] => Either[(x.Knight, y.Knight), (x.Knave, y.Knave)] = \n",
    "    xSays => eitherKnightOrKnave(x)(\n",
    "        xIsKnight ?=> \n",
    "            Left(xIsKnight, knightsAreTruthful(x)(xSays)),\n",
    "        xIsKnave ?=> \n",
    "            Right(xIsKnave, knavesAreLiers(x)(xSays)))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 47,
   "id": "66f883d6",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "defined \u001b[32mfunction\u001b[39m \u001b[36msameTypeAndIsKnightThenOtherKnight\u001b[39m"
      ]
     },
     "execution_count": 47,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "def sameTypeAndIsKnightThenOtherKnight[P, Q]: (Either[(P, Q), (Not[P], Not[Q])], P) => Q = \n",
    "    case (Left(_, q),_) => q\n",
    "    case (Right(np, _),p) => np(p)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 48,
   "id": "14cb415d",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "defined \u001b[32mfunction\u001b[39m \u001b[36msaysOtherKnaveThenDiffType\u001b[39m"
      ]
     },
     "execution_count": 48,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "def saysOtherKnaveThenDiffType(using KnightsAndKnaves)(using dn: DN)(x: Inhabitant, y: Inhabitant): \n",
    "    x.Says[y.Knave] => Either[(x.Knight, y.Knave), (x.Knave, y.Knight)] = \n",
    "    xSays => eitherKnightOrKnave(x)(\n",
    "        xIsKnight ?=> \n",
    "            Left((xIsKnight, knightsAreTruthful(x)(xSays))),\n",
    "        xIsKnave ?=> \n",
    "            Right((xIsKnave, dn.left(knavesAreLiers(x)(xSays))))\n",
    "    )"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 49,
   "id": "fec5aa83",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "defined \u001b[32mfunction\u001b[39m \u001b[36mdiffTypeAndOtherKnightThenIsKnave\u001b[39m"
      ]
     },
     "execution_count": 49,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "def diffTypeAndOtherKnightThenIsKnave[P, Q]: (Either[(P, Not[Q]), (Not[P], Q)], Q) => Not[P] = \n",
    "    case (Left(_, nq),q) => nq(q)\n",
    "    case (Right(np, _),_) => np"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 50,
   "id": "18c49720",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "defined \u001b[32mfunction\u001b[39m \u001b[36msameTypeAndOtherKnaveThenIsKnave\u001b[39m"
      ]
     },
     "execution_count": 50,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "def sameTypeAndOtherKnaveThenIsKnave[P, Q]: (Either[(P, Q), (Not[P], Not[Q])], Not[Q]) => Not[P] = \n",
    "    case (Left(_, q),nq) => nq(q)\n",
    "    case (Right(np,_),_) => np"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 51,
   "id": "997ce949",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "defined \u001b[32mfunction\u001b[39m \u001b[36mdiffTypeAndIsKnaveThenOtherKnight\u001b[39m"
      ]
     },
     "execution_count": 51,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "def diffTypeAndIsKnaveThenOtherKnight[P, Q]: (Either[(P, Not[Q]), (Not[P], Q)], Not[P]) => Q = \n",
    "    case (Left(p, _),np) => np(p)\n",
    "    case (Right(_, q),_) => q"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 52,
   "id": "3e79af02",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "defined \u001b[32mfunction\u001b[39m \u001b[36mpuzzle3\u001b[39m"
      ]
     },
     "execution_count": 52,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "def puzzle3(using KnightsAndKnaves)(\n",
    "    bob: Inhabitant, neil: Inhabitant, francine: Inhabitant, zelda: Inhabitant, henry: Inhabitant, wallace: Inhabitant)(using dn: DN):\n",
    "        (bob.Says[francine.Knight], \n",
    "         neil.Says[bob.Knave], \n",
    "         francine.Says[neil.Knave],\n",
    "         francine.Says[Either[(francine.Knight, bob.Knight),(francine.Knave, bob.Knave)]],\n",
    "         henry.Says[wallace.Knight],\n",
    "         henry.Says[zelda.Knave],\n",
    "         francine.Says[Either[(francine.Knight, wallace.Knave),(francine.Knave, wallace.Knight)]]) => (neil.Knave, henry.Knave, wallace.Knave, bob.Knight, francine.Knight, zelda.Knight) = \n",
    "        (bobSays, neilSays, francineSays1, francineSays2, henrySays1, henrySays2, francineSays3) => \n",
    "                // A knight or a knave will say they are the same type as a knight. \n",
    "                // So when Francine says they are the same type as Bob, we know that Bob is a knight.\n",
    "                val bobIsKnight: bob.Knight = saysSameTypeThenOtherKnight(francine, bob)(francineSays2)\n",
    "                // Both knights and knaves will say they are not the same type as a knave. \n",
    "                // So when Francine says they are a different type than Wallace, we know that Wallace is a knave.\n",
    "                val wallaceIsKnave: wallace.Knave = saysDiffTypeThenOtherKnave(francine, wallace)(francineSays3)\n",
    "                // All islanders will call one of their same kind a knight. \n",
    "                // So when Bob says that Francine is a knight, we know that Francine and Bob are the same type. \n",
    "                val sameTypeBF: Either[(bob.Knight, francine.Knight),(bob.Knave, francine.Knave)] = saysOtherKnightThenSameType(bob, francine)(bobSays)\n",
    "                // Since Bob is a knight, then Francine is a knight.\n",
    "                val francineIsKnight: francine.Knight = sameTypeAndIsKnightThenOtherKnight(sameTypeBF, bobIsKnight)\n",
    "                // All islanders will call a member of the opposite type a knave. \n",
    "                // So when Neil says that Bob is a knave, we know that Bob and Neil are opposite types. \n",
    "                val oppositeTypeNB: Either[(neil.Knight, bob.Knave), (neil.Knave, bob.Knight)] = saysOtherKnaveThenDiffType(neil, bob)(neilSays)\n",
    "                // Since Bob is a knight, then Neil is a knave. \n",
    "                val neilIsKnave: neil.Knave = diffTypeAndOtherKnightThenIsKnave(oppositeTypeNB, bobIsKnight)\n",
    "                // All islanders will call one of their same kind a knight. \n",
    "                // So when Henry says that Wallace is a knight, we know that Wallace and Henry are the same type. \n",
    "                val sameTypeHW: Either[(henry.Knight, wallace.Knight),(henry.Knave, wallace.Knave)] = saysOtherKnightThenSameType(henry, wallace)(henrySays1)\n",
    "                // Since Wallace is a knave, then Henry is a knave.\n",
    "                val henryIsKnave: henry.Knave = sameTypeAndOtherKnaveThenIsKnave(sameTypeHW, wallaceIsKnave)\n",
    "                // All islanders will call a member of the opposite type a knave. \n",
    "                // So when Henry says that Zelda is a knave, we know that Zelda and Henry are opposite types. \n",
    "                val oppositeTypeHZ: Either[(henry.Knight, zelda.Knave), (henry.Knave, zelda.Knight)] = saysOtherKnaveThenDiffType(henry, zelda)(henrySays2)\n",
    "                // Since Henry is a knave, then Zelda is a knight.\n",
    "                val zeldaIsKnight: zelda.Knight = diffTypeAndIsKnaveThenOtherKnight(oppositeTypeHZ, henryIsKnave)\n",
    "                (neilIsKnave, henryIsKnave, wallaceIsKnave, bobIsKnight, francineIsKnight, zeldaIsKnight)"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Scala 3.3",
   "language": "scala",
   "name": "scala33"
  },
  "language_info": {
   "codemirror_mode": "text/x-scala",
   "file_extension": ".sc",
   "mimetype": "text/x-scala",
   "name": "scala",
   "nbconvert_exporter": "script",
   "version": "2.13.12"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}