Proof terms and meta-theory

Authors:

Yannick Forster

Théo Winterhalter

Files:

Display all goals and responses

For this class we will look a bit more at the theory behind Agda, Lean and Rocq: dependent type theory. We will see how this underlying theory comes into play when proving theorems and defining functions. Knowing this isn't strictly necessary to use Lean or Rocq (for Agda this is a different story), but it will certainly help, for instance to understand error messages a bit more. And sometimes it makes proving easier. It's also relevant if you want to work in the area of proof assistants later.

From Stdlib Require Import List.
Import ListNotations.

Dependent functions and type universes

So what makes depentent type theory dependent? In simple type theory, variants of which are used in OCaml for instance, types can depend on other types, as exemplified by list A (using Rocq syntax). Dependent types can additionally depend on terms. This allows types to include computation or even be computations themselves.

See for instance the if in the type of the function below.

Definition dependent (b : bool) : if b then nat else bool :=
  match b with true => 0 | false => true end.

We already used such if statements when showcasing Σ types in the previous lecture so it shouldn't be too surprising.

The thing which allows us to include computation in types is that terms and types are not actually separated. In particular, types have a type, often Type, and Type itself has a type! This bring us to the notion of universe.

Essentially Type and Prop are universes. They contain respectively the types and propositions (as the names suggest).

Exercise: N-ary functions

Define a n-ary summation function sum, such that e.g. sum 3 = fun a b c => a + b + c.

Fixpoint nary (n : nat) :=
  match n with
  | 0 => nat
  | S n => nat -> nary n
  end.

Fixpoint sum' (n : nat) (a : nat) : nary n :=
  REPLACE_ME.Not a truly recursive fixpoint. [non-recursive,fixpoints,default]

Definition sum n : nary n :=
  REPLACE_ME.

Lemma sum_2 : sum 2 = fun x1 x2 => x1 + x2.sum 2 = (fun x1 x2 : nat => x1 + x2)
Proof.sum 2 = (fun x1 x2 : nat => x1 + x2)
Admitted.

Lemma sum_3 : sum 3 = fun x1 x2 x3 => x1 + x2 + x3.sum 3 = (fun x1 x2 x3 : nat => x1 + x2 + x3)
Proof.sum 3 = (fun x1 x2 x3 : nat => x1 + x2 + x3)
Admitted.

Check Type.Type
     : Type

Above you see that Type itself has type Type. It makes sense, after all Type is indeed a Type. However, assuming Type : Type actually leads to inconistencies (proofs of False) so instead, we have a hierarchy of universes: basically Type₀ : Type₁ : Type₂ …

You can ask Rocq to show you universe levels by using the following command.

Set Printing Universes.
Check Type.Type@{lesson3_part1.29}
     : Type@{lesson3_part1.29+1}
(* {lesson3_part1.29} |=  *)
Unset Printing Universes.

This is not very easy to read but essentially it says that Typeᵢ lives in Typeᵢ₊₁.

The fact that the universe levels are not displayed and inferred by the system is sometimes called typical ambiguity.

Even while hidden they still play an important role. If for instance we alias Type under some name T, we will run into an issue with the following definition because it will pick a specific universe level (the index i in Typeᵢ).

Definition T := Type.
Fail Check (forall (X : T), X) : T.The command has indeed failed with message:
The term "forall X : T, X" has type "Type" while it is expected to have type
 "T"
(universe inconsistency: Cannot enforce T.u0 < T.u0 because T.u0 = T.u0).

Here you get what is called a "universe inconsistency" because you cannot quantify over a universe and stay within it essentially.

Compare however with the following, seemingly equivalent, presentation.

Check (forall (X : Type), X) : Type.(forall X : Type, X) : Type
     : Type

This time it works because the Type on the right has a higher level that the one on the left so that it is able to contain it. You don't need to worry too much about universes at this point but know that they exist to forbid inconsistencies and that sometimes you will get universes inconsistencies that will require to look more closely at the definitions.

We will also have examples about this later, so stay tuned. 😎

Back to Prop now.

Check Prop.Prop
     : Type

Prop is of type Type and actually Prop doens't have any hidden universe levels. It however has one interesting property which is that to create a proposition you can quantify over anything. This includes Prop itself. This propery is called impredicativity and is not present in Agda for instance.

Check (forall (P : Prop), P) : Prop.(forall P : Prop, P) : Prop
     : Prop

Proof terms

Let us consider again the even predicate from the previous lesson.

Inductive even : nat -> Prop :=
| evenO : even 0
| evenS : forall n, even n -> even (S (S n)).

As we showed you, constructor is actually applying the correct constructor between evenO and evenS. So when proving even 4 we can actually be explicit like below:

Lemma even_four : even 4.even 4
Proof.even 4
  apply evenS.even 2 apply evenS.even 0 apply evenO.
Qed.

Now let us use Print to see what the proof is to Rocq.

Print even_four.even_four = evenS 2 (evenS 0 evenO)
     : even 4

You see two uses of evenS followed by evenO. We also see that the numbers 2 and 0 are there because they appear as arguments to evenS but they're not really necessary so we can mark them as implicit so they don't bother us.

Arguments evenS {n}.

Now the proof of even 4 we write directly as follows:

Definition even_four' :=
  evenS (evenS evenO).

Exercise: Even

Define a proof term of the following type:

Fixpoint even_double n : even (n * 2) :=
  REPLACE_ME.Not a truly recursive fixpoint. [non-recursive,fixpoints,default]

Forall, implication

For now you saw what to do with forall and -> interactively, and it was very similar: you use intro or intros to prove them, and apply to use them.

When we prove something using tactics we can ask Rocq to show how it built it with the command Show Proof. Let's see on an example.

Goal forall P Q, P -> (P -> Q) -> Q.forall P Q : Type, P -> (P -> Q) -> Q
Proof.forall P Q : Type, P -> (P -> Q) -> Q
  intros P Q x f.P, Q: Type
x: P
f: P -> Q
Q
  apply f.P, Q: Type
x: P
f: P -> Q
P
  apply x.
  Show Proof.(fun (P Q : Type) (x : P) (f : P -> Q) => f x)
Qed.

We get the proof term corresponding to the proof: it's a definition whose type is exactly the proposition we wanted to prove. We can use it directly to prove our lemma.

Goal forall P Q, P -> (P -> Q) -> Q.forall P Q : Type, P -> (P -> Q) -> Q
Proof.forall P Q : Type, P -> (P -> Q) -> Q
  apply (fun P Q x f => f x).
Qed.

We see that function abstraction (or λ-abstraction, the fun … => part) corresponds to intros, while apply is interpreted as function application (hence the name).

Coming up a with a proof term by hand is hard, and Rocq can also help us write it using the refine tactic which accepts a partial term with some underscores (_) and then you can fill them interactively.

Goal forall P Q, P -> (P -> Q) -> Q.forall P Q : Type, P -> (P -> Q) -> Q
Proof.forall P Q : Type, P -> (P -> Q) -> Q

Basically here we do intros P Q x f.

  refine (fun P Q x f => _).P, Q: Type
x: P
f: P -> Q
Q

Now apply f.

  refine (f _).P, Q: Type
x: P
f: P -> Q
P

Now apply x.

  refine x.
Qed.

Tip

You can also mix Definition and the refine tactic with the refine attribute as follows (it works with other commands such as Fixpoint):

#[refine] Definition mp : forall P Q, P -> (P -> Q) -> Q :=
  fun P Q x f => _.P, Q: Type
x: P
f: P -> Q
Q
Proof.P, Q: Type
x: P
f: P -> Q
Q
  apply f, x.
Qed.

The proof in essence hasn't changed. All it comes down to is the typing rules of the theory. If you know the Curry-Howard correspondance for simple type theory this shouldn't be surprising. Let us recap the idea quickly. Proving A → B is the same as defining a function from A to B. The introduction rule corresponds to λ-abstraction:

\begin{equation*} \begin{array}{c@{\qquad\qquad}c} \fbox{Natural deduction} & \fbox{Simple type theory} \\[1em] \dfrac{\Gamma, A \vdash B}{\Gamma \vdash A \to B} & \dfrac{\Gamma, x: A \vdash t : B}{\Gamma \vdash \lambda (x : A).\ t : A \to B} \end{array} \end{equation*}

If you don't know λ-calculus, then think of λ x. t as a function taking an argument x and returning t where t might mention x.

The elimination rule for implication then corresponds to application:

\begin{equation*} \begin{array}{c@{\qquad\qquad}c} \fbox{Natural deduction} & \fbox{Simple type theory} \\[1em] \dfrac{\Gamma \vdash A \to B \qquad \Gamma \vdash A}{\Gamma \vdash B} & \dfrac{\Gamma \vdash f : A \to B \qquad \Gamma \vdash u : A}{\Gamma \vdash f\ u : B} \end{array} \end{equation*}

We mentioned before that we have dependent types, that lets us write things such as forall (x : A), B, where B may refer to x. This generalises the rules above to quantifiers:

\begin{equation*} \fbox{Dependent type theory} \end{equation*}

\begin{equation*} \frac{\Gamma, x : A \vdash t : B}{\Gamma \vdash \lambda (x : A).\ t : \forall (x : A).\ B} \qquad \frac{\Gamma \vdash f : \forall (x : A). B \qquad \Gamma \vdash u : A}{\Gamma \vdash f\ u : B[x := u]} \end{equation*}

Since x can appear in B, it needs to be replaced by u, which is what the \(B[x := u]\) represents. Let us see how it works in practice:

Goal forall (f : forall n, even n), even 1.(forall n : nat, even n) -> even 1
Proof.(forall n : nat, even n) -> even 1
  refine (fun f => f 1).

f 1 has type even 1, the n was substitued by 1.

Qed.

Let us see again proof terms in action and how it compares to tactics.

Lemma even_plus_four :
  forall (n : nat) (H : even n), even (4 + n).forall n : nat, even n -> even (4 + n)
Proof.forall n : nat, even n -> even (4 + n)
  intros n H.n: nat
H: even n
even (4 + n)
  apply evenS.n: nat
H: even n
even (S (S n))
  apply evenS.n: nat
H: even n
even n
  apply H.
Qed.

Lemma even_plus_four_refine :
  forall (n : nat) (H : even n), even (4 + n).forall n : nat, even n -> even (4 + n)
Proof.forall n : nat, even n -> even (4 + n)
  refine (fun n H => evenS (evenS _)).n: nat
H: even n
even n
  refine H.
Qed.

We can just do it in direct style.

Definition even_plus_four_term :
  forall (n : nat), even n -> even (4 + n)
:= fun n H => evenS (evenS H).

Exercise: Proof terms

Prove the following statements using proof terms. If it's too hard to do directly, you can use the interactive mode together with the refine tactic.

Definition ex1 : forall (P Q : Prop), P -> Q -> P :=
  REPLACE_ME.

Definition ex2 :
  forall (P Q R : Prop), P -> (P -> Q) -> (P -> Q -> R) -> R
:=
  REPLACE_ME.

Exercise: Less than

We give you this type for "less than" (lt).

Inductive lt (n : nat) : nat -> Prop :=
| lt_B : lt n (S n)
| lt_S m : lt n m -> lt n (S m).

Prove the following lemma interactively using intros and apply.

Lemma lt_plus_4 :
  forall n m,
    lt n m ->
    lt n (4 + m).forall n m : nat, lt n m -> lt n (4 + m)
Proof.forall n m : nat, lt n m -> lt n (4 + m)
Admitted.

Now prove it with a proof term.

Definition lt_plus_4' n m : lt n m -> lt n (4 + m) :=
  REPLACE_ME.

And, or, exists

First, we'll have a look at the definitions of various logical connectives and propositions we've used over the course of the lecture.

Module Show_Definitions.

First, False can be seen as the empty type, so we define it as an inductive type with absolutely no constructor. We write this as below, with an odd syntax that really just lists all—meaning 0—the constructors.

  Inductive False := .

True on the other hand is like the unit type: it has exactly one constructor which happens to be called I.

  Inductive True := I.

~ P is a notation for not P which unfolds to P -> False. But this you already knew.

  Definition not (P : Prop) := P -> False.

  Notation "~ P" := (not P).

Conjunction A /\ B is a notation for and A B which is defined in a very similar way to cartesian product A * B, except that A and B, as well as A /\ B are propositions (they live in the Prop universe).

  Inductive and (P Q : Prop) : Prop :=
  | conj : P -> Q -> and P Q.

Disjunction P \/ Q is a notation for or P Q and has two constructors: one saying P is enough to prove P \/ Q and one saying Q is enough.

  Inductive or (P Q : Prop) : Prop :=
  | or_introl : P -> or P Q
  | or_intror : Q -> or P Q.

End Show_Definitions.

You can also use the Print command to see the definitions above. Note how you can use quotation marks around a notation to print it as well, which can be quite handy when you don't know what it represents.

Print False.Inductive False : Prop :=  .
Print True.Inductive True : Prop :=  I : True.
Print "~".Notation "~ x" := (not x)

not = fun A : Prop => A -> False
     : Prop -> Prop

Arguments not A%_type_scope
Print and.Inductive and (A B : Prop) : Prop :=  conj : A -> B -> A /\ B.

Arguments and (A B)%_type_scope
Arguments conj [A B]%_type_scope _ _
Print "/\".Notation "A /\ B" := (and A B)

Inductive and (A B : Prop) : Prop :=  conj : A -> B -> A /\ B.

Arguments and (A B)%_type_scope
Arguments conj [A B]%_type_scope _ _
Print or.Inductive or (A B : Prop) : Prop :=
    or_introl : A -> A \/ B | or_intror : B -> A \/ B.

Arguments or (A B)%_type_scope
Arguments or_introl [A B]%_type_scope _, [_] _ _
Arguments or_intror [A B]%_type_scope _, _ [_] _
Print "\/".Notation "A \/ B" := (or A B)

Inductive or (A B : Prop) : Prop :=
    or_introl : A -> A \/ B | or_intror : B -> A \/ B.

Arguments or (A B)%_type_scope
Arguments or_introl [A B]%_type_scope _, [_] _ _
Arguments or_intror [A B]%_type_scope _, _ [_] _

To eliminate a proof of False, one can just match on it and provide the exactly zero cases that are needed.

Definition elim_False : forall (Z : Prop), False -> Z :=
  fun Z a =>
    match a with end.

The rest should be easier to understand.

Definition elim_and :
  forall (X Y Z : Prop), X /\ Y -> (X -> Y -> Z) -> Z
:= fun X Y Z a e =>
    match a with
    | conj x y => e x y
    end.

Definition elim_or :
  forall (X Y Z : Prop), X \/ Y -> (X -> Z) -> (Y -> Z) -> Z
:= fun X Y Z a e1 e2 =>
    match a with
    | or_introl x => e1 x
    | or_intror y => e2 y
    end.

Exercise: Connectives as proof terms

Prove the following with a proof term. Hint: Use Print "\/" if needed.

Definition or_comm P Q : P \/ Q -> Q \/ P :=
  REPLACE_ME.

Prove the following with a proof term.

Definition ex3 :
  forall X (P Q : X -> Prop),
    (forall x, P x <-> Q x) ->
    (forall x, Q x) ->
    forall x, P x
:=
  REPLACE_ME.

Prove the following with a proof term. If you have trouble with this one, try to use refine to fill the term interactively.

Definition Russel X : ~ (X <-> ~ X)
:=
  REPLACE_ME.

Exercise: Impredicative encodings

Thanks to impredicativity of Prop (the ability to quantify over propositions within propositions) it is possible to define most connectives using only forall and -> (no inductive definitions).

For instance, one can define False as follows:

Definition iFalse := forall (P : Prop), P.

Show that iFalse is equivalent to False.

Lemma iFalse_iff : False <-> iFalse.False <-> iFalse
Proof.False <-> iFalse
Admitted.

Define the impredicative encoding of True and show it equivalent to True.

Definition iTrue : Prop :=
  REPLACE_ME.

Lemma iTrue_iff : True <-> iTrue.True <-> iTrue
Proof.True <-> iTrue
Admitted.

Now do the same thing for conjunction, disjunction and the existential quantifier.

Definition iAnd (P Q : Prop) : Prop :=
  REPLACE_ME.

Lemma iAnd_iff :
  forall P Q,
    P /\ Q <-> iAnd P Q.forall P Q : Prop, P /\ Q <-> iAnd P Q
Proof.forall P Q : Prop, P /\ Q <-> iAnd P Q
Admitted.
Definition iOr (P Q : Prop) : Prop :=
  REPLACE_ME.

Lemma iOr_iff :
  forall P Q,
    P \/ Q <-> iOr P Q.forall P Q : Prop, P \/ Q <-> iOr P Q
Proof.forall P Q : Prop, P \/ Q <-> iOr P Q
Admitted.

Definition iEx (X : Type) (P : X -> Prop) : Prop :=
  REPLACE_ME.

Lemma iEx_iff :
  forall X P,
    (exists (x : X), P x) <-> iEx X P.forall (X : Type) (P : X -> Prop), (exists x : X, P x) <-> iEx X P
Proof.forall (X : Type) (P : X -> Prop), (exists x : X, P x) <-> iEx X P
Admitted.