**This TD will be noted.** It is quite long, you should
finish it at home and hand it back on **Friday 13 December
2024** on moodle or by mail.

That it is noted does not mean that you cannot ask questions, on the
contrary: we want to make sure that you have understood the basic
concepts of the first part of the course. Your submission should come
with a **short report** (around 5 pages, in English or
French) explaining:

- what you managed to implement or not in the project (please be specific about the questions you addressed or not),
- how you progressed in the project and what required most efforts,
- the design choices you did when implementing,
- improvements that could have been performed if you had more time.

If you are progressing quickly, you might need concepts that we have not yet seen in the course. In this case, remember that you can have a look at the exhaustive course notes or ask me questions.

The goal here is to implement a prover for propositional logic which
allows to check proofs and easily elaborate those. Your file is supposed
to be named `prover.ml`

.

Although that this is not required, I strongly suggest that you use GitHub in order to track your files and modifications on those, and have automated tests (if you don’t feel comfortable with git, simply skip those steps). If you choose to do so, begin by following those steps:

Go on this webpage and click on the

*Fork*button (upper right of the page), in order to copy the repository containing initial files for the project on you account, and then*Create fork*.Click on the

*Code*button which will provide you with the name of you repository (this should be something like`git@github.com:username/proof-assistant-project.git`

).Download the files on your computer by cloning the repository

`git clone git@github.com:username/proof-assistant-project.git`

(the url should be the one you obtained above)

When working on your files, you can

save the modifications you made by typing

`git commit . -m "Implemented the proof assistant."`

and then upload them on the server with

`git push`

track a new file

`my-new-file`

that you created`git add my-new-file`

Feel free to ask if you need assistance.

We begin by implementing a type checker for the simply
typed λ-calculus. We respectively define the type of *type
variables* and *term variables* by

```
(** Type variables. *)
type tvar = string
(** Term variables. *)
type var = string
```

A *simple type* is either a type variable or an implication
between simple types. Define a type `ty`

for simple types.

Define a type `tm`

for λ-terms à
la Church (the variables in abstractions are typed).

Define a function `string_of_ty`

of type `ty -> string`

which gives a string representation of a type. For instance, the
representation of the type

\[ (A\to B)\to A\to C \]

should be

`((A => B) => (A => C))`

Define a function `string_of_tm`

of type `tm -> string`

which gives a string representation of a term. For instance, the
representation of the term

\[ λ(f:A\to B).λ(x:A).fx \]

should be

`(fun (f : (A => B)) -> (fun (x : A) -> (f x)))`

(the keyword `fun`

is used here in place of λ). If you
want, you can copy the following UTF-8 symbols in your strings, but you
will have to adapt the parser below:

λ | ∧ | ⊤ | ⇒ | π | ₁ |

Π | ∨ | ⊥ | ¬ | ι | ₂ |

We define a type for typing contexts by

`type context = (var * ty) list`

and an exception

`exception Type_error`

Define a function `infer_type`

of
type `context -> tm -> ty`

which infers the type of a term \(t\)
in a given context \(\Gamma\): it
returns a type \(A\) such that \(\Gamma\vdash t:A\) is derivable using the
usual rules of simply-typed λ-calculus. If no such type exists, it
should raise `Type_error`

. Test it
by ensuring that

\[ λ(f:A\to B).λ(g:B\to C).λ(x:A).g(f x) \]

has type

\[ (A\to B)\to(B\to C)\to A\to C \]

Also ensure that the following raise `Type_error`

(and not some other
exception):

- \(λ(f:A).x\)
- \(λ(f:A).λ(x:B).fx\)
- \(λ(f:A\to B).λ(x:B).fx\)

We recall that the typing rules are

In the case of the axiom rule, it can be useful to use the `List.assoc`

function.

Define a function `check_type`

of
type `context -> tm -> ty -> unit`

which checks whether a term has a given type and raises `Type_error`

if this is not the case. Test
that

- \(λ(x:A).x\) has type \(A\to A\),
- \(λ(x:A).x\) does not have type \(B\to B\),
- \(x\) does not have type \(A\).

Make the definitions of `infer_type`

and `check_type`

mutually recursive (see there for the syntax) and simplify your
inference function by using checking in it.

Our aim is now to progressively add support for other logical connectives (this is the goal of the questions below). We recall that the full set of rules is

When adding constructors keep in mind that

we need to be able to perform type inference: we might need to add some typing information to some type constructors,

the less typing information we have to write, the better,

it can be a good idea to slightly change the rules in order to use functions instead of having to recall free variables, for instance, the elimination rule for disjunction could be implemented as

Add a constructor for conjunction of types and the corresponding
constructors for terms (depending on your formalization some of the term
constructor might need to take types as arguments, but please try to
avoid that). In order to test it, write a term `and_comm`

witnessing the commutativity of
conjunction:

`print_endline (string_of_ty (infer_type [] and_comm))`

should print

`((A /\ B) => (B /\ A))`

Add type and term constructors for truth and show \((\top\Rightarrow A)\Rightarrow A\).

Add type and term constructors for disjunctions. Show that disjunction is commutative.

Add type and term constructors for falsity. Show that

\[ (A\land(A\Rightarrow\bot))\Rightarrow B \]

We do not explicitly add the negation in our language since it can be coded as \(\lnot A=A\Rightarrow\bot\).

Instead of writing terms in OCaml it can be useful to generate terms
from strings. In order to do so, we need to use a lexer (in order to
split the string in tokens) and a parser (in order to construct terms
from sequences of tokens), which will complicate things a bit since we
now have multiple files which need to be compiled together. Note: in
OCaml the lexer and parser generators are respectively ocamllex and
ocamlyacc. Fortunately, the dune
program will do this for us if we provide it with the right files.
*Feel free to ask
for help if you get into trouble here!*

Perform the following steps, in the same folder where you have your
`prover.ml`

file.

Download the

`dune-project`

file: this indicates that we are going to use dune.Download the

`dune`

file: this indicates to dune what we need to compile.Download the

`lexer.mll`

file: this is the lexer.Download the

`parser.mly`

file: this is the parser.Move your definitions of

`ty`

and`tm`

from`prover.ml`

to a new file named`expr.ml`

.Define the following functions at the beginning of

`prover.ml`

:`open Expr let ty_of_string s = Parser.ty Lexer.token (Lexing.from_string s) let tm_of_string s = Parser.tm Lexer.token (Lexing.from_string s)`

This import the definitions from

`expr.ml`

and defines the functions`ty_of_string`

and`tm_of_string`

, of respective types`string -> ty`

and`string -> tm`

, which respectively construct a type and a term from a string (calling the lexer and the parser in order to do so).

Now, you cannot use the interactive mode anymore. In order to run your program, you should type

`dune exec ./prover.exe`

If you get compilation errors in `parser.mly`

, you need to
adapt this file by putting the actual names of your constructors for
terms and types in the expressions between curly brackets.

The following code should be used in order to test the parsing of types:

```
let () =
let l = [
"A => B";
"A /\\ B";
"T";
"A \\/ B";
"_";
"not A"
]in
List.iter (fun s -> Printf.printf "the parsing of %S is %s\n%!" s (string_of_ty (ty_of_string s))) l
```

and of terms

```
let () =
let l = [
"t u v";
"fun (x : A) -> t";
"(t , u)";
"fst(t)";
"snd(t)";
"()";
"case t of x -> u | y -> v";
"left(t,B)";
"right(A,t)";
"absurd(t,A)"
]in
List.iter (fun s -> Printf.printf "the parsing of %S is %s\n%!" s (string_of_tm (tm_of_string s))) l
```

and should indicate you the syntax chosen here. It might be a good
idea to adapt your functions `string_of_ty`

and
`string_of_tm`

so that the two syntaxes match.

As you can imagine, directly writing a full λ-term in order to prove a formula is cumbersome and we now investigate a nice interface in order to incrementally elaborate proofs.

Write a function `string_of_ctx`

of type `context -> string`

which gives the string representation of a context, such as

`x : A => B , y : A /\ B , Z : T`

The functions `List.map`

and
`String.concat`

can be useful in order to do so.

Define a type for sequents (here, of the form \(\Gamma\vdash A\)):

`type sequent = context * ty`

Write a function `string_of_seq`

of type `sequent -> string`

which returns something like

`x : A => B , y : A |- B`

Now, copy the code provided in the file `proving.ml`

at the end of
`prover.ml`

. It defines a function `prove`

of type `context -> ty -> tm`

which, given a
context \(\Gamma\) and a type \(A\) returns a term \(t\) such that \(\Gamma\vdash t:A\) is derivable. Of course,
this function will not guess the proof by itself but will ask the user
to enter some special commands, called *tactics*, in order to do
so. This is for instance the way the Coq
prover works. The code below the function first asks the user for a
formula to prove:

`Please enter the formula to prove:`

If you enter a formula such as

`A => B => A`

It then prints

`Let's prove it.`

to indicate that we have started the proof, then it shows the sequent
we are currently proving, called the current *goal*:

` |- (A => (B => A))`

(we are proving the above formula in the empty context) and then it displays

`? `

to indicate that he is waiting for a tactic from the user. One of the
two tactics currently implemented is `intro`

. It takes an
argument \(x\), which is a variable
name and, when the goal is an implication, performs an introduction
rule

using \(x\) as the name of the new variable in the premise, and then it goes on proving the premise of the introduction rule. Our proof could thus start as follows:

```
Please enter the formula to prove:
A => B => A
Let's prove it.
|- (A => (B => A))
? intro x
x : A |- (B => A)
? intro y
x : A , y : B |- A
?
```

Now, in order to finish our proof, we should use an axiom rule. This
is implemented by the tactic `exact x`

which indicate that
the current goal is exactly the hypothesis `x`

in the
context:

```
x : A , y : B |- A
? exact x
done.
```

Finally, the program prints the corresponding proof term and ensures that its type is the formula we wanted to prove:

```
Proof term is
(fun (x : A) -> (fun (y : B) -> x))
Typechecking... ok.
```

This last step is important: our tactics can perform complicated tasks, and might thus be buggy, but this is not a problem since we trust our typechecker to detect this.

We have tactics for the axiom rule (`exact`

) and for the
introduction rule for arrows (`intro`

). In order, to be able
to perform full proofs with arrows, we still need to implement the
elimination rule for arrows:

Implement a tactic `elim`

taking as argument a variable
\(x\) whose type in the context is of
the form \(A\to B\) and implements the
above rule with \(t=x\): the user will
be left with proving the premise on the right (i.e. we have to prove
\(A\)). For instance,

```
f : (A => B) , x : A |- B
? elim f
f : (A => B) , x : A |- A
```

Prove the formula

`(A => B) => A => B`

In order not to have to type the proofs form the beginning each time,
you can save your proofs in files which contain the list of commands you
entered (including the initial formula). For instance, the proof of
`A => B => A`

is stored in the file k.proof.

In order to test such a file, you can feed your program with it as follows:

`cat k.proof | dune exec ./prover.exe`

This is the files you are asked to write when asked to prove
formulas. We chose to give them the `.proof`

extension. Write
the proof files for the following formulas:

`app.proof`

:`(A => B) => A => B`

`comp.proof`

:`(A => B) => (B => C) => A => C`

`appid.proof`

:`((A => A) => B) => B`

*Remark.* In case you cannot run
the program in a terminal, you can directly modify the code in order to
input the commands from a file. Namely, in OCaml you can open a file by
writing

`let infile = open_in "name_of_your_file.proof" in ...`

you can then read from the file instead of the standard input by changing the line

`let a = input_line stdin in`

to

`let a = input_line infile in`

*Optional.* It might be a good idea to store all the commands
you type in the interactive mode in a file (so that you do not have to
copy them by hand after elaborating your proof). You can open a file
with the `open_out`

function of type `string -> out_channel`

(the argument is the file name) and write to it with the `output_string`

function of type
`out_channel -> string -> unit`

.

Try to prove

`(A => B => C) => (A => B) => A => C`

can you manage to do it? No. The reason is that we have restricted elimination rule of arrow

to the case where \(t\) is a
variable. We now introduce another tactic `cut`

which takes
the formula \(A\) as argument and
implements the above rule: it will successively ask the user to prove
both premises of the rule. For instance, we could start trying proving
`A => A`

by first proving a lemma `B`

:

```
|- (A => A)
? cut B
|- (B => (A => A))
? intro y
y : B |- (A => A)
? intro x
y : B , x : A |- A
? exact x
|- B
```

Once this is implemented, prove (in `s.proof`

)

`(A => B => C) => (A => B) => A => C`

Extend the `intro`

tactic so that it implements the
introduction rule for conjunctions when the goal is a conjunction:

```
|- (A /\ B)
? intro
|- A
? ...
|- B
? ...
```

Prove

`diag.proof`

:`A => A /\ A`

`curry1.proof`

:`(A /\ B => C) => A => B => C`

Add a `fst`

and `snd`

tactic, which take as
argument a variable whose type is a conjunction, and use the left (resp.
right) elimination rule on it in order to prove the current goal. For
instance, a full proof of

`A /\ B => A`

is

```
Please enter the formula to prove:
A /\ B => A
Let's prove it.
|- ((A /\ B) => A)
? intro x
x : (A /\ B) |- A
? fst x
done.
```

Prove

`andcomm.proof`

:`A /\ B => B /\ A`

`curry2.proof`

:`(A => B => C) => A /\ B => C`

Extend the `intro`

tactic so that it implements the
introduction rule for truth.

Prove

`tintro.proof`

:`A => T`

`tstr.proof`

:`(T => A) => A`

Add `left`

and `right`

tactics, which
respectively perform the left and right introduction rules for
disjunction. We should have

```
|- (A \/ B)
? left
|- A
? ...
```

and

```
|- (A \/ B)
? right
|- B
? ...
```

Prove

`injl.proof`

:`A => A \/ B`

`injr.proof`

:`B => A \/ B`

Extend the `elim`

tactic in order to implement the
elimination rule for disjunction on a variable:

```
x : (A \/ B) |- C
? elim x
x : (A \/ B) , x : A |- C
? ...
x : (A \/ B) , x : B |- C
? ...
```

Prove

`orcomm.proof`

:`A \/ B => B \/ A`

`orelim.proof`

:`(A \/ B) => (A => C) => (B => C) => C`

`dist.proof`

:`(A /\ (B \/ C)) => (A /\ B) \/ (A /\ C)`

Extend the `elim`

tactic so that it implement the
elimination rule on a variable of type \(\bot\) (which is noted `_`

here):

```
x : _ |- A
? elim x
done.
```

We recall that `not A`

is a shortcut for
`A => _`

. Prove

`felim.proof`

:`_ => A`

`ntf.proof`

:`not T => _`

`nni.proof`

:`A => not (not A)`

`contr.proof`

:`(A => B) => (not B => not A)`

`nnef.proof`

:`not (not _) => _`

`nnem.proof`

:`not (not (A \/ not A))`

`impdm.proof`

:`((not A) \/ B) => A => B`

`russel.proof`

:`(A => not A) => (not A => A) => _`

Add a type `Nat`

for (unary) natural numbers with three
constructors (zero, the successor of a natural number, and the
recursor). In order to add support for this type you should

add a constructor

`Nat`

to the type`ty`

in`expr.ml`

,add a line

`"Nat" { NAT } |`

in

`lexer.mll`

which states that when we read the string`Nat`

, we should produce a token`NAT`

,add a line

`%token NAT`

at the beginning of

`parser.mly`

in order to declare the token`NAT`

,add a rule

`| NAT { Nat }`

to

`ty:`

in`parser.mly`

in order to state that when we read the token`NAT`

we should produce the term`Nat`

(which is an element of type`ty`

).

Similar operations should be performed to add zero, the successor and the recursor.

Add two introduction rules corresponding to zero and successor.

Add an elimination rule which implements the recurrence principle on
natural numbers (by extending the `elim`

tactic).

Define

`pred.proof`

: the*predecessor*function (by convention the predecessor of zero is zero),`add.proof`

: the*addition*function.

If the above is done and working you can implement some of the extensions below. The reason why they are optional at this point is that you will anyway have to implement similar functions in next part for dependent types.

Define a reduction procedure for the calculus and show the normal forms of proofs. Check that the addition of 6 and 5 gives 11.

Add support for giving a name to a proof once it is over, and use those definitions in further proofs.

For instance, declare that addition is called `add`

and
use it to define multiplication. Also define exponentiation.

Define other inductive types such as options, lists, etc. and prove interesting properties about those.

Add support for general inductive types.

In this part, we are going to implement dependent types. While this
is not considerably much harder than what we have done above, there are
many subtle details, making it difficult to get the implementation
right. Since, in dependent types, the terms and types are both merged
into *expressions*, it is better to start a new prover from
scratch. You should work in a new folder, in a file
`prover.ml`

. You can work in interactive mode at first.

Define a type for variables

`type var = string`

and a type for expressions

```
type expr =
| Typeof var
| Var of expr * expr
| App of var * expr * expr
| Abs of var * expr * expr
| Pi (* forget about the constructors below at first *)
| Nat
| Zof expr
| S of expr * expr * expr * expr
| Ind of expr * expr
| Eq of expr
| Refl of expr * expr * expr * expr * expr | J
```

where

`Type`

is the type of all types (this is written`Set`

in agda)`Var`

is a variable`App`

is an application`Abs`

is a λ-abstraction (the first expression is the type of the variable, and the second the body of the abstraction)`Pi`

is a dependent product (with the same conventions as for abstractions):`Pi(x, a, b)`

is the type of functions which take an argument of type`a`

and return a result of type`b`

*where*(i.e. have`b`

might depend on`x`

`x`

as free variable).

The other constructors below are for natural numbers and equality types, which will be implemented in a second time, and can be ignored for now (you can suppose that they will never occur).

Define a function `to_string`

of
type `expr -> string`

which provides the string representation of an expression. Again, you
can simply return `assert false`

for now for the last seven constructors.

Define a function `fresh_var`

of
type `unit -> var`

which returns a fresh variable name at each call. For instance it might
successively return `"x1"`

, then `"x2"`

, then
`"x3"`

, and so on. You can suppose that those are never
already used in the terms you encounter.

Define a function `subst`

of type
`var -> expr -> expr -> expr`

such that `subst x t u`

is the term
obtained by replacing the variable `x`

by `t`

in
`u`

. This substitution should be *capture-avoiding*:
an easy (but not particularly efficient) way to achieve this is to
systematically replace the variables bound by an abstraction or a
dependent product by a fresh variable name.

Define the type of contexts:

`type context = (var * (expr * expr option)) list`

A context associates, to each variable, a type (the first
`expr`

) and optionally a value: this value will be used when
we make definitions, to store the value of variables.

Define a function `string_of_context`

of type `context -> string`

.
The result should consist in one line for each element of the context of
the form

`x : A`

if the variable `x`

has type `A`

and no value
or

`x : A = t`

if the variable `x`

has type `A`

and value
`t`

.

Define a function `normalize`

of
type `context -> expr -> expr`

which computes the normal form of an expression. Note that a variable
which has a value in the environment should be replaced by (the normal
form of) its value, which is why we need the context argument. Also note
that the types are now dependent: this means that, in an abstraction or
a dependent product, the type of the variable should also be normalized.
You can assume that this function will only be called on expressions
which are well-typed.

Define a function `alpha`

of type
`expr -> expr -> bool`

which tests whether two terms are α-convertible. Note that you can use
substitution to change the name of a variable in the case of an
abstraction or a dependent product.

Using the two previous functions, define a function `conv`

of type `context -> expr -> expr -> bool`

which determines whether two terms are αβ-convertible.

An important remark: **this is the function you should always
use in order to compare expressions**. In particular, you should
never compare two types using equality `=`

or inequality
`<>`

, otherwise α-conversion and β-conversion will not
be correctly handled.

First, define an exception

`exception Type_error of string`

which will be raised when the type inference fails (the argument is a string which you can use to describe the error which happened).

Define a function `infer`

of type
`context -> expr -> expr`

which infers the type of an expression in a given context (or raises
`Type_error`

if there is no such type). Note that the type of
an abstraction (`Abs`

) is a Π-type (`Pi`

), whereas
the type of a Π-type should be `Type`

. You can assume that
`Type`

is of type `Type`

itself.

Use it to define a function `check`

of type `context -> expr -> expr -> unit`

which raises `Type_error`

if, in a
given context, a given term does not have a given type.

In order to add an interaction loop, we will need to perform as before.

Download the file

`dune-project`

.Download the file

`dune`

.Download the file

`lexer.mll`

.Download the file

`parser.mly`

.Move the declarations of the types

`var`

and`expr`

from`prover.ml`

to a new file named`expr.ml`

.Add the following at the beginning of

`prover.ml`

:`open Expr let of_string s = Parser.expr Lexer.token (Lexing.from_string s)`

As before, you should now be able to run your program with

`dune exec ./prover.exe`

Copy all the code contained in this
file at the end of `prover.ml`

: it provides an
interaction loop. The syntax for terms is illustrated below, we only
mention that functions are of the form

`fun (x : A) -> t`

and dependent products

`Pi (x : A) -> B`

The notation `A => B`

is the arrow type implemented as
a dependent product as usual.

The commands available are

`assume`

: suppose given a variable of a given type,`define`

: define an expression,`context`

: print the current context,`type`

: print the type of an expression,`check`

: check that an expression has a given type,`eval`

: compute the normal form of an expression,`exit`

: quit the program.

For your convenience, all the commands you type are stored in a file
`interactive.proof`

. An example session is

```
? assume Bool : Type
Bool assumed of type Type
? assume true : Bool
true assumed of type Bool
? assume false : Bool
false assumed of type Bool
? context
Bool : Type
true : Bool
false : Bool
? define idBool = fun (b : Bool) -> b
idBool defined to (fun (b : Bool) -> b) of type ((b : Bool) -> Bool)
? type idBool true
(idBool true) is of type Bool
? check idBool false = Bool
Ok.
? eval idBool true
true
? define id = fun (A : Type) -> fun (x : A) -> x
id defined to (fun (A : Type) -> (fun (x : A) -> x)) of type ((A : Type) -> ((x : A) -> A))
? check id = Pi (A : Type) -> Pi (x : A) -> A
Ok.
? type id (Bool => Bool) (id Bool)
((id ((_ : Bool) -> Bool)) (id Bool)) is of type ((x4 : Bool) -> Bool)
? exit
Bye.
```

The list of those commands can be found in the file `bool.proof`

and, as before, it
can be run with

`cat bool.proof | dune exec ./prover.exe`

Run those commands and ensure that you have the same results as above.

Extend your functions in order to handle natural numbers:

`Nat`

is the type of natural numbers,`Z`

is zero,`S t`

is the successor of`t`

,`Ind`

is the*induction principle*which takes 4 arguments:- a predicate
`p`

of type`Nat => Type`

, - a term
`z`

of type`p Z`

, the base case, - a term
`s`

of type`Pi (n : Nat) -> p n => p (S n)`

, the inductive case, - a term
`n`

of type`Nat`

and returns a

`p n`

.- a predicate

We also recall the two reduction rules for `Ind`

:

`Ind p z s Z`

\(\rightsquigarrow\)`z`

,`Ind p z s (S n)`

\(\rightsquigarrow\)`s n (Ind p z s n)`

.

In a file `dnat.proof`

, define the *predecessor*
function `pred`

and ensure that it works as expected (by
convention the predecessor of zero is zero):

```
? eval pred Z
Z
? eval pred (S (S (S Z)))
(S (S Z))
```

Define the *addition* function `add`

and ensure
that it works as expected:

```
? eval add (S (S (S Z))) (S (S Z))
(S (S (S (S (S Z)))))
```

Extend your functions in order to handle equality:

`t = u`

is the type of proofs of equality between`t`

and`u`

(both supposed to be of the same type),`Refl t`

is a proof that`t`

is equal to itself,`J`

is the*eliminator*for equality which takes five arguments- a predicate
`p`

of type`Pi (x : A) -> Pi (y : A) -> x = y => Type`

, - a proof
`r`

of`p`

in the case of reflexivity, i.e.`r`

is of type`Pi (x : A) -> p x x (Refl x)`

, - an element
`x`

of type`A`

, - an element
`y`

of type`A`

, - a proof
`e`

of equality between`x`

and`y`

, i.e. of type`x = y`

,

and returns a

`p x y e`

.- a predicate

The reduction rule for `J`

is

`J p r x x (Refl x)`

\(\rightsquigarrow\)`r x`

In the file `dnat.proof`

:

Show that successor is compatible with equality, i.e., if two natural numbers

`m`

and`n`

are equal then their successors are also equal: you should define a term`Seq`

such that`? check Seq = Pi (x : Nat) -> Pi (y : Nat) -> Pi (e : x = y) -> S x = S y Ok.`

Show that zero is a neutral element for addition: you should define terms

`zadd`

and`addz`

such that`? check zadd = Pi (n : Nat) -> add Z n = n Ok. ? check addz = Pi (n : Nat) -> add n Z = n Ok.`

(one should be much easier to define than the other).

Show that addition is associative and commutative.

Define multiplication and show similar properties.

Add support for

- falsity,
- truth,
- coproducts, and
- inductive types (using W-types, which subsume all the above cases).

For each of those, prove a few properties (e.g. from TD5) showing that your implementation works. For the last one, you can for instance define the type of binary trees, as well as the function which computes the height of a binary tree.

Implement an interactive prover with tactics (`intro`

,
`elim`

, etc.) as you did in the first part.

Prove that the system is inconsistent because we assumed
`Type`

to be of type `Type`

(if you have
implemented inductive types, this can be done by encoding Russell’s
paradox as in the course, if you have not this is much more involved and
can be done following Girard’s paradox, which is described in the course
notes).

Correct this by adding a hierarchy of universes.

There are two standard ways of handling α-conversion, implement one of those, or both (make a backup of your current implementation first!):

- use de Bruijn indices in order to represent variable names,
- use normalization by evaluation in order to reuse OCaml’s binders when normalizing terms.