**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.

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

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 in place of λ).

We define a type for typing contexts by

and an exception

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 `tm -> ty -> bool`

which checks whether a term has a given type. 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:

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). 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\)):

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`

*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

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

and a type for expressions

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

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:

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

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)`

.

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`

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).

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`

.

Correct this by adding a hierarchy of universes.

Modify your implementation in order to use de Bruijn indices instead of variable names (make a backup of your current implementation first!).