Implementing a propositional prover

Samuel Mimram

This TD will be noted. It is quite long, you should finish it at home and hand it back on 15 December 2023 on moodle (or by mail if you do not have access to moodle).

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:

  1. what you managed to implement or not in the project (please be specific about the questions you addressed or not),
  2. how you progressed in the project and what required most efforts,
  3. the design choices you did when implementing,
  4. 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.

1 Type inference for a simply typed calculus

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

1.1 Simple types

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

1.2 λ-terms

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

1.3 String representation

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:

λ ∧ ⊤ ⇒ π ₁
Π ∨ ⊥ ¬ ι ₂

1.4 Type inference

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

We recall that the typing rules are

Typing rules

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

1.5 Type checking

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

1.6 Type inference and checking together

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.

1.7 Other connectives

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

Typing rules

When adding constructors keep in mind that

1.8 Conjunction

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

1.9 Truth

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

1.10 Disjunction

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

1.11 Falsity

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

1.12 Parsing strings

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.

2 Interactive prover

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.

2.1 String representation of contexts

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.

2.2 Sequents

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

2.3 An interactive prover

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

Introduction of arrows

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.

2.4 Elimination of arrows

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:

Arrow elimination

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

2.5 Proofs in files

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:

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.

2.6 Full arrow elimination

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

Arrow elimination

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

2.7 Conjunctions

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

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

2.8 Truth

Extend the intro tactic so that it implements the introduction rule for truth.

Prove

2.9 Disjunction

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

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

2.10 Falsity

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

3 Natural numbers

3.1 A type for natural numbers

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.

3.2 Introduction rules

Add two introduction rules corresponding to zero and successor.

3.3 Elimination rule

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

Define

4 Optional: small extensions

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.

4.1 Reduction

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

4.2 Declarations

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.

4.3 Other inductive types

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

Add support for general inductive types.

5 Dependent 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.

5.1 Expressions

Define a type for variables

type var = string

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

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

5.2 String representation

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.

5.3 Fresh variable names

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.

5.4 Substitution

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.

5.5 Contexts

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.

5.6 Normalization

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.

5.7 α-conversion

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.

5.8 Conversion

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.

5.9 Type inference

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.

5.10 Type checking

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.

5.11 Interaction loop

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

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.

5.12 Natural numbers

Extend your functions in order to handle natural numbers:

We also recall the two reduction rules for Ind:

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

5.13 Equality

Extend your functions in order to handle equality:

The reduction rule for J is

5.14 Using the prover

In the file dnat.proof:

5.15 Optional: inductive types

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.

5.16 Optional: interactive prover

Implement an interactive prover with tactics (intro, elim, etc.) as you did in the first part.

5.17 Optional: universes

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.

5.18 Optional: better handling of indices

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