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:
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 pushtrack a new file my-new-file that you created
git add my-new-fileFeel 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 = stringA 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) listand an exception
exception Type_errorDefine 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):
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
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.exeIf 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))) land 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))) land 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 : TThe 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 * tyWrite a function string_of_seq
of type sequent -> string
which returns something like
x : A => B , y : A |- BNow, 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 => AIt 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 |- AProve the formula
(A => B) => A => BIn 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.exeThis 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 => Bcomp.proof:
(A => B) => (B => C) => A => Cappid.proof:
((A => A) => B) => BRemark. 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 into
let a = input_line infile inOptional. 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 => Ccan 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
|- BOnce this is implemented, prove (in s.proof)
(A => B => C) => (A => B) => A => CExtend 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 /\ Acurry1.proof:
(A /\ B => C) => A => B => CAdd 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 => Ais
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 /\ Acurry2.proof:
(A => B => C) => A /\ B => CExtend the intro tactic so that it implements the
introduction rule for truth.
Prove
tintro.proof: A => Ttstr.proof: (T => A) => AAdd 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 \/ Binjr.proof: B => A \/ BExtend 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 \/ Aorelim.proof:
(A \/ B) => (A => C) => (B => C) => Cdist.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: _ => Antf.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 => Brussel.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 NATat 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 = stringand 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 * exprwhere
Type is the type of all types (this is written
Set in agda)Var is a variableApp is an applicationAbs 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 b might depend on
x (i.e. have 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)) listA 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 : Aif the variable x has type A and no value
or
x : A = tif 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 stringwhich 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.exeCopy 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) -> tand dependent products
Pi (x : A) -> BThe 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.exeRun 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:
p of type Nat => Type,z of type p Z, the base case,s of type
Pi (n : Nat) -> p n => p (S n), the inductive
case,n of type Natand returns a p n.
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
p of type
Pi (x : A) -> Pi (y : A) -> x = y => Type,r of p in the case of reflexivity,
i.e. r is of type
Pi (x : A) -> p x x (Refl x),x of type A,y of type A,e of equality between x and
y, i.e. of type x = y,and returns a p x y e.
The reduction rule for J is
J p r x x (Refl x) \(\rightsquigarrow\) r xIn 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
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!):