MPRI PRFA — Proof Assistants

Proof terms and meta-theory — Part 2

From Stdlib Require Import List.
Import ListNotations.

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!

Note that instead of Qed we need to put Defined to tell Rocq we care about the content of the definition.

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 apply n.add: nat -> nat -> nat
n, m: nat
nat apply m.
Defined.add is defined

Modulo some simplication, 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.Unnamed_thm is defined

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.

Actually, if we deactivate the termination checking, we can derive a proof of False very easily.

Unset Guard Checking.

False is now simply proven via a loop!

Fixpoint f (x : unit) : False := f x.f is defined
f is recursively defined (guarded on 1st argument)

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

Goal False.False
Proof.False
  exact (f tt).
Qed.Unnamed_thm0 is defined

Set Guard Checking.

The termination checker is not the only important part of the system. One such criterion is called strict positivity and is imposed on inductive types definitions.

It says that a constructor to an inductive type cannot mention said inductive type on the left of an arrow (->). See the following example when deactivating positivity checking from which we can derive False.

Unset Positivity Checking.

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

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.Unnamed_thm1 is defined

Set Positivity Checking.

Recursors

Induction principles in Rocq are not primitive, they actually unfold to a combination of Fixpoint and match.

See below how we define them for nat and list.

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.nat_ind is defined
nat_ind is recursively defined (guarded on 4th argument)

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.list_ind is defined
list_ind is recursively defined (guarded on 5th argument)

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]. Or in more mathy, λ-calculus notation:

\begin{equation*} (\lambda x.\ t)\ u \mapsto 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.

Note. δ is like [d]efinition.

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

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 add) which is defined through a combination of Fixpoint (or fix) and pattern matching (match).

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.

Controlling unfolding

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

There are more strategies like lazy, hnf, or vm_compute…

📖 More detail can be found in the reference manual.

Here 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.X is declared
Y is declared
Z is declared

 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)

exfalso quodlibet:

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

 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.Russell is defined

 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.Unnamed_thm2 is defined

End Demo.

ADVANCED

Mutual inductive types

It is also possible to define several inductive types at the same time. You just combine them with the with keyword.

This way we can define the type of trees mutually with that of forests (which are basically lists of trees).

Inductive ntree (A : Type) :=
| nnode : A -> nforest A -> ntree A

with nforest (A : Type) :=
| nnil : nforest A
| ncons : ntree A -> nforest A -> nforest A.ntree, nforest are defined
ntree_rect is defined
ntree_ind is defined
ntree_rec is defined
ntree_sind is defined
nforest_rect is defined
nforest_ind is defined
nforest_rec is defined
nforest_sind is defined

You can then define mutual definitions over such types by using Fixpoint and the with keyword.

Fixpoint count {A} (t : ntree A) {struct t} : nat :=
  match t with
  | nnode _ a l => 1 + count_list l
  end

with count_list {A} (l : nforest A) {struct l} : nat :=
  match l with
  | nnil _ => 0
  | ncons _ t tl => count t + count_list tl
  end.count is defined
count_list is defined
count, count_list are recursively defined (guarded respectively on 2nd, 2nd arguments)

Nested inductive types

Finally, you can define more inductive types by using what is called nesting. In the type below, you define a tree as something that contains a list of trees.

Inductive tree :=
| N (ts : list tree).tree is defined
tree_rect is defined
tree_ind is defined
tree_rec is defined
tree_sind is defined

Definition empty_tree :=
  N [].empty_tree is defined

Definition some_tree :=
  N [ empty_tree ; N [ empty_tree ; empty_tree ] ].some_tree is defined