Exercise session 3 — Solutions

🏠 Go back to the course homepage.

From Stdlib Require Import List.
Import ListNotations.

Set Default Goal Selector "!".

EXERCISE

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 :=
  fun P Q p q => p.ex1 is defined

Definition ex2 :
  forall (P Q R : Prop), P -> (P -> Q) -> (P -> Q -> R) -> R
:= fun P Q R p f g => g p (f p).ex2 is defined

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

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

EXERCISE

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)
  intros n m h.n, m: nat
h: lt n m
lt n (4 + m)
  apply lt_S.n, m: nat
h: lt n m
lt n (S (S (S m))) apply lt_S.n, m: nat
h: lt n m
lt n (S (S m)) apply lt_S.n, m: nat
h: lt n m
lt n (S m) apply lt_S.n, m: nat
h: lt n m
lt n m apply h.
Qed.lt_plus_4 is defined

Note we make lt_S easier to use by making n, m implicit.

Arguments lt_S {n m}.

EXERCISE

Prove the following with a proof term.

Definition lt_plus_4' n m : lt n m -> lt n (4 + m) :=
  fun h => lt_S (lt_S (lt_S (lt_S h))).lt_plus_4' is defined

EXERCISE

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

Definition or_comm P Q : P \/ Q -> Q \/ P :=
  fun h =>
    match h with
    | or_introl p => or_intror p
    | or_intror q => or_introl q
    end.or_comm is defined

EXERCISE

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
:=
  fun X P Q equiv f x =>
    match equiv x with
    | conj hpq hqp =>
        hqp (f x)
    end.ex3 is defined

We can also write it this way:

Definition ex3_alt :
  forall X (P Q : X -> Prop),
    (forall x, P x <-> Q x) ->
    (forall x, Q x) ->
    forall x, P x
:=
  fun X P Q equiv f x =>
    let 'conj hpq hqp := equiv x in
    hqp (f x).ex3_alt is defined

EXERCISE

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

Definition Russel X : ~ (X <-> ~ X)
:=
  fun h =>
    let 'conj f g := h in
    let x : X := g (fun x => f x x) in
    f x x.Russel is defined

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

EXERCISE

Show that iFalse is equivalent to False.

Lemma iFalse_iff : False <-> iFalse.False <-> iFalse
Proof.False <-> iFalse
  split.False -> iFalse
iFalse -> False
  -False -> iFalse contradiction.
  -iFalse -> False intro h.h: iFalse
False apply h.
Qed.iFalse_iff is defined

EXERCISE

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

Definition iTrue : Prop :=
  iFalse -> iFalse.iTrue is defined

Lemma iTrue_iff : True <-> iTrue.True <-> iTrue
Proof.True <-> iTrue
  split.True -> iTrue
iTrue -> True
  -True -> iTrue intros _.iTrue intros h.h: iFalse
iFalse assumption.
  -iTrue -> True intros _.True constructor.
Qed.iTrue_iff is defined

EXERCISE

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

If you look at the solution you should see that they are in a sense connected to the elimination rule of the corresponding connective. Note that you can get it basically by using Print and_ind.

For conjunction, the idea is that having a proof of A /\ B is that same as being able to prove any X as long as A -> B -> X holds, in other words as long as X is provable assuming A and B.

Another way of seeing it is that if you have h : iAnd P Q then apply h should be equivalent to destruct h' with h' : P /\ Q.

Definition iAnd (P Q : Prop) : Prop :=
  forall (X : Prop), (P -> Q -> X) -> X.iAnd is defined

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
  intros P Q.P, Q: Prop
P /\ Q <-> iAnd P Q split.P, Q: Prop
P /\ Q -> iAnd P Q
P, Q: Prop
iAnd P Q -> P /\ Q
  -P, Q: Prop
P /\ Q -> iAnd P Q intros [hP hQ].P, Q: Prop
hP: P
hQ: Q
iAnd P Q intros X h.P, Q: Prop
hP: P
hQ: Q
X: Prop
h: P -> Q -> X
X
    apply h.P, Q: Prop
hP: P
hQ: Q
X: Prop
h: P -> Q -> X
P
P, Q: Prop
hP: P
hQ: Q
X: Prop
h: P -> Q -> X
Q all: assumption.
  -P, Q: Prop
iAnd P Q -> P /\ Q intros h.P, Q: Prop
h: iAnd P Q
P /\ Q apply h.P, Q: Prop
h: iAnd P Q
P -> Q -> P /\ Q
    intros hP hQ.P, Q: Prop
h: iAnd P Q
hP: P
hQ: Q
P /\ Q split.P, Q: Prop
h: iAnd P Q
hP: P
hQ: Q
P
P, Q: Prop
h: iAnd P Q
hP: P
hQ: Q
Q all: assumption.
Qed.iAnd_iff is defined

For disjunction it's similar, but with two branches.

Definition iOr (P Q : Prop) : Prop :=
  forall (X : Prop), (P -> X) -> (Q -> X) -> X.iOr is defined

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
  intros P Q.P, Q: Prop
P \/ Q <-> iOr P Q split.P, Q: Prop
P \/ Q -> iOr P Q
P, Q: Prop
iOr P Q -> P \/ Q
  -P, Q: Prop
P \/ Q -> iOr P Q intros h X hP hQ.P, Q: Prop
h: P \/ Q
X: Prop
hP: P -> X
hQ: Q -> X
X
    destruct h.P, Q: Prop
H: P
X: Prop
hP: P -> X
hQ: Q -> X
X
P, Q: Prop
H: Q
X: Prop
hP: P -> X
hQ: Q -> X
X
    +P, Q: Prop
H: P
X: Prop
hP: P -> X
hQ: Q -> X
X apply hP.P, Q: Prop
H: P
X: Prop
hP: P -> X
hQ: Q -> X
P assumption.
    +P, Q: Prop
H: Q
X: Prop
hP: P -> X
hQ: Q -> X
X apply hQ.P, Q: Prop
H: Q
X: Prop
hP: P -> X
hQ: Q -> X
Q assumption.
  -P, Q: Prop
iOr P Q -> P \/ Q intros h.P, Q: Prop
h: iOr P Q
P \/ Q apply h.P, Q: Prop
h: iOr P Q
P -> P \/ Q
P, Q: Prop
h: iOr P Q
Q -> P \/ Q
    +P, Q: Prop
h: iOr P Q
P -> P \/ Q intro.P, Q: Prop
h: iOr P Q
H: P
P \/ Q left.P, Q: Prop
h: iOr P Q
H: P
P assumption.
    +P, Q: Prop
h: iOr P Q
Q -> P \/ Q intro.P, Q: Prop
h: iOr P Q
H: Q
P \/ Q right.P, Q: Prop
h: iOr P Q
H: Q
Q assumption.
Qed.iOr_iff is defined

Definition iEx (X : Type) (P : X -> Prop) : Prop :=
  forall (Y : Prop), (forall x, P x -> Y) -> Y.iEx is defined

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
  intros X P.X: Type
P: X -> Prop
(exists x : X, P x) <-> iEx X P split.X: Type
P: X -> Prop
(exists x : X, P x) -> iEx X P
X: Type
P: X -> Prop
iEx X P -> exists x : X, P x
  -X: Type
P: X -> Prop
(exists x : X, P x) -> iEx X P intros [x hx] Y h.X: Type
P: X -> Prop
x: X
hx: P x
Y: Prop
h:= forall x: X, P x -> Y
Y
    specialize (h x hx).X: Type
P: X -> Prop
x: X
hx: P x
Y: Prop
h: Y
Y
    assumption.
  -X: Type
P: X -> Prop
iEx X P -> exists x : X, P x intros h.X: Type
P: X -> Prop
h: iEx X P
exists x : X, P x apply h.X: Type
P: X -> Prop
h: iEx X P
forall x : X, P x -> exists x0 : X, P x0
    intros x hx.X: Type
P: X -> Prop
h: iEx X P
x: X
hx: P x
exists x0 : X, P x0
    exists x.X: Type
P: X -> Prop
h: iEx X P
x: X
hx: P x
P x assumption.
Qed.iEx_iff is defined

Advanced exercises

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)

EXERCISE

Define a map function for ntree. Hint: You probably will have to change Definition into something else. Answer: You need Fixpoint.

Fixpoint ntree_map {A B} (f : A -> B) (t : ntree A) : ntree B :=
  match t with
  | nnode _ a l => nnode _ (f a) (nforest_map f l)
  end

with nforest_map {A B} (f : A -> B) (l : nforest A) :=
  match l with
  | nnil _ => nnil _
  | ncons _ t tl => ncons _ (ntree_map f t) (nforest_map f tl)
  end.ntree_map is defined
nforest_map is defined
ntree_map, nforest_map are recursively defined (guarded respectively on 4th, 4th 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

EXERCISE

Can you give an element of type tree?

Definition ex4 : tree :=
  N [].ex4 is defined

Inductive All {X} (P : X -> Type) : list X -> Type :=
| All_nil : All P nil
| All_cons x l : P x -> All P l -> All P (x :: l).All is defined
All_rect is defined
All_ind is defined
All_rec is defined
All_sind is defined

Arguments All_nil {X P}.
Arguments All_cons {X P}.

Fixpoint tree_rect_strong (P : tree -> Type)
    (f : forall (ts : list tree), All P ts -> P (N ts))
    (t : tree) : P t :=
  let fix F ts : All P ts :=
    match ts with
    | [] => All_nil
    | t' :: l => All_cons _ _ (tree_rect_strong P f t') (F l)
    end
  in
  match t with
  | N ts => f ts (F ts)
  end.tree_rect_strong is defined
tree_rect_strong is recursively defined (guarded on 3rd argument)

EXERCISE

Extend the type tree to have labelled nodes.

Prove a bijection between the new tree and ntree, ie. define functions to_tree : forall A, ntree A -> tree A from_tree : forall A, tree A -> ntree A and show that they invert each other.

For the solution, we will make a new tree type, called xtree for e``x``tended.

Inductive xtree A :=
| Nx (x : A) (ts : list (xtree A)).xtree is defined
xtree_rect is defined
xtree_ind is defined
xtree_rec is defined
xtree_sind is defined

Fixpoint to_tree {A} (t : ntree A) : xtree A :=
  match t with
  | nnode _ a l => Nx _ a (to_tree_list l)
  end

with to_tree_list {A} (l : nforest A) : list (xtree A) :=
  match l with
  | nnil _ => []
  | ncons _ t tl => to_tree t :: to_tree_list tl
  end.to_tree is defined
to_tree_list is defined
to_tree, to_tree_list are recursively defined (guarded respectively on 2nd, 2nd arguments)

Fixpoint from_tree {A} (t : xtree A) : ntree A :=
  let fix F ts :=
    match ts with
    | [] => nnil _
    | t :: l => ncons _ (from_tree t) (F l)
    end
  in
  match t with
  | Nx _ a ts => nnode _ a (F ts)
  end.from_tree is defined
from_tree is recursively defined (guarded on 2nd argument)

We reprove the induction principle from above.

Fixpoint xtree_rect_strong A (P : xtree A -> Type)
    (f : forall a ts, All P ts -> P (Nx _ a ts))
    (t : xtree A) : P t :=
  let fix F ts : All P ts :=
    match ts with
    | [] => All_nil
    | t' :: l => All_cons _ _ (xtree_rect_strong A P f t') (F l)
    end
  in
  match t with
  | Nx _ a ts => f a ts (F ts)
  end.xtree_rect_strong is defined
xtree_rect_strong is recursively defined (guarded on 4th argument)

Then we can use it to prove one direction.

Lemma to_from_tree :
  forall A (t : xtree A),
    to_tree (from_tree t) = t.forall (A : Type) (t : xtree A), to_tree (from_tree t) = t
Proof.forall (A : Type) (t : xtree A), to_tree (from_tree t) = t
  intros A t.A: Type
t: xtree A
to_tree (from_tree t) = t
  induction t as [a ts ih] using xtree_rect_strong.A: Type
a: A
ts: list (xtree A)
ih:= All (fun t: xtree A => to_tree (from_tree t) = t) ts
to_tree (from_tree (Nx A a ts)) = Nx A a ts
  cbn.A: Type
a: A
ts: list (xtree A)
ih:= All (fun t: xtree A => to_tree (from_tree t) = t) ts
Nx A a (to_tree_list ((fix F (ts0 : list (xtree A)) : nforest A := match ts0 with | [] => nnil A | t :: l => ncons A (from_tree t) (F l) end) ts)) = Nx A a ts f_equal.A: Type
a: A
ts: list (xtree A)
ih:= All (fun t: xtree A => to_tree (from_tree t) = t) ts
to_tree_list ((fix F (ts0 : list (xtree A)) : nforest A := match ts0 with | [] => nnil A | t :: l => ncons A (from_tree t) (F l) end) ts) = ts
  induction ih as [| t l e hl ihl].A: Type
a: A
to_tree_list (nnil A) = []
A: Type
a: A
t: xtree A
l: list (xtree A)
e: to_tree (from_tree t) = t
hl:= All (fun t: xtree A => to_tree (from_tree t) = t) l
ihl:= to_tree_list ((fix F (ts : list (xtree A)) : nforest A := match ts with | [] => nnil A | t :: l => ncons A (from_tree t) (F l) end) l) = l
to_tree_list (ncons A (from_tree t) ((fix F (ts : list (xtree A)) : nforest A := match ts with | [] => nnil A | t0 :: l0 => ncons A (from_tree t0) (F l0) end) l)) = t :: l
  -A: Type
a: A
to_tree_list (nnil A) = [] reflexivity.
  -A: Type
a: A
t: xtree A
l: list (xtree A)
e: to_tree (from_tree t) = t
hl:= All (fun t: xtree A => to_tree (from_tree t) = t) l
ihl:= to_tree_list ((fix F (ts : list (xtree A)) : nforest A := match ts with | [] => nnil A | t :: l => ncons A (from_tree t) (F l) end) l) = l
to_tree_list (ncons A (from_tree t) ((fix F (ts : list (xtree A)) : nforest A := match ts with | [] => nnil A | t0 :: l0 => ncons A (from_tree t0) (F l0) end) l)) = t :: l cbn.A: Type
a: A
t: xtree A
l: list (xtree A)
e: to_tree (from_tree t) = t
hl:= All (fun t: xtree A => to_tree (from_tree t) = t) l
ihl:= to_tree_list ((fix F (ts : list (xtree A)) : nforest A := match ts with | [] => nnil A | t :: l => ncons A (from_tree t) (F l) end) l) = l
to_tree (from_tree t) :: to_tree_list ((fix F (ts : list (xtree A)) : nforest A := match ts with | [] => nnil A | t0 :: l0 => ncons A (from_tree t0) (F l0) end) l) = t :: l rewrite e.A: Type
a: A
t: xtree A
l: list (xtree A)
e: to_tree (from_tree t) = t
hl:= All (fun t: xtree A => to_tree (from_tree t) = t) l
ihl:= to_tree_list ((fix F (ts : list (xtree A)) : nforest A := match ts with | [] => nnil A | t :: l => ncons A (from_tree t) (F l) end) l) = l
t :: to_tree_list ((fix F (ts : list (xtree A)) : nforest A := match ts with | [] => nnil A | t0 :: l0 => ncons A (from_tree t0) (F l0) end) l) = t :: l f_equal.A: Type
a: A
t: xtree A
l: list (xtree A)
e: to_tree (from_tree t) = t
hl:= All (fun t: xtree A => to_tree (from_tree t) = t) l
ihl:= to_tree_list ((fix F (ts : list (xtree A)) : nforest A := match ts with | [] => nnil A | t :: l => ncons A (from_tree t) (F l) end) l) = l
to_tree_list ((fix F (ts : list (xtree A)) : nforest A := match ts with | [] => nnil A | t0 :: l0 => ncons A (from_tree t0) (F l0) end) l) = l
    apply ihl.
Qed.to_from_tree is defined

For the other direction, it's maybe more complicated.

We'll show you several ways. One is to use mutual fixed points like for when defining the function. When doing this interactively, we have to be careful that we indeed use the induction hypothesis only on strict subterms. Warning: Rocq will only check at Qed, not before. You can still ask if it's ok up to this point by using the Guarded command inside the proof.

For this, we also give a name to the fix nested in from_tree.

(*
Fixpoint from_tree_list {A} (l : list (xtree A)) :=
  match l with
  | [] => nnil _
  | t :: l => ncons _ (from_tree t) (from_tree_list l)
  end.
*)

Definition from_tree_list {A} :=
  fix F (ts : list (xtree A)) : nforest A :=
    match ts with
    | [] => nnil A
    | t :: l0 => ncons A (from_tree t) (F l0)
    end.from_tree_list is defined

Fixpoint from_to_tree A (t : ntree A) :
  from_tree (to_tree t) = t

with from_to_tree_list A (l : nforest A) :
  from_tree_list (to_tree_list l) = l.from_to_tree:= forall (A : Type) (t: ntree A), from_tree (to_tree t) = t
from_to_tree_list:= forall (A : Type) (l: nforest A), from_tree_list (to_tree_list l) = l
A: Type
t: ntree A
from_tree (to_tree t) = t
from_to_tree:= forall (A : Type) (t: ntree A), from_tree (to_tree t) = t
from_to_tree_list:= forall (A : Type) (l: nforest A), from_tree_list (to_tree_list l) = l
A: Type
l: nforest A
from_tree_list (to_tree_list l) = l

Proof.from_to_tree:= forall (A : Type) (t: ntree A), from_tree (to_tree t) = t
from_to_tree_list:= forall (A : Type) (l: nforest A), from_tree_list (to_tree_list l) = l
A: Type
t: ntree A
from_tree (to_tree t) = t
from_to_tree:= forall (A : Type) (t: ntree A), from_tree (to_tree t) = t
from_to_tree_list:= forall (A : Type) (l: nforest A), from_tree_list (to_tree_list l) = l
A: Type
l: nforest A
from_tree_list (to_tree_list l) = l
  -from_to_tree:= forall (A : Type) (t: ntree A), from_tree (to_tree t) = t
from_to_tree_list:= forall (A : Type) (l: nforest A), from_tree_list (to_tree_list l) = l
A: Type
t: ntree A
from_tree (to_tree t) = t destruct t as [a l].from_to_tree:= forall (A : Type) (t: ntree A), from_tree (to_tree t) = t
from_to_tree_list:= forall (A : Type) (l: nforest A), from_tree_list (to_tree_list l) = l
A: Type
a: A
l: nforest A
from_tree (to_tree (nnode A a l)) = nnode A a l
    cbn.from_to_tree:= forall (A : Type) (t: ntree A), from_tree (to_tree t) = t
from_to_tree_list:= forall (A : Type) (l: nforest A), from_tree_list (to_tree_list l) = l
A: Type
a: A
l: nforest A
nnode A a ((fix F (ts : list (xtree A)) : nforest A := match ts with | [] => nnil A | t :: l0 => ncons A (from_tree t) (F l0) end) (to_tree_list l)) = nnode A a l f_equal.from_to_tree:= forall (A : Type) (t: ntree A), from_tree (to_tree t) = t
from_to_tree_list:= forall (A : Type) (l: nforest A), from_tree_list (to_tree_list l) = l
A: Type
a: A
l: nforest A
(fix F (ts : list (xtree A)) : nforest A := match ts with | [] => nnil A | t :: l0 => ncons A (from_tree t) (F l0) end) (to_tree_list l) = l apply from_to_tree_list.
  -from_to_tree:= forall (A : Type) (t: ntree A), from_tree (to_tree t) = t
from_to_tree_list:= forall (A : Type) (l: nforest A), from_tree_list (to_tree_list l) = l
A: Type
l: nforest A
from_tree_list (to_tree_list l) = l destruct l as [| a l].from_to_tree:= forall (A : Type) (t: ntree A), from_tree (to_tree t) = t
from_to_tree_list:= forall (A : Type) (l: nforest A), from_tree_list (to_tree_list l) = l
A: Type
from_tree_list (to_tree_list (nnil A)) = nnil A
from_to_tree:= forall (A : Type) (t: ntree A), from_tree (to_tree t) = t
from_to_tree_list:= forall (A : Type) (l: nforest A), from_tree_list (to_tree_list l) = l
A: Type
a: ntree A
l: nforest A
from_tree_list (to_tree_list (ncons A a l)) = ncons A a l
    +from_to_tree:= forall (A : Type) (t: ntree A), from_tree (to_tree t) = t
from_to_tree_list:= forall (A : Type) (l: nforest A), from_tree_list (to_tree_list l) = l
A: Type
from_tree_list (to_tree_list (nnil A)) = nnil A reflexivity.
    +from_to_tree:= forall (A : Type) (t: ntree A), from_tree (to_tree t) = t
from_to_tree_list:= forall (A : Type) (l: nforest A), from_tree_list (to_tree_list l) = l
A: Type
a: ntree A
l: nforest A
from_tree_list (to_tree_list (ncons A a l)) = ncons A a l cbn.from_to_tree:= forall (A : Type) (t: ntree A), from_tree (to_tree t) = t
from_to_tree_list:= forall (A : Type) (l: nforest A), from_tree_list (to_tree_list l) = l
A: Type
a: ntree A
l: nforest A
ncons A (from_tree (to_tree a)) (from_tree_list (to_tree_list l)) = ncons A a l rewrite from_to_tree, from_to_tree_list.from_to_tree:= forall (A : Type) (t: ntree A), from_tree (to_tree t) = t
from_to_tree_list:= forall (A : Type) (l: nforest A), from_tree_list (to_tree_list l) = l
A: Type
a: ntree A
l: nforest A
ncons A a l = ncons A a l reflexivity.
Qed.from_to_tree is defined
from_to_tree_list is defined

Another option is to use Scheme which will derive better induction principles, working with mutual inductive types.

With them, no more fear of non-terminating fixed points.

Scheme ntree_nforest_rec := Induction for ntree Sort Set
  with nforest_ntree_rec := Induction for nforest Sort Set.ntree_nforest_rec is defined
nforest_ntree_rec is defined
ntree_nforest_rec, nforest_ntree_rec are recursively defined

Lemma from_to_tree_alt :
  forall A (t : ntree A),
    from_tree (to_tree t) = t.forall (A : Type) (t : ntree A), from_tree (to_tree t) = t
Proof.forall (A : Type) (t : ntree A), from_tree (to_tree t) = t
  intros A t.A: Type
t: ntree A
from_tree (to_tree t) = t

Before we apply the induction principle, we tell Rocq to see the goal as a predicate over t with the pattern t tactic.

  pattern t.A: Type
t: ntree A
(fun n : ntree A => from_tree (to_tree n) = n) t

Now we need to give the predicate for forests:

  apply ntree_nforest_rec
  with (P0 := fun l => from_tree_list (to_tree_list l) = l).A: Type
t: ntree A
forall (a : A) (n : nforest A), from_tree_list (to_tree_list n) = n -> from_tree (to_tree (nnode A a n)) = nnode A a n
A: Type
t: ntree A
from_tree_list (to_tree_list (nnil A)) = nnil A
A: Type
t: ntree A
forall n : ntree A, from_tree (to_tree n) = n -> forall n0 : nforest A, from_tree_list (to_tree_list n0) = n0 -> from_tree_list (to_tree_list (ncons A n n0)) = ncons A n n0
  -A: Type
t: ntree A
forall (a : A) (n : nforest A), from_tree_list (to_tree_list n) = n -> from_tree (to_tree (nnode A a n)) = nnode A a n intros a l ih.A: Type
t: ntree A
a: A
l: nforest A
ih: from_tree_list (to_tree_list l) = l
from_tree (to_tree (nnode A a l)) = nnode A a l
    cbn.A: Type
t: ntree A
a: A
l: nforest A
ih: from_tree_list (to_tree_list l) = l
nnode A a ((fix F (ts : list (xtree A)) : nforest A := match ts with | [] => nnil A | t0 :: l0 => ncons A (from_tree t0) (F l0) end) (to_tree_list l)) = nnode A a l f_equal.A: Type
t: ntree A
a: A
l: nforest A
ih: from_tree_list (to_tree_list l) = l
(fix F (ts : list (xtree A)) : nforest A := match ts with | [] => nnil A | t0 :: l0 => ncons A (from_tree t0) (F l0) end) (to_tree_list l) = l apply ih.
  -A: Type
t: ntree A
from_tree_list (to_tree_list (nnil A)) = nnil A reflexivity.
  -A: Type
t: ntree A
forall n : ntree A, from_tree (to_tree n) = n -> forall n0 : nforest A, from_tree_list (to_tree_list n0) = n0 -> from_tree_list (to_tree_list (ncons A n n0)) = ncons A n n0 intros t' iht l ihl.A: Type
t, t': ntree A
iht: from_tree (to_tree t') = t'
l: nforest A
ihl: from_tree_list (to_tree_list l) = l
from_tree_list (to_tree_list (ncons A t' l)) = ncons A t' l
    cbn.A: Type
t, t': ntree A
iht: from_tree (to_tree t') = t'
l: nforest A
ihl: from_tree_list (to_tree_list l) = l
ncons A (from_tree (to_tree t')) (from_tree_list (to_tree_list l)) = ncons A t' l rewrite iht, ihl.A: Type
t, t': ntree A
iht: from_tree (to_tree t') = t'
l: nforest A
ihl: from_tree_list (to_tree_list l) = l
ncons A t' l = ncons A t' l reflexivity.
Qed.from_to_tree_alt is defined

Here is the Fibonnaci function.

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.

Fixpoint fib n : nat :=
  match n with
  | 0 | 1 => 1
  | S (S n as m) => fib m + fib n
  end.fib is defined
fib is recursively defined (guarded on 1st argument)

EXERCISE

Define the Fibonnaci function fib using nat_rect directly.

The idea is to recursively produce a pair (fib (n-1), fib n) and then take the second projection snd.

Definition fib_natrec n :=
  let p :=
    nat_rect (fun _ => (nat * nat)%type)
      (0,1)
      (fun _ '(f0, f1) => (f1, f0 + f1))
      n
  in
  snd p.fib_natrec is defined

EXERCISE

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.below is defined
below is recursively defined (guarded on 2nd argument)

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 :=
  match n with
  | 0 => (F 0 tt, tt)
  | S n => let r := brec' P F n in (F (S n) r , r)
  end.brec' is defined
brec' is recursively defined (guarded on 3rd argument)

Definition brec {P : nat -> Type}
  (F : forall n, below P n -> P n) : forall n, P n :=
  fun n => fst (brec' P F n).brec is defined

Definition fib_brec : nat -> nat :=
  brec (fun n =>
    match n with
    | 0 => fun _ => 1
    | 1 => fun _ => 1
    | S (S n) => fun r => fst r + fst (snd r)
    end
  ).fib_brec is defined

Inconsistencies

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

termination of recursive functions, which needs to be ensured

strict positivity of inductives, which you have seen in the lecture

having type hierarchies rather than a Type : Type rule
Unset Guard Checking.

EXERCISE

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

Lemma S_neq n : n <> S n.n: nat
n <> S n
Proof.n: nat
n <> S n
  induction n as [| n ih].0 <> 1
n: nat
ih: n <> S n
S n <> S (S n)
  -0 <> 1 discriminate.
  -n: nat
ih: n <> S n
S n <> S (S n) intros e.n: nat
ih: n <> S n
e: S n = S (S n)
False inversion e.n: nat
ih: n <> S n
e: S n = S (S n)
H0: n = S n
False
    apply ih.n: nat
ih: n <> S n
e: S n = S (S n)
H0: n = S n
n = S n assumption.
Qed.S_neq is defined

Definition idnat (x : nat) := x.idnat is defined

Fixpoint f (x : nat) : nat := S (f (idnat x)).f is defined
f is recursively defined (guarded on 1st argument)

Goal False.False
Proof.False
  apply S_neq with (f 0).f 0 = S (f 0)
  reflexivity.
Qed.Unnamed_thm is defined

Set Guard Checking.

Unset Positivity Checking.

EXERCISE

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

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

Lemma bad_not_bad :
  bad <-> ~ bad.bad <-> ~ bad
Proof.bad <-> ~ bad
  split.bad -> ~ bad
~ bad -> bad
  -bad -> ~ bad intros h [nh].h: bad
nh: bad -> False
False contradiction.
  -~ bad -> bad intros nh.nh: ~ bad
bad constructor.nh: ~ bad
bad -> False assumption.
Qed.bad_not_bad is defined

Goal False.False
Proof.False
  apply (Russel _ bad_not_bad).
Qed.Unnamed_thm0 is defined

Set Positivity Checking.

EXERCISE

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

Module Hierarchy.Interactive Module Hierarchy started

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

  Fact embeds_refl X :
    embeds X X.X: Type
embeds X X
  Proof.X: Type
embeds X X
    exists (fun x => x), (fun x => x).X: Type
forall x : X, x = x reflexivity.
  Qed.embeds_refl is defined

  Definition Tyi :=
    Type.Tyi is defined

  Inductive tree (A : Tyi) (D : A -> Tyi) : Tyi :=
  | T (a : A) (f : D a -> tree A D).tree is defined
tree_rect is defined
tree_ind is defined
tree_rec is defined
tree_sind is defined

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

  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
    induction s as [a f ih].A: Tyi
D: A -> Tyi
a: A
f: D a -> tree A D
ih:= forall d: D a, ~ sub (f d) (f d)
~ sub (T a f) (T a f)
    intros [x e].A: Tyi
D: A -> Tyi
a: A
f: D a -> tree A D
ih:= forall d: D a, ~ sub (f d) (f d)
x: D a
e: f x = T a f
False
    apply (ih x).A: Tyi
D: A -> Tyi
a: A
f: D a -> tree A D
ih:= forall d: D a, ~ sub (f d) (f d)
x: D a
e: f x = T a f
sub (f x) (f x)
    rewrite e at 2.A: Tyi
D: A -> Tyi
a: A
f: D a -> tree A D
ih:= forall d: D a, ~ sub (f d) (f d)
x: D a
e: f x = T a f
sub (f x) (T a f)
    unfold sub.A: Tyi
D: A -> Tyi
a: A
f: D a -> tree A D
ih:= forall d: D a, ~ sub (f d) (f d)
x: D a
e: f x = T a f
exists x0 : D a, f x0 = f x
    exists x.A: Tyi
D: A -> Tyi
a: A
f: D a -> tree A D
ih:= forall d: D a, ~ sub (f d) (f d)
x: D a
e: f x = T a f
f x = f x reflexivity.
  Qed.sub_irrefl is defined

  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)))
    intros [F [G h]].A: Type
D: A -> Tyi
E: Tyi -> A
F: tree A D -> D (E (tree A D))
G: D (E (tree A D)) -> tree A D
h:= forall x: tree A D, G (F x) = x
False
    apply (sub_irrefl (T (E (tree A D)) G)).A: Type
D: A -> Tyi
E: Tyi -> A
F: tree A D -> D (E (tree A D))
G: D (E (tree A D)) -> tree A D
h:= forall x: tree A D, G (F x) = x
sub (T (E (tree A D)) G) (T (E (tree A D)) G)
    simpl.A: Type
D: A -> Tyi
E: Tyi -> A
F: tree A D -> D (E (tree A D))
G: D (E (tree A D)) -> tree A D
h:= forall x: tree A D, G (F x) = x
exists x : D (E (tree A D)), G x = T (E (tree A D)) G exists (F (T (E (tree A D)) G)).A: Type
D: A -> Tyi
E: Tyi -> A
F: tree A D -> D (E (tree A D))
G: D (E (tree A D)) -> tree A D
h:= forall x: tree A D, G (F x) = x
G (F (T (E (tree A D)) G)) = T (E (tree A D)) G apply h.
  Qed.hier is defined

  Theorem hierarchy :
    forall (X : Tyi),
      ~ embeds Tyi X.forall X : Tyi, ~ embeds Tyi X
  Proof.forall X : Tyi, ~ embeds Tyi X
    intros X [E [D h]].X: Tyi
E: Tyi -> X
D: X -> Tyi
h:= forall x: Tyi, D (E x) = x
False
    apply (hier X D E).X: Tyi
E: Tyi -> X
D: X -> Tyi
h:= forall x: Tyi, D (E x) = x
embeds (tree X D) (D (E (tree X D))) rewrite h.X: Tyi
E: Tyi -> X
D: X -> Tyi
h:= forall x: Tyi, D (E x) = x
embeds (tree X D) (tree X D) apply embeds_refl.
  Qed.hierarchy is defined

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

End Hierarchy.Module Hierarchy is defined