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 dependent 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 brings 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 an 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 inconsistencies (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 than 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 universe inconsistencies that will require you 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 doesn'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 property 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 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 correspondence 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 substituted 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 Russell 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.

Using tactics to build definitions

There is no rule that says that tactics are reserved for proofs. Proving and programming are essentially the same thing in Rocq!

Fixpoint add (n m : nat) {struct n} : nat.add: nat -> nat -> nat
n, m: nat
nat
Proof.add: nat -> nat -> nat
n, m: nat
nat
  destruct n.add: nat -> nat -> nat
m: nat
nat
add: nat -> nat -> nat
n, m: nat
nat
  -add: nat -> nat -> nat
m: nat
nat apply m.
  -add: nat -> nat -> nat
n, m: nat
nat apply S.add: nat -> nat -> nat
n, m: nat
nat apply add.add: nat -> nat -> nat
n, m: nat
nat
add: nat -> nat -> nat
n, m: nat
nat
    +add: nat -> nat -> nat
n, m: nat
nat apply n.
    +add: nat -> nat -> nat
n, m: nat
nat apply m.
Defined.

We can show that the resulting add we just defined is actually exactly the same as the one from the standard library. At least from the point of view of Rocq:

Goal Nat.add = add.Nat.add = add
Proof.Nat.add = add
  reflexivity.
Qed.

Modulo some simplification, we get the same thing as what we would have written by hand.

Eval compute in add.= fix add (n m : nat) {struct n} : nat :=
    match n with
    | 0 => m
    | S n0 => S (add n0 m)
    end
: nat -> nat -> nat

Proofs using terms can be quite short.

Goal forall X (p q : X -> Prop),
  (forall x, p x <-> q x) ->
  (forall x, q x) ->
  forall x, p x.forall (X : Type) (p q : X -> Prop),
(forall x : X, p x <-> q x) -> (forall x : X, q x) -> forall x : X, p x
Proof.forall (X : Type) (p q : X -> Prop),
(forall x : X, p x <-> q x) -> (forall x : X, q x) -> forall x : X, p x
  intros X p q f g x.X: Type
p, q: X -> Prop
f: forall x : X, p x <-> q x
g: forall x : X, q x
x: X
p x
  refine (match f x with conj _ h => _ end).X: Type
p, q: X -> Prop
f: forall x : X, p x <-> q x
g: forall x : X, q x
x: X
q0: p x -> q x
h: q x -> p x
p x
  exact (h (g x)).
  Show Proof.(fun (X : Type) (p q : X -> Prop) (f : forall x : X, p x <-> q x)
   (g : forall x : X, q x) (x : X) =>
 match f x with
 | conj _ h => h (g x)
 end)
Qed.

Exercise: Tactics for programs

There is also a fix tactic to introduce fix in the term. It takes two arguments: fix f n introduces an assumption f in the context, with the same type as the goal, and n indicates which argument (starting from 1) is recursive.

So below fix rec 1 introduces rec : nat -> nat -> nat where the first argument is recursive, a bit like writing rec a b {struct a}.

Definition addition : nat -> nat -> nat.nat -> nat -> nat
Proof.nat -> nat -> nat
  fix rec 1.rec: nat -> nat -> nat
nat -> nat -> nat
  intros n m.rec: nat -> nat -> nat
n, m: nat
nat
  destruct n.rec: nat -> nat -> nat
m: nat
nat
rec: nat -> nat -> nat
n, m: nat
nat
  -rec: nat -> nat -> nat
m: nat
nat apply m.
  -rec: nat -> nat -> nat
n, m: nat
nat apply S.rec: nat -> nat -> nat
n, m: nat
nat apply rec.rec: nat -> nat -> nat
n, m: nat
nat
rec: nat -> nat -> nat
n, m: nat
nat
    +rec: nat -> nat -> nat
n, m: nat
nat apply n.
    +rec: nat -> nat -> nat
n, m: nat
nat apply m.
Defined.

First prove the following.

Goal Nat.add = addition.Nat.add = addition
Proof.Nat.add = addition
Admitted.

Now define an append function on lists (the one we write ++) using the fix tactic.

Definition append {A : Type} : list A -> list A -> list A.A: Type
list A -> list A -> list A
Proof.A: Type
list A -> list A -> list A
Admitted.

Goal List.app = @append.app = @append
Proof.app = @append
Admitted.

Guard condition

If you remember, when we talked about Fixpoint we mentioned {struct n} and how it was necessary to tell Rocq which argument was structurally recursive but we never explicitly said why termination is so important in the first place.

So, let's disable termination checking and find out! It's actually very easy to derive False from this. We use the following command to disable the termination checker.

Unset Guard Checking.

False is now simply proven via a loop!

Fixpoint f (x : unit) : False := f x.

We get back a proof of False by applying the function f.

Goal False.False
Proof.False
  exact (f tt).
Qed.

Let's not forget to turn termination checking back on. Turning it off is in any case not something we recommend you do, but it's nice for certain exercises.

Set Guard Checking.

Exercise: Non-termination (advanced)

There are three crucial potential breaking points of consistency of type theory:

termination of recursive functions, which needs to be ensured;
strict positivity of inductive types, which we see in the lecture right after this exercise;
having type hierarchies rather than a Type : Type rule.

Define a function of type nat -> nat and use it to deduce False. Note that this is surprisingly tricky.

Unset Guard Checking.

Set Guard Checking.

Strict positivity

The termination checker is not the only important part of the system. Another important criterion, called strict positivity, is imposed on inductive type definitions.

It says that a constructor of an inductive type cannot mention said inductive type on the left of an arrow (->). As before, we'll break things by disabling positivity checking. We once again derive False.

Unset Positivity Checking.

Inductive bad :=
| C : (bad -> False) -> bad.

It already looks fishy because C here has type ~ bad -> bad.

Goal False.False
Proof.False

Remember, the tick notation does pattern matching.

  pose (f := fun '(C g) => g (C g)).f:= fun '(C g) => g (C g): bad -> False
False
  exact (f (C f)).
Qed.

Set Positivity Checking.

Ok, so what happened here? We first proved f : ~ bad by deducing False from an element of bad. By case analysis, that element is necessarily of the form C g with g : ~ bad so we just need to construct an element of bad to conclude with g. We do so by providing C g. From f : ~ bad we can once again construct bad and thus deduce a contradiction.

Don't worry if it makes you scratch your head a bit too much. The exercise below might help by presenting it slightly differently.

Exercise: Non-positive types (advanced)

Define an inductive type bad such that bad <-> ~ bad, use lemma Russell from above to derive a contradiction.

Unset Positivity Checking.

Set Positivity Checking.

Recursors

We've been using induction principles for inductive types quite a bit, but in Rocq they are not primitive. They actually unfold to a combination of fix and match.

See below how we define the induction principles for nat and list. You should have the necessary background to understand these definitions now.

Fixpoint nat_ind (P : nat -> Prop) (z : P 0)
  (s : forall (n : nat), P n -> P (S n)) (n : nat) : P n :=
  match n with
  | 0 => z
  | S n => s n (nat_ind P z s n)
  end.

Fixpoint list_ind {X} (P : list X -> Prop) (n : P nil)
  (c : forall (x : X) (l : list X), P l -> P (cons x l)) (l : list X)
: P l :=
  match l with
  | nil => n
  | cons x l => c x l (list_ind P n c l)
  end.

Exercise: More induction principles

Define induction principles using Fixpoint for all the following types of trees.

Inductive btree :=
| bL
| bN (b1 b2 : btree).

Inductive ltree (L : Type) :=
| lL (l : L)
| lN (l : L) (b1 b2 : ltree L).

Inductive atree (L : Type) (B : L -> Type) :=
| aN (l : L) (bs : B l -> atree L B).

Abbreviation altree L :=
  (atree (L * bool) (fun p => if snd p then bool else False)).

Define functions to : forall {L}, ltree L -> altree L and of : forall {L}, altree L -> ltree L such that forall L (t : ltree L), of (to t) = t.

Exercise: Nested induction principles

Inductive rtree :=
| rN (bs : list rtree).rtree is nested using list. No scheme for list is registered as All. It can
be generated using command "Scheme All" e.g. "Scheme All for list.".
[register-all,automation,default]
rtree is nested using list. No scheme for list is registered as All. It can
be generated using command "Scheme All" e.g. "Scheme All for list.".
[register-all,automation,default]
rtree is nested using list. No scheme for list is registered as All. It can
be generated using command "Scheme All" e.g. "Scheme All for list.".
[register-all,automation,default]
rtree is nested using list. No scheme for list is registered as All. It can
be generated using command "Scheme All" e.g. "Scheme All for list.".
[register-all,automation,default]
rtree is nested using list. No scheme for list is registered as All. It can
be generated using command "Scheme All" e.g. "Scheme All for list.".
[register-all,automation,default]
rtree is nested using list. No scheme for list is registered as All. It can
be generated using command "Scheme All" e.g. "Scheme All for list.".
[register-all,automation,default]
rtree is nested using list. No scheme for list is registered as All. It can
be generated using command "Scheme All" e.g. "Scheme All for list.".
[register-all,automation,default]
rtree is nested using list. No scheme for list is registered as All. It can
be generated using command "Scheme All" e.g. "Scheme All for list.".
[register-all,automation,default]
rtree is nested using list. No scheme for list is registered as All. It can
be generated using command "Scheme All" e.g. "Scheme All for list.".
[register-all,automation,default]
rtree is nested using list. No scheme for list is registered as All. It can
be generated using command "Scheme All" e.g. "Scheme All for list.".
[register-all,automation,default]
rtree is nested using list. No scheme for list is registered as All. It can
be generated using command "Scheme All" e.g. "Scheme All for list.".
[register-all,automation,default]
rtree is nested using list. No scheme for list is registered as All. It can
be generated using command "Scheme All" e.g. "Scheme All for list.".
[register-all,automation,default]

Define an induction principle using Fixpoint for rtree. You may use the Forall predicate to help you.

Exercise: Fibonacci with recursors (advanced)

Here is the Fibonacci function.

Fixpoint fib n : nat :=
  match n with
  | 0 | 1 => 1
  | S (S n as m) => fib m + fib n
  end.

Notice the as keyword to give a name to subexpression S n. This way Rocq knows that S n is a subterm of the one we started with.

Define the Fibonacci function fib using nat_rect directly.

Define it using course-of-values recursion, a form of strong induction shown below. Of course you need to prove brec first.

Fixpoint below (P : nat -> Type) (n : nat) : Type :=
  match n with
  | 0 => unit
  | S n => P n * below P n
  end.

Compute below _ 5.     = (?P 4 * (?P 3 * (?P 2 * (?P 1 * (?P 0 * unit)))))%type
     : Type
where
?P : [ |- nat -> Type]

Fixpoint brec' (P : nat -> Type)
  (F : forall n', below P n' -> P n') (n : nat) {struct n} :
  P n * below P n :=
  REPLACE_ME.Not a truly recursive fixpoint. [non-recursive,fixpoints,default]

Definition brec {P : nat -> Type}
  (F : forall n, below P n -> P n) : forall n, P n :=
  REPLACE_ME.

Reduction

Up till now we've been using simpl a lot without really telling you what it does. Essentially it triggers what we call reduction rules. Those correspond to the evaluation of programs.

The first rule that applies is called β-reduction. What it does is turn (fun x => t) u into t[x := u], which, remember, is a notation for t where every (free) occurrence of x is replaced by u. Or in more mathy, λ-calculus notation:

\begin{equation*} (\lambda x.\ t)\ u \mapsto_{\beta} t[x := u] \end{equation*}

We can see it in action by using the Eval command. It takes as argument a reduction strategy (such as simpl).

Eval simpl in (fun x => x) 2. (* = 2 *)= 2
: nat

Now simpl does much more than β so if we want to only perform β we do:

Eval cbn beta in (fun x => 2 + x) (3 * 4). (* = 2 + 3 * 4 *)= 2 + 3 * 4
: nat

cbn stands for call-by-name and is a strategy that can be parametrised by flags such as beta to limit its action. Here we have limited it to β-reduction. Indeed, one can notice that neither + nor * have been reduced. This way we get control over computation.

We have not really seen them, but it's also possible to introduce let bindings in definitions as a way to name intermediary results.

Expression let x := u in t can be reduced (using ζ-reduction) by substituting u for x in t.

Eval cbn zeta in let x := 100 * 100 in x * x * x.= 100 * 100 * (100 * 100) * (100 * 100)
: nat

Unfolding definitions

There are several ways to unfold definitions. The first one is with the unfold strategy. unfold foo will unfold the constant foo.

Another one is to perform δ-reduction which simply replaces names by the corresponding definitions. A list of names can be provided but is optional. If no name is provided then all possible δ-reductions are performed. To use delta we switch to cbv which stands for call-by-value.

Definition foo := 2 + 9.
Definition bar := let x := 10 in x * x.
Definition baz := foo + bar.

Eval unfold foo in foo + foo.= 2 + 9 + (2 + 9)
: nat
Eval cbv delta [foo bar] in foo + bar + baz.= 2 + 9 + (let x := 10 in x * x) + baz
: nat
Eval cbv delta in foo + bar + baz.= (fix add (n m : nat) {struct n} : nat :=
     match n with
     | 0 => m
     | S p => S (add p m)
     end)
    ((fix add (n m : nat) {struct n} : nat :=
        match n with
        | 0 => m
        | S p => S (add p m)
        end)
       ((fix add (n m : nat) {struct n} : nat :=
           match n with
           | 0 => m
           | S p => S (add p m)
           end)
          2 9)
       (let x := 10 in
        (fix mul (n m : nat) {struct n} : nat :=
           match n with
           | 0 => 0
           | S p =>
               (fix add (n0 m0 : nat) {struct n0} : nat :=
                  match n0 with
                  | 0 => m0
                  | S p0 => S (add p0 m0)
                  end)
                 m (mul p m)
           end)
          x x))
    ((fix add (n m : nat) {struct n} : nat :=
        match n with
        | 0 => m
        | S p => S (add p m)
        end)
       ((fix add (n m : nat) {struct n} : nat :=
           match n with
           | 0 => m
           | S p => S (add p m)
           end)
          2 9)
       (let x := 10 in
        (fix mul (n m : nat) {struct n} : nat :=
           match n with
           | 0 => 0
           | S p =>
               (fix add (n0 m0 : nat) {struct n0} : nat :=
                  match n0 with
                  | 0 => m0
                  | S p0 => S (add p0 m0)
                  end)
                 m (mul p m)
           end)
          x x))
: nat

The output from the previous function might be surprising to you. Let's look at a simpler example to understand what is happening.

Eval cbv delta in 2 + 1.= (fix add (n m : nat) {struct n} : nat :=
     match n with
     | 0 => m
     | S p => S (add p m)
     end)
    2 1
: nat

What happened is that Rocq here also unfolded the definition of + (which is Nat.add) which is defined through a combination of Fixpoint (or fix) and pattern matching (match).

Strategies like cbn or simpl attempt to be nicer on the user and actually refold definitions such as + in the end because it's much easier to read.

More reduction rules

fix and match have their own set of reduction rules of the same name. The combination of the two is called ι-reduction (ι like [i]nductive).

We will see how it goes in interactive mode where we can also use unfold, cbn or cbv as tactics (exactly like simpl).

Goal 2 + 1 = 3.2 + 1 = 3
Proof.2 + 1 = 3
  cbv delta.(fix add (n m : nat) {struct n} : nat :=
   match n with
   | 0 => m
   | S p => S (add p m)
   end)
  2 1 =
3

This performs one unfolding of the fix:

  cbn fix.match 2 with
| 0 => 1
| S p =>
    S
      ((fix add (n m : nat) {struct n} : nat :=
          match n with
          | 0 => m
          | S p0 => S (add p0 m)
          end)
         p 1)
end = 3

It's still there in the recursive branch!

Now we reduce to the right branch:

  cbn match.S
  ((fix add (n m : nat) {struct n} : nat :=
      match n with
      | 0 => m
      | S p => S (add p m)
      end)
     1 1) =
3

One more step:

  cbn fix.S
  match 1 with
  | 0 => 1
  | S p =>
      S
        ((fix add (n m : nat) {struct n} : nat :=
            match n with
            | 0 => m
            | S p0 => S (add p0 m)
            end)
           p 1)
  end =
3 cbn match.S
  (S
     ((fix add (n m : nat) {struct n} : nat :=
         match n with
         | 0 => m
         | S p => S (add p m)
         end)
        0 1)) =
3

Or we use ι-reduction which does it all at once:

  cbn iota.3 = 3
Abort.

To summarise, the available reduction rules are

β for function application;
ζ for letin;
δ for constants;
match for matches;
fix for fixpoints;
ι combining fix and match.

Controlling unfolding

Sometimes we want to simplify an expression but only focusing on some parts. Say in the expression (S n + m) - m from last week where we only wanted to reduce the + part. We showed simpl add but there are other ways to do it.

For instance, you can give to cbn a list of definitions it can unfold. Notice how we can use the notation directly!

Goal forall n m, (S n + m) - m = n.forall n m : nat, S n + m - m = n
Proof.forall n m : nat, S n + m - m = n
  intros n m.n, m: nat
S n + m - m = n
  cbn [ "+" ].n, m: nat
S (n + m) - m = n
Abort.

Sometimes we'd rather provide a list of exceptions not to be unfolded. For this we use the minus symbol before the list.

Goal forall n m, (S n + m) - m = n.forall n m : nat, S n + m - m = n
Proof.forall n m : nat, S n + m - m = n
  intros n m.n, m: nat
S n + m - m = n
  cbn - [ "-" ].n, m: nat
S (n + m) - m = n
Abort.

Below is a demo of examples of proof terms. In particular we show you cases where the proof term is much shorter than using tactics.

Section Demo.

 Variables X Y Z: Prop.

 Check fun (x : X) => x.fun x : X => x
     : X -> X
 Check fun (x : X) (y : Y) => x.fun (x : X) (_ : Y) => x
     : X -> Y -> X
 Check fun (x : X) (y : Y) => y.fun (_ : X) (y : Y) => y
     : X -> Y -> Y
 Check fun (f : X -> Y -> Z) y x => f x y.fun (f : X -> Y -> Z) (y : Y) (x : X) => f x y
     : (X -> Y -> Z) -> Y -> X -> Z
 Check fun (h : X /\ Y) => match h with conj x y => x end.fun h : X /\ Y => match h with
                  | conj x _ => x
                  end
     : X /\ Y -> X
 Check fun (h : X /\ Y) => match h with conj x y => y end.fun h : X /\ Y => match h with
                  | conj _ y => y
                  end
     : X /\ Y -> Y
 Check fun (h : X /\ Y) => match h with conj x y => conj y x end.fun h : X /\ Y => match h with
                  | conj x y => conj y x
                  end
     : X /\ Y -> Y /\ X
 Check
   fun (h : (X /\ Y) /\ Z) =>
     match h with
       conj (conj x y) z => conj x (conj y z)
     end.fun h : (X /\ Y) /\ Z =>
match h with
| conj (conj x y) z => conj x (conj y z)
end
     : (X /\ Y) /\ Z -> X /\ Y /\ Z

Note implicit argument overloading of or_introl and or_intror.

 Check fun (h : X \/ Y) =>
  match h with
    or_introl x => or_intror Y x
  | or_intror y => or_introl X y
  end.fun h : X \/ Y =>
match h with
| or_introl x => or_intror x
| or_intror y => or_introl y
end
     : X \/ Y -> Y \/ X
 Check fun (h : (X \/ Y) \/ Z) =>
  match h with
    or_introl (or_introl x) => or_introl (Y \/ Z) x
  | or_introl (or_intror y) => or_intror (or_introl y)
  | or_intror z => or_intror (or_intror z)
  end.fun h : (X \/ Y) \/ Z =>
match h with
| or_introl (or_introl x) => or_introl x
| or_introl (or_intror y) => or_intror (or_introl y)
| or_intror z => or_intror (or_intror z)
end
     : (X \/ Y) \/ Z -> X \/ Y \/ Z
 Check conj
   (fun (h : X /\ Y) => match h with conj x y => conj y x end)
   (fun (h : Y /\ X) => match h with conj y x => conj x y end).conj (fun h : X /\ Y => match h with
                        | conj x y => conj y x
                        end)
  (fun h : Y /\ X => match h with
                     | conj y x => conj x y
                     end)
     : (X /\ Y -> Y /\ X) /\ (Y /\ X -> X /\ Y)

ex falso quodlibet:

 Check fun h: False => match h return X with end.fun h : False => match h return X with
                 end
     : False -> X

 Check fun x (f : ~X) => f x.fun (x : X) (f : ~ X) => f x
     : X -> ~ X -> False
 Check fun x (f : ~X) => elim_False Y (f x).fun (x : X) (f : ~ X) => elim_False Y (f x)
     : X -> ~ X -> Y
 Check fun x (f : ~X) => match f x return Y with end.fun (x : X) (f : ~ X) => match f x return Y with
                         end
     : X -> ~ X -> Y
 Check fun (f : X -> ~X) g => let x := g (fun x => f x x) in f x x.fun (f : X -> ~ X) (g : (X -> False) -> X) =>
let x : X := g (fun x : X => f x x) in f x x
     : (X -> ~ X) -> ((X -> False) -> X) -> False

 Fact Russell' :
   ~ (X <-> ~ X).X, Y, Z: Prop
~ (X <-> ~ X)
 Proof.X, Y, Z: Prop
~ (X <-> ~ X)
   intros [f g].X, Y, Z: Prop
f: X -> ~ X
g: ~ X -> X
False
   assert (x : X).X, Y, Z: Prop
f: X -> ~ X
g: ~ X -> X
X
X, Y, Z: Prop
f: X -> ~ X
g: ~ X -> X
x: X
False
   -X, Y, Z: Prop
f: X -> ~ X
g: ~ X -> X
X apply g.X, Y, Z: Prop
f: X -> ~ X
g: ~ X -> X
~ X intros x.X, Y, Z: Prop
f: X -> ~ X
g: ~ X -> X
x: X
False exact (f x x).
   -X, Y, Z: Prop
f: X -> ~ X
g: ~ X -> X
x: X
False exact (f x x).
   Show Proof.((fun H : X <-> ~ X =>
  match H with
  | conj x x0 =>
      (fun (f : X -> ~ X) (g : ~ X -> X) =>
       let x1 : X := g ((fun x1 : X => f x1 x1) : ~ X) in f x1 x1) x x0
  end)
 :
 ~ (X <-> ~ X))
 Qed.

 Goal ~ (X <-> ~ X).X, Y, Z: Prop
~ (X <-> ~ X)
 Proof.X, Y, Z: Prop
~ (X <-> ~ X)
   refine (fun a => match a with conj f g => _ end).X, Y, Z: Prop
a: X <-> ~ X
f: X -> ~ X
g: ~ X -> X
False
   refine (let x:X := _ in f x x).X, Y, Z: Prop
a: X <-> ~ X
f: X -> ~ X
g: ~ X -> X
X
   refine (g (fun x => _)).X, Y, Z: Prop
a: X <-> ~ X
f: X -> ~ X
g: ~ X -> X
x: X
False
   exact (f x x).
   Show Proof.(fun a : X <-> ~ X =>
 match a with
 | conj f g => let x : X := g (fun x : X => f x x) in f x x
 end)
 Qed.

End Demo.

Exercise: Type : Type (advanced)

We are going to prove a theorem allowing to prove False from Type : Type. Fill in the missing parts below.

Module Hierarchy.

  Definition embeds X Y :=
    exists (E : X -> Y) (D : Y -> X),
      forall x, D (E x) = x.

  Fact embeds_refl X :
    embeds X X.X: Type
embeds X X
  Proof.X: Type
embeds X X
  Admitted.

  Definition Tyi :=
    Type.

  Inductive tree (A : Tyi) (D : A -> Tyi) : Tyi :=
  | T (a : A) (f : D a -> tree A D).

  Arguments T { _ _}.

  Definition sub {A : Tyi} {D : A -> Tyi} (s t : @tree A D) : Prop :=
    match t with
    | T a f => exists x, f x = s
    end.

  Fact sub_irrefl {A D} :
    forall s : tree A D, ~ sub s s.A: Tyi
D: A -> Tyi
forall s : tree A D, ~ sub s s
  Proof.A: Tyi
D: A -> Tyi
forall s : tree A D, ~ sub s s
  Admitted.

  Lemma hier A D (E : Tyi -> A) :
    ~ embeds (tree A D) (D (E (tree A D))).A: Type
D: A -> Tyi
E: Tyi -> A
~ embeds (tree A D) (D (E (tree A D)))
  Proof.A: Type
D: A -> Tyi
E: Tyi -> A
~ embeds (tree A D) (D (E (tree A D)))
  Admitted.

  Theorem hierarchy :
    forall (X : Tyi),
      ~ embeds Tyi X.forall X : Tyi, ~ embeds Tyi X
  Proof.forall X : Tyi, ~ embeds Tyi X
  Admitted.

We now enable the Type : Type rule.

  Unset Universe Checking.

  Lemma inconsistent : False.False
  Proof.False
    apply (hierarchy Tyi).embeds Tyi Tyi
    apply embeds_refl.
  Qed.

End Hierarchy.