**This TD will be noted.** It is quite long, you should
finish it at home. 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 (a few pages, in English or
French) explaining:

- what you managed to implement or not in the project,
- 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`

.

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 = (string * 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))`

A 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 the file
`parser.ml`

, we provide you with functions, which you can
copy in your code in order to do so (this is not the
way people would usually do parsing, but it has the advantage of not
requiring external tools or files, if you are used to more standard
techniques feel free to use them). The two functions of interest for you
are `ty_of_string`

and `tm_of_string`

, of respective types `string -> ty`

and `string -> tm`

.
Depending on the names you gave to the constructors you might have to
adapt them a bit (feel free to ask for help).

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";
"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 your program. 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 this
file k.proof.

In order to test a file, open a console and compile your program

`ocamlopt prover.ml -o prover`

and then feed it with the file:

`cat k.proof | ./prover`

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). You can easily add the support for the type `Nat`

int the parser by adding `"Nat"`

to the `lexer`

list (this declares
it as a keyword) and adding a match case

`Genlex.Kwd "Nat" -> Nat | `

to the `base`

function in `ty_of_tk`

.

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. This part can replace the article presentation. Since, in
dependent types, the terms and types are both merged into
*expressions*, it is better to start a new prover from
scratch.

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.

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`

which will be raised when the type inference fails.

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.

Copy all the code contained in this
file at the end of your file. It defines a function `of_string`

of type `string -> expr`

which takes care of parsing an expression, and 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 is can
be run with

`cat bool.proof | ./prover`

if you do not want to type all the commands each time.

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:

`Eq 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) -> Eq 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 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`Eq 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 : Eq x y) -> Eq (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) -> Eq (add Z n) n Ok. ? check addz = Pi (n : Nat) -> Eq (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.