PRFA.tp3c

Exercise session 3 — Proof terms — SOLUTIONS

From Coq 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 : ∀ (P Q : Prop), P → Q → P :=
fun P Q p q ⇒ p.

Definition ex2 : ∀ (P Q R : Prop), P → (P → Q ) → (P → Q → R ) → R :=
fun P Q R p f g ⇒ g p (f p).

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

EXERCISE

Prove the following lemma interactively using intros and apply.

Lemma lt_plus_4 :
  ∀ n m,
    lt n m →
    lt n (4 + m).
Proof.
  intros n m h.
  apply lt_S. apply lt_S. apply lt_S. apply lt_S. apply h.
Qed.

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

EXERCISE

Prove the following with a proof term. Hint: Use Print or 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.

EXERCISE

Prove the following with a proof term.

Definition ex3 :
  ∀ X (P Q : X → Prop),
    (∀ x, P x ↔ Q x ) →
    (∀ x, Q x ) →
    ∀ x, P x
:=
  fun X P Q equiv f x ⇒
    match equiv x with
    | conj hpq hqp ⇒
        hqp (f x)
    end.

We can also write it this way:

Definition ex3_alt :
  ∀ X (P Q : X → Prop),
    (∀ x, P x ↔ Q x ) →
    (∀ x, Q x ) →
    ∀ x, P x
:=
  fun X P Q equiv f x ⇒
    let 'conj hpq hqp := equiv x in
    hqp (f x).

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.

Impredicative encodings

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

For instance, one can define False as follows:

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

EXERCISE

Show that iFalse is equivalent to False.

Lemma iFalse_iff : False ↔ iFalse.
Proof.
  split.
  - contradiction.
  - intro h. apply h.
Qed.

EXERCISE

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

Definition iTrue : Prop :=
  iFalse → iFalse.

Lemma iTrue_iff : True ↔ iTrue.
Proof.
  split.
  - intros _. intros h. assumption.
  - intros _. constructor.
Qed.

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 :=
  ∀ (X : Prop), (P → Q → X ) → X.

Lemma iAnd_iff :
  ∀ P Q,
    P ∧ Q ↔ iAnd P Q.
Proof.
  intros P Q. split.
  - intros [hP hQ]. intros X h.
    apply h. all: assumption.
  - intros h. apply h.
    intros hP hQ. split. all: assumption.
Qed.

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

Definition iOr (P Q : Prop) : Prop :=
  ∀ (X : Prop), (P → X ) → (Q → X ) → X.

Lemma iOr_iff :
  ∀ P Q,
    P ∨ Q ↔ iOr P Q.
Proof.
  intros P Q. split.
  - intros h X hP hQ.
    destruct h.
    + apply hP. assumption.
    + apply hQ. assumption.
  - intros h. apply h.
    + intro. left. assumption.
    + intro. right. assumption.
Qed.

Definition iEx (X : Type) (P : X → Prop) : Prop :=
  ∀ (Y : Prop), (∀ x, P x → Y ) → Y.

Lemma iEx_iff :
  ∀ X P,
    (∃ (x : X ), P x ) ↔ iEx X P.
Proof.
  intros X P. split.
  - intros [x hx] Y h.
    specialize (h x hx).
    assumption.
  - intros h. apply h.
    intros x hx.
    ∃ x. assumption.
Qed.

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.

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.

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.

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

EXERCISE

Can you give an element of type tree?

Definition ex4 : tree :=
  N [].

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

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

Fixpoint tree_rect_strong (P : tree → Type)
    (f : ∀ (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.

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

Inductive xtree A :=
| Nx (x : A) (ts : list (xtree A)).

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.

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.

We reprove the induction principle from above.

Fixpoint xtree_rect_strong A (P : xtree A → Type)
    (f : ∀ 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.

Then we can use it to prove one direction.

Lemma to_from_tree :
  ∀ A (t : xtree A),
    to_tree (from_tree t) = t.
Proof.
  intros A t.
  induction t as [a ts ih] using xtree_rect_strong.
  cbn. f_equal.
  induction ih as [| t l e hl ihl].
  - reflexivity.
  - cbn. rewrite e. f_equal.
    apply ihl.
Qed.

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: Coq 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.

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.

Proof.
  - destruct t as [a l].
    cbn. f_equal. apply from_to_tree_list.
  - destruct l as [| a l].
    + reflexivity.
    + cbn. rewrite from_to_tree, from_to_tree_list. reflexivity.
Qed.

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.

Lemma from_to_tree_alt :
  ∀ A (t : ntree A),
    from_tree (to_tree t) = t.
Proof.
  intros A t.
  (* Before we apply the induction principle, we tell Coq to see the goal
    as a predicate over t with the pattern t tactic.
  *)
  pattern 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).
  - intros a l ih.
    cbn. f_equal. apply ih.
  - reflexivity.
  - intros t' iht l ihl.
    cbn. rewrite iht, ihl. reflexivity.
Qed.

Here is the Fibonnaci function.

Notice the as keyword to give a name to subexpression S n. This way Coq 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.

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.

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.

Compute below _ 5.

Fixpoint brec' (P : nat → Type)
  (F : ∀ 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.

Definition brec {P : nat → Type}
  (F : ∀ n, below P n → P n) : ∀ n, P n :=
  fun n ⇒ fst (brec' P F n).

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

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.
Proof.
  induction n as [| n ih].
  - discriminate.
  - intros e. inversion e.
    apply ih. assumption.
Qed.

Definition idnat (x : nat) := x.

Fixpoint f (x : nat) : nat := S (f (idnat x)).

Goal False.
Proof.
  apply S_neq with (f 0).
  reflexivity.
Qed.

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.

Lemma bad_not_bad :
  bad ↔ ¬ bad.
Proof.
  split.
  - intros h [nh]. contradiction.
  - intros nh. constructor. assumption.
Qed.

Goal False.
Proof.
  apply (Russel _ bad_not_bad).
Qed.

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.

  Definition embeds X Y :=
    ∃ (E : X → Y) (D : Y → X ),
      ∀ x, D (E x) = x.

  Fact embeds_refl X :
    embeds X X.
  Proof.
  ∃ (fun x ⇒ x), (fun x ⇒ x). reflexivity.
  Qed.

  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 ⇒ ∃ x , f x = s
    end.

  Fact sub_irrefl {A D} :
    ∀ s : tree A D, ¬ sub s s.
  Proof.
    induction s as [a f ih].
    intros [x e].
    apply (ih x).
    rewrite e at 2.
    unfold sub.
    ∃ x. reflexivity.
  Qed.

  Lemma hier A D (E : Tyi → A) :
    ¬ embeds (tree A D) (D (E (tree A D))).
  Proof.
    intros [F [G h]].
    apply (sub_irrefl (T (E (tree A D)) G)).
    simpl. ∃ (F (T (E (tree A D)) G)). apply h.
  Qed.

  Theorem hierarchy :
    ∀ (X : Tyi),
      ¬ embeds Tyi X.
  Proof.
    intros X [E [D h]].
    apply (hier X D E). rewrite h. apply embeds_refl.
  Qed.

We now enable the Type : Type rule

  Unset Universe Checking.

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

End Hierarchy.