diff --git a/demo.ipynb b/demo.ipynb
index 5a2a429..38c2720 100644
--- a/demo.ipynb
+++ b/demo.ipynb
@@ -1,1086 +1,1431 @@
{
"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 tatics\n",
"- The equivalence between LEM and DNE\n",
"- The soundness of STLC\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 have a better understanding of Curry-Howard corespondence and its role in Coq\n",
"- you can do simple proofs in Coq\n",
"\n"
]
},
{
"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": 1,
"metadata": {
"coq_kernel_metadata": {
"auto_roll_back": true,
"cell_id": "825f10d1ce154c34af48b10b4d22130c",
"evaluated": true,
"execution_id": "1108c94f825442ec862692136097969d",
"rolled_back": false
},
"scrolled": true
},
"outputs": [
{
"data": {
"text/html": [
"\n",
"
\n"
],
"text/plain": [
"Error: The reference double was not found in the current environment."
]
},
"execution_count": 8,
"metadata": {
"coq_kernel_evaluated": false,
"coq_kernel_execution_id": "186f1e496640486a957c7b5ab67b7fb7",
"coq_kernel_rolled_back": false
},
"output_type": "execute_result"
}
],
"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": 8,
"metadata": {
"coq_kernel_metadata": {
"auto_roll_back": false,
"cell_id": "a5059f058cc242d4845372dfaf7f27e8",
"evaluated": true,
"execution_id": "57ca315e13744eb58f32703a168992f4",
"rolled_back": false
},
"scrolled": true
},
"outputs": [
{
"data": {
"text/html": [
"\n",
"
\n",
" \n",
"
\n",
"\n",
"
\n",
" \n",
" Cell evaluated.\n",
"
\n",
"\n",
"
\n",
" \n",
" Cell rolled back.\n",
"
\n",
"\n",
"
\n",
" \n",
"\n",
"
\n",
" \n",
" Auto rollback\n",
"
\n",
"
\n"
],
"text/plain": []
},
"execution_count": 10,
"metadata": {
"coq_kernel_evaluated": true,
"coq_kernel_execution_id": "57ca315e13744eb58f32703a168992f4",
"coq_kernel_rolled_back": false
},
"output_type": "execute_result"
}
],
"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": 10,
"metadata": {
"coq_kernel_metadata": {
"auto_roll_back": false,
"cell_id": "613bdcf8cb014b83b6803c57ba6220ed",
"evaluated": true,
"execution_id": "d1b95e42535a450eb5623a10c461aea8",
"rolled_back": false
}
},
"outputs": [
{
"data": {
"text/html": [
"\n",
"
\n"
],
"text/plain": []
},
"execution_count": 14,
"metadata": {
"coq_kernel_evaluated": true,
"coq_kernel_execution_id": "11ef805b36d749838f1ec162fbe8c29f",
"coq_kernel_rolled_back": false
},
"output_type": "execute_result"
}
],
"source": [
"Fixpoint factorial (n:nat) : nat\n",
" (* := ??? *). Admitted."
]
},
{
"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 types are 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 intutionist 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": "03f36c5cedea47028bd48f91cb6e2cb8",
"evaluated": true,
"execution_id": "1fbfd4d5c4e642a1825792ab6fb96934",
"rolled_back": false
}
},
"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": [
"**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 define an inductive type without any constructors, thus it is impossible for a term to inhabit the type.\n",
+ "**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 intutionistic 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": [
+ "## 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 construction](https://en.wikipedia.org/wiki/Calculus_of_constructions).\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 types_, 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 need to define the predicate `even`: "
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 17,
+ "metadata": {
+ "coq_kernel_metadata": {
+ "auto_roll_back": true,
+ "cell_id": "2973d5394486467fb793b828c4a58bf2",
+ "evaluated": true,
+ "execution_id": "818dcd4d709c4b86af1c963249992cdf",
+ "rolled_back": false
+ },
+ "scrolled": true
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/html": [
+ "\n",
+ "
\n",
+ " \n",
+ "
\n",
+ "\n",
+ "
\n",
+ " \n",
+ " Cell evaluated.\n",
+ "
\n",
+ "\n",
+ "
\n",
+ " \n",
+ " Cell rolled back.\n",
+ "
\n",
+ "\n",
+ "
\n",
+ " \n",
+ "\n",
+ "
\n",
+ " \n",
+ " Auto rollback\n",
+ "
\n",
+ "
\n"
+ ],
+ "text/plain": []
+ },
+ "execution_count": 36,
+ "metadata": {
+ "coq_kernel_evaluated": true,
+ "coq_kernel_execution_id": "818dcd4d709c4b86af1c963249992cdf",
+ "coq_kernel_rolled_back": false
+ },
+ "output_type": "execute_result"
+ }
+ ],
+ "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": 45,
+ "metadata": {
+ "coq_kernel_metadata": {
+ "auto_roll_back": true,
+ "cell_id": "8a15a5495077495390f9cdffda2539cb",
+ "evaluated": false,
+ "execution_id": "f81281ca773948ca8830e249bbd23862",
+ "rolled_back": false
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/html": [
+ "\n",
+ "