{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "# A Short Introduction to Coq\n",
    "\n",
    "\n",
    "In this tutorial, we are going to play with [Coq](https://coq.inria.fr/), which is a popular proof assitant based on solid [type theories](https://en.wikipedia.org/wiki/Calculus_of_constructions).\n",
    "\n",
    "This tutorial contains the following content:\n",
    "\n",
    "- Basic functional programming in Coq\n",
    "- Curry-Howard correspondence\n",
    "- First-order Logic\n",
    "- Proof by tactics\n",
    "- The equivalence between LEM and DNE\n",
    "\n",
    "In the above, LEM refers to the [law of excluded middle](https://en.wikipedia.org/wiki/Law_of_excluded_middle), DNE refers to the [law of double negation](https://en.wikipedia.org/wiki/Double_negation).\n",
    "\n",
    "After this tutorial, we hope that\n",
    "\n",
    "- you understand how Curry-Howard corespondence is embodied in Coq\n",
    "- you can do simple proofs in Coq with and without tactics"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "## Basic Functional Programming in Coq"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "The core of Coq is a functional programming language, called Gallina. It offers features like _algebraic data types_, _pattern matching_, _parametric polymorphism_, as commonly supported by functional languages."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "We create a playground, so that the names will not clash with definitions from Coq."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true,
     "cell_id": "e92282ad107c41f28fa980c940a82449",
     "execution_id": "8aa0beb5e1e6477d98d9d8426182a68a"
    },
    "scrolled": true
   },
   "outputs": [],
   "source": [
    "Module FPPlayground."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "We may define a type for booleans as follows:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": false,
     "cell_id": "0abfc9828952473f8a29b34a4e30d9ff",
     "execution_id": "c9ad6ecec7b94b1186edbaf54bec71ca"
    },
    "scrolled": false
   },
   "outputs": [],
   "source": [
    "Inductive bool : Set :=\n",
    "  | true\n",
    "  | false."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "The type `Set` indicates that the type `bool` is not a proposition, but a \"value\" type."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "With the definition above, we can define the common boolean operations:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": false,
     "cell_id": "7790d819124b4933b66c00b68bf4e80c",
     "execution_id": "0ab1807e74f8434c86c730701f22ee07"
    },
    "scrolled": true
   },
   "outputs": [],
   "source": [
    "Definition negb (b:bool) : bool :=\n",
    "  match b with\n",
    "  | true => false\n",
    "  | false => true\n",
    "  end.\n",
    "\n",
    "Definition andb (b1:bool) (b2:bool) : bool :=\n",
    "  match b1 with\n",
    "  | true => b2\n",
    "  | false => false\n",
    "  end.\n",
    "\n",
    "Definition orb (b1:bool) (b2:bool) : bool :=\n",
    "  match b1 with\n",
    "  | true => true\n",
    "  | false => b2\n",
    "  end."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "Natural numbers can be defined as follows:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": false,
     "cell_id": "eb3c2797d48a4eb3b65dd2c2f49c2a2d",
     "execution_id": "c0fe58c6e3ae43df83ffef475121c223"
    },
    "scrolled": true
   },
   "outputs": [],
   "source": [
    "Inductive nat : Set :=\n",
    "  | O\n",
    "  | S (n : nat)."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true,
     "cell_id": "a42297630f54425d8f318b823d59457c",
     "execution_id": "93025c91cb7f40c484657134fecca622"
    }
   },
   "source": [
    "Now we can define the predecessor function:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": false,
     "cell_id": "704e0c9597bf4f338a38d7d2f1664610",
     "execution_id": "6fd56273027a4c528ada411bac6ab983"
    }
   },
   "outputs": [],
   "source": [
    "Definition pred (n : nat) : nat :=\n",
    "  match n with\n",
    "    | O => O\n",
    "    | S n' => n'\n",
    "  end."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "Let's now define a function that doubles its argument:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true,
     "cell_id": "8edd83ba67004246bd579289154f1e8d",
     "execution_id": "341e26f0d294433588bd96ffa21eb1a9"
    }
   },
   "outputs": [],
   "source": [
    "Definition double (n : nat) : nat :=\n",
    "  match n with\n",
    "    | O => O\n",
    "    | S n' => S (S (double n'))\n",
    "  end."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "Oops! Coq complains that `double` was not found. We need to use the keyword `Fixpoint`:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": false,
     "cell_id": "c9cb343ec7954b048dfcff92a54389ea",
     "execution_id": "bfb1a541480648328c46a3ad4e19d9a6"
    },
    "scrolled": true
   },
   "outputs": [],
   "source": [
    "Fixpoint double (n : nat) : nat :=\n",
    "  match n with\n",
    "    | O => O\n",
    "    | S n' => S (S (double n'))\n",
    "  end."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "Why the complexity? The reason is that in the above, `double` is a recursive function. You might remember from TAPL that unrestricted general recursion can make any type inhabited. By Curry-Howard correspondance, it means that any proposition can be proved true!\n",
    "\n",
    "Consequently, recursive functions must terminate in order to be accepted by Coq. Coq uses a simple mechanism to check termination of recursive calls, namely _structural recursion_: the recursive call must take an argument which is _structurally_ smaller."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": false,
     "cell_id": "9eb8a2526eab4e8e8a7865f8a5496d69",
     "execution_id": "5afc43921fc04a1d9fedba5ccd267cb8"
    }
   },
   "outputs": [],
   "source": [
    "Fixpoint plus (n : nat) (m : nat) : nat :=\n",
    "  match n with\n",
    "    | O => m\n",
    "    | S n' => S (plus n' m)\n",
    "  end."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "**Exercise 1**: Factorial\n",
    "\n",
    "Please implement the `factorial` function given below:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": false,
     "cell_id": "4bd2f25a3213447d85fa2da3fb885703",
     "execution_id": "61424b35157a4fd0891e018b2d09ed28"
    }
   },
   "outputs": [],
   "source": [
    "Fixpoint factorial (n:nat) : nat\n",
    "  (* := ??? *). Admitted."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": false,
     "cell_id": "7fff38a63174499984e1762c005749e5",
     "execution_id": "b5a62a0e45954c46b55e711d79e22996"
    }
   },
   "outputs": [],
   "source": [
    "End FPPlayground."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "## Curry-Howard correspondence"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "As we learned from class lectures, [Curry-Howard correspondence](https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence) plays a critical role in proof assitants that are based on type theories. The key insight is that\n",
    "\n",
    "- proofs are programs, and\n",
    "- propositions are types\n",
    "\n",
    "To show that a proposition is provable, it suffices to show that the corresponding type is inhabited by a program. In this section we will see how this correspondence is embodied in Coq."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "**Implication**. The most important correspondence is between the function type `A -> B` and implication `A -> B`. Consequently, the proof of `A -> B` is a function of the type `A -> B`. By the [BHK interpretation](https://en.wikipedia.org/wiki/Brouwer%E2%80%93Heyting%E2%80%93Kolmogorov_interpretation) of intuitionist logic, a function that proves `A -> B` basically transforms the proof of `A` to the proof of `B`.\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true,
     "cell_id": "264bebc3b80945b3948d47d83e09ac74",
     "execution_id": "1fbfd4d5c4e642a1825792ab6fb96934"
    }
   },
   "source": [
    "**Conjunction**. The proposition `A /\\ B` is represented by a product type:\n",
    "\n",
    "\n",
    "```Coq\n",
    "Inductive and (A B:Prop) : Prop :=\n",
    "  conj : A -> B -> A /\\ B\n",
    "where \"A /\\ B\" := (and A B) : type_scope.\n",
    "```\n",
    "\n",
    "Note that the constructor `conj` has the type `A -> B -> A /\\ B`, which can be read as _given a proof of A and a proof of B, then we can construct a proof of A /\\ B_.\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "In the above, the type `Prop` refers to propositions."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "**Disjunction**. A disjunction `A \\/ B` means either we have a proof of `A` or a proof of `B`, thus it is naturally represented by a sum type:\n",
    "\n",
    "```Coq\n",
    "Inductive or (A B:Prop) : Prop :=\n",
    "  | or_introl : A -> A \\/ B\n",
    "  | or_intror : B -> A \\/ B\n",
    "where \"A \\/ B\" := (or A B) : type_scope.\n",
    "```"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "**If and only if**. The proposition `A <-> B` is embodied by the type `(A -> B) /\\ (B -> A)`, consequently the proof will be a tuple of functions.\n",
    "\n",
    "```Coq\n",
    "Definition iff (A B:Prop) := (A -> B) /\\ (B -> A).\n",
    "Notation \"A <-> B\" := (iff A B) : type_scope.\n",
    "```"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "**False**. Which type corresponds to the proposition `False`? As we can never prove `False`, it should correspond to a type that is not inhabited. This can be done in Coq by defining an inductive type without any constructors, thus it is impossible for a term to inhabit the type.\n",
    "\n",
    "```Coq\n",
    "Inductive False : Prop :=.\n",
    "```"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "**Negation**. How to represent the proposition `~A` in types? In intuitionistic logic, `~A` is interpreted as `A -> False`, i.e., a proof of `A` will lead to absurdity.\n",
    "\n",
    "```Coq\n",
    "Definition not (A:Prop) := A -> False.\n",
    "```\n",
    "\n",
    "Consequently, `~~A` is the same as `(A -> False) -> False`."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "As an exercise, let's prove the following theorem, which says that for any proposition `P`, we may prove `~~P` from `P`:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true,
     "cell_id": "5477c8b7ab764a338539e4558104e8a9",
     "execution_id": "bd5c6da0e1dc480c894f4195fb9d42fb"
    }
   },
   "outputs": [],
   "source": [
    "Definition neg_fun_prop: Prop := forall P: Prop, P -> ~~P."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "The proof is just a function that has the type `neg_fun_prop`:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true,
     "cell_id": "d0424c5bdbd148a884545bf755d0913e",
     "execution_id": "1cb148d287b245ce92f6b98ff8bbf649"
    }
   },
   "outputs": [],
   "source": [
    "Definition neg_fun_proof := fun (P:Prop) (p: P) (np: ~P) => np p."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "Let's check the type to see it's indeed the proof:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true,
     "cell_id": "f7826cb6b1bd47c5844df0ae0c8027ba",
     "execution_id": "c8e18c7c8c8b418aa0fd2f3aa68ccd05"
    },
    "scrolled": true
   },
   "outputs": [],
   "source": [
    "Check neg_fun_proof."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "The type is equivalent to `neg_fun_prop`:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true,
     "cell_id": "5a7bbf3e43fa4da981d9b5d951b87294",
     "execution_id": "ebb20a5335db4ba188d06df0b995acdc"
    }
   },
   "outputs": [],
   "source": [
    "Check neg_fun_proof: neg_fun_prop."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "## First-order logic\n",
    "\n",
    "So far, what we have seen are formulas of propositional logic. You might be wondering, what about first-order logic formulas, e.g. $\\forall x \\in A.P(x)$ and $\\exists x \\in A.P(x)$? That leads us to [dependent types](https://en.wikipedia.org/wiki/Dependent_type). Coq is based on a dependent type theory called [calculus of inductive constructions](https://coq.inria.fr/distrib/current/refman/language/cic.html).\n",
    "\n",
    "The most important type in dependent type theories is the $\\Pi$-type, which is of the form $\\Pi_{x:A}B(x)$. $\\Pi$ types denote _dependent functions_, whose return _type_ depends on the parameter of the function. In Coq, the $\\Pi$ type is written as `forall x:A, B`. We illustrate by proving the following theorem:\n",
    "\n",
    "$$\\forall x \\in nat. even(double(x))$$\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "First, we reproduce the definitions of `nat` and `double` below."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true,
     "cell_id": "f18e5ae7b4f6492c8e1bbfd79dc2065c",
     "execution_id": "11e008b2833a4da488927e3ed9b59cd3"
    }
   },
   "outputs": [],
   "source": [
    "Module FOPlayground.\n",
    "\n",
    "Inductive nat : Type :=\n",
    "  | O\n",
    "  | S (n : nat).\n",
    "\n",
    "Fixpoint double (n : nat) : nat :=\n",
    "  match n with\n",
    "    | O => O\n",
    "    | S n' => S (S (double n'))\n",
    "  end."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "Next, we need to define the predicate `even`: "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true,
     "cell_id": "598e4269ad3d45ad84953db2a14a76d3",
     "execution_id": "639b001901a84ba087fd087ca317e994"
    },
    "scrolled": true
   },
   "outputs": [],
   "source": [
    "Inductive even : nat -> Prop :=\n",
    "  | even0 : even O\n",
    "  | evenS : forall x:nat, even x -> even (S (S x))."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "The definition says that `O` is even, and if `x` is even, then `S S x` is even. Now we can define the proposition formally:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true,
     "cell_id": "bf561732a5c646a8930a71eca9670147",
     "execution_id": "3c88606ae61e4c8f8cfee8319d42e2fc"
    }
   },
   "outputs": [],
   "source": [
    "Definition even_prop: Prop := forall x:nat, even (double x)."
   ]
  },
  {
   "source": [
    "The proof is just a recursive function:"
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true,
     "cell_id": "cc128a942afe4df786efa3932fa2c5e8",
     "execution_id": "633ebc64fda741a2adbcff3b51131837"
    }
   },
   "outputs": [],
   "source": [
    "Fixpoint even_proof(x: nat): even (double x) :=\n",
    "  match x with\n",
    "  | O      => even0\n",
    "  | S n'   => evenS (double n') (even_proof n')\n",
    "  end."
   ]
  },
  {
   "source": [
    "Note that in the above, the recursion is well-founded, because it is structurally decreasing on `x`."
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "We can check the type to see we actually proved the theorem:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true,
     "cell_id": "925a62737f6b42ac929be6190f2ea753",
     "execution_id": "e9f354ebab2742d3a679b9ac4220936b"
    }
   },
   "outputs": [],
   "source": [
    "Check even_proof: even_prop."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "This example reveals the essence of _proof by induction_ from the perspective of type theory: it is just structural recursion."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true,
     "cell_id": "eda1f71f86b748be84f533f7c734105c",
     "execution_id": "3dccf0fb307f40a2bf03d5c05871d8c8"
    }
   },
   "outputs": [],
   "source": [
    "End FOPlayground."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "From the above, it is clear that universal quantification can be encoded as $\\Pi$ types. But what about existential quantification? In Coq, existential quantification is encoded as follows:\n",
    "\n",
    "```Coq\n",
    "Inductive ex (A:Type) (P:A -> Prop) : Prop :=\n",
    "  ex_intro : forall x:A, P x -> ex (A:=A) P.\n",
    "```"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "Equality (strictly speaking _propositional equality_) is also encoded by an inductive type:\n",
    "\n",
    "```Coq\n",
    "Inductive eq (A:Type) (x:A) : A -> Prop :=\n",
    "    eq_refl : x = x :>A\n",
    "```"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "And the type `A -> B` is a special case of $\\Pi$ types:\n",
    "\n",
    "```Coq\n",
    "Notation \"A -> B\" := (forall (_ : A), B) : type_scope.\n",
    "```"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "You may find more information about the encoding of logic in Coq here: https://coq.inria.fr/stdlib/Coq.Init.Logic.html."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true,
     "cell_id": "cfedc29e1ac44c48815fd45b89bd2473",
     "execution_id": "37ec84e6650f49d6b2ba6072ab9385b7"
    }
   },
   "source": [
    "**Exercise 2**: Define an inductive predicate `odd`, and prove that `forall n:nat, odd (S (double n))`."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "## Introduction to proofs by tactics"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "As you have seen in previous examples, doing proofs by writing functions is very different from how proofs are usually done. Fortunately, Coq comes with a language called [_Ltac_,](https://coq.inria.fr/refman/proof-engine/ltac.html), which enables an imperative proving style that is more natural. Ltac also makes it possible to define heuristics to automate some proofs. Ltac only helps to synthesize the proofs, thus even if there are bugs in Ltac, it is not an issue --- all programs or proofs have to be checked by a small trusted core.\n",
    "\n",
    "In the following, we assume the definitions in standard library: https://coq.inria.fr/stdlib/Coq.Init.Datatypes.html.\n",
    "\n",
    "**Tactics 101**. Let's see how to use the common tactics to do proofs in Coq. We first define the theorem to be proved:\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true,
     "cell_id": "9715859f4f0a476b84f0909e59cb9e7e",
     "execution_id": "9626e7f7c0494ed89b121d34daa6e3f3"
    }
   },
   "outputs": [],
   "source": [
    "Theorem neg_fun: forall P: Prop, P -> ~~P."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "From the output, we see there is one proof goal. We start proof by writing `Proof`"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true,
     "cell_id": "ab1ef59cfdb04c579c09010a8c74bbbc",
     "execution_id": "734fd493b2864d868e598bdffe1355d2"
    }
   },
   "outputs": [],
   "source": [
    "Proof."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "If the goal is universal quantification or implication, we can use `intros` to introduce the conditions as premises:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true,
     "cell_id": "45f70ed206e14f53b7704dd527e7584e",
     "execution_id": "cd25e327b99c41ea82d8bafa69735de7"
    }
   },
   "outputs": [],
   "source": [
    "intros."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "As introduced before, `~P` is defined as `P -> False`. We can use `unfold` to expand the definition:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true,
     "cell_id": "c9c06ba1f4b44b6f84ab98f031a795d9",
     "execution_id": "ec44e53fbfa54a5c9fe41eae0453b10c"
    }
   },
   "outputs": [],
   "source": [
    "unfold not."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "Now we can use `intros` again:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true,
     "cell_id": "ea08af0b36864f4e9efad9057407db90",
     "execution_id": "0776b298d05840d9884139aa5f8c17d0"
    }
   },
   "outputs": [],
   "source": [
    "intros."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "Now we see that the proof goal is the return type of `H0`, the tactic `apply` is useful in this case:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true,
     "cell_id": "eda1d89189fa4f1daa204f4adf27dedd",
     "execution_id": "78300f2fa145478d9f30d54fb00b19a8"
    }
   },
   "outputs": [],
   "source": [
    "apply H0."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "Now we see the proof goal `P` is already a given premise, we can use `exact` to complete the proof:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true,
     "cell_id": "7171145e1c4d404894a963fd456ca82b",
     "execution_id": "3250e5850a0a4d198c3319c92e19b8d3"
    }
   },
   "outputs": [],
   "source": [
    "exact H."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "Now we can end the proof by `QED`:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true,
     "cell_id": "03b405c509e24efc8dee8d731a8aeb8c",
     "execution_id": "80576450b1254e67ad7ef3fd791bb681"
    }
   },
   "outputs": [],
   "source": [
    "Qed."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true,
     "cell_id": "fa90a0e938ca436093820c77b5868661",
     "execution_id": "3b382b67bcd241d68b9ff6c0973e13e4"
    }
   },
   "source": [
    "We put all the proof steps together for readability:\n",
    "\n",
    "```Coq\n",
    "Theorem neg_fun: forall P: Prop, P -> ~~P.\n",
    "Proof.\n",
    "  intros. unfold not. intros. apply H0. exact H.\n",
    "Qed.\n",
    "```"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "**Proof by simplification**. When the proof goals involves definition of functions, the tactic `simpl` is handy. For example, we may prove"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true,
     "cell_id": "60c8f37ea88443cc897629a7328d4554",
     "execution_id": "a10fcc61b8594a19829ec838cc355cd1"
    }
   },
   "outputs": [],
   "source": [
    "Theorem plus_11: 7 + 4 = 6 + 5.\n",
    "Proof."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true,
     "cell_id": "9ed0fc1f7e5745ee9382ee893b7be6ae",
     "execution_id": "d4a9be90b423487a9d42fa380c5fea96"
    }
   },
   "outputs": [],
   "source": [
    "simpl."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "The tactic `reflexivity` can be use to prove `a = a` and completes the proof: "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true,
     "cell_id": "406d4dd69d7b4e86a4038bbad479eab4",
     "execution_id": "aa06b28aa57b4b3b9cfb841885a41c7b"
    }
   },
   "outputs": [],
   "source": [
    "reflexivity.\n",
    "Qed."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "**Proof by rewriting**. To take advantage of known equalities, we can use the tactic `rewrite`. For example, we may prove"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true,
     "cell_id": "830efa8c27924ed381f34d74e33f9198",
     "execution_id": "550d08762a324f53801fcd4f48f66411"
    }
   },
   "outputs": [],
   "source": [
    "Theorem eq_rewrite: forall m n:nat, m = n -> m + 2 = n + 2.\n",
    "Proof.\n",
    "  intros m n H. rewrite -> H. reflexivity.\n",
    "Qed."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "**Proof by case analysis**. In the following, we can use `destruct` on do case analysis on the value of `b`:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true,
     "cell_id": "9c29ffb4e4f64fe188bad472dd0fa87a",
     "execution_id": "29ee225ace9346578b2c937d118b659c"
    }
   },
   "outputs": [],
   "source": [
    "Theorem neg_eql : forall b : bool, negb (negb b) = b.\n",
    "Proof.\n",
    "  intros b. destruct b.\n",
    "  (* case 1 *) simpl. reflexivity.\n",
    "  (* case 2 *) simpl. reflexivity.\n",
    "Qed.\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "**Proof by induction**. Here we can redo the proof of `even(double(n))` with the tactic `induction`:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true,
     "cell_id": "63b5dc9cd3d34a129e8d33dc56025bfa",
     "execution_id": "41f01b0f40474ef480d715ccc8cc18ac"
    }
   },
   "outputs": [],
   "source": [
    "Fixpoint double (n : nat) : nat :=\n",
    "  match n with\n",
    "    | 0 => 0\n",
    "    | S n' => S (S (double n'))\n",
    "  end.\n",
    "\n",
    "Inductive even : nat -> Prop :=\n",
    "  | even0 : even 0\n",
    "  | evenS : forall n:nat, even n -> even (S (S n)).\n",
    "\n",
    "Theorem even_prop: forall n:nat, even (double n).\n",
    "Proof.\n",
    "  intros n. induction n as [|n' IH].\n",
    "  (* case 1 *) simpl. constructor.\n",
    "  (* case 1 *) simpl. constructor. exact IH.\n",
    "  Show Proof. (* show the synthesized proof term *)\n",
    "Qed."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "You can find the full list of tactics in Coq [here](https://coq.inria.fr/refman/coq-tacindex.html)."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "**Exercise 3**: Prove commutativity of addition (tip: prove a lemma first):"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true,
     "cell_id": "910f646a33a542718398b65ecf99f913",
     "execution_id": "143d8203473a4718826a95e5af78d863"
    }
   },
   "outputs": [],
   "source": [
    "Theorem add_commutativity: forall m n:nat, m + n = n + m.\n",
    "Proof. Admitted."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "## The equivalence between LEM and DNE"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "Curry-Howard correspondence is usually formulated only for _intuitionistic logics_ (IL), in which the _law of excluded middle_ (LEM) or equivalently the _law of double negation_ (DNE) does not hold. Concretely, the following propositions\n",
    "are not provable in IL, thus by the correspondence there exists no programs in Coq that prove them:\n",
    "\n",
    "- LEM: $\\forall P.P \\vee \\neg P$\n",
    "- DNE: $\\forall P.\\neg \\neg P \\to P$\n",
    "\n",
    "This problem is about proving that intuitionistic logic with the law of excluded\n",
    "middle is equivalent to intuitionistic logic with the law of double negation,\n",
    "that is IL + LEM = IL + DNE."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "First, we formulate the proof goal formally:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true,
     "cell_id": "a651edec609b4949b471f477b1bc64a9",
     "execution_id": "7c6b5aaf0fbd417fa75df59241b9b8e1"
    }
   },
   "outputs": [],
   "source": [
    "Definition LEM_DNE_EQ: Prop := (forall P: Prop, P \\/~P) <-> (forall P: Prop, ~~P -> P)."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "The forward direction is relatively easy:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true,
     "cell_id": "33f7ffd354db4f25a85d795abc867a00",
     "execution_id": "a039ec9f557843ddb5edd30a4ff96d87"
    }
   },
   "outputs": [],
   "source": [
    "Theorem LEM_DNE: (forall P: Prop, P \\/~P) -> (forall P: Prop, ~~P -> P).\n",
    "Proof.\n",
    "  intros H P nnp. destruct (H P) as [p|np].\n",
    "  exact p. destruct (nnp np).\n",
    "Qed."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "The reverse direction needs some trick, in particular the three usage of `pose`:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true,
     "cell_id": "3d6ce61372a348f6871ccc20d69d6eb7",
     "execution_id": "ae6e800282404bca817b1d1ee0ffc3da"
    }
   },
   "outputs": [],
   "source": [
    "Theorem DNE_LEM: (forall P: Prop, ~~P -> P) -> (forall P: Prop, P \\/~P).\n",
    "Proof.\n",
    "  intros H P. pose (H (P \\/ ~P)) as H1.\n",
    "  apply H1. intros H2.\n",
    "  pose (fun p:P => H2 (or_introl p)) as H3.\n",
    "  pose (fun p:~P => H2 (or_intror p)) as H4.\n",
    "  apply H4.\n",
    "  exact H3.\n",
    "Qed."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "Now we can just combine the two sub-proofs together:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true,
     "cell_id": "21bd3722786344259527b091c7951a7f",
     "execution_id": "5eb9df9ec3044a1a81a2e27f58deada8"
    }
   },
   "outputs": [],
   "source": [
    "Definition proof_for_eq := conj LEM_DNE DNE_LEM."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "Let's check if the proof indeed has the right type:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true,
     "cell_id": "3d41919c067d482a8e0804292a059fea",
     "execution_id": "bceb3b607b314421a78daa1327bf587f"
    }
   },
   "outputs": [],
   "source": [
    "Check proof_for_eq : LEM_DNE_EQ."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true,
     "cell_id": "de09d8a863504feebbb1013ea44edba8",
     "execution_id": "e48c7d8c4f5c40aa81b0cec86da84f27"
    }
   },
   "source": [
    "Voila! To understand better how the proof works, the following exercise is highly recommended:"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "**Exercise 4**: Redo the proof by implementing a function that has the type `LEM_DNE_EQ` without using tactics."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "## Going further"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "coq_kernel_metadata": {
     "auto_roll_back": true
    }
   },
   "source": [
    "We only scratched the surface of Coq. The following resources are useful if you want to go further:\n",
    "\n",
    "- [Software Foundations](https://softwarefoundations.cis.upenn.edu/current/index.html)\n",
    "- [Type Safety in Three Easy Lemmas](http://siek.blogspot.com/2013/05/type-safety-in-three-easy-lemmas.html) and the [code](https://gist.github.com/dkrustev/5890291)\n",
    "- [The calculus of constructions](https://hal.inria.fr/file/index/docid/76024/filename/RR-0530.pdf), _T. Coquand, Gérard Huet_, 1986\n",
    "- [Calculus of Inductive Constructions](https://coq.inria.fr/distrib/current/refman/language/cic.html)"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Coq",
   "language": "coq",
   "name": "coq"
  },
  "language_info": {
   "file_extension": ".v",
   "mimetype": "text/x-coq",
   "name": "coq",
   "version": "8.9.1"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}