PRFA.tp2c

Exercise session 2 — Inductive types — SOLUTIONS

Set Default Goal Selector "!". (* To force bullet usage. *)

Module define_nat.

  (* Inductive types can be defined using the Inductive keyword *)
  Inductive nat :=
  | O : nat
  | S : nat → nat.

EXERCISE
Define addition.
  Fixpoint add (n m : nat) {struct n} : nat :=
    match n with
    | O ⇒ m
    | S n ⇒ S (add n m)
    end.

EXERCISE
Define subtraction on natural numbers, truncating at 0. In other words, when n < m then sub n m = 0.
  Fixpoint sub (n m : nat) : nat :=
    match n, m with
    | O, _ ⇒ O
    | S n', O ⇒ n
    | S n', S m' ⇒ sub n' m'
    end.

EXERCISE
Prove the following lemma. You will replace Admitted with Qed once it is done. What Admitted does should be obvious: it admits a lemma without proof or with a partial proof, it can be used in subsequent proofs as if it were proven.
  Lemma add_0 :
    ∀ n,
      add n O = n.
  Proof.
    intros n. induction n as [| n ih].
    - reflexivity.
    - simpl. rewrite ih. reflexivity.
  Qed.

EXERCISE
  Lemma add_S :
    ∀ n m,
      add n (S m) = S (add n m).
  Proof.
    intros n m. induction n as [| n ih].
    - reflexivity.
    - simpl. rewrite ih. reflexivity.
  Qed.

With the following commands we declare notations for add and sub.
  Infix "+" := add.
  Infix "-" := sub.

EXERCISE
We can solve this one by using the lemmas add_0 and add_S above. It is also possible to do it by induction on n which might feel more natural. But is actually much worse so we'll spare you the details.
  Lemma add_sub :
    ∀ n m,
      (n + m) - m = n.
  Proof.
    intros n m. induction m as [| m ih].
    - rewrite add_0. destruct n. all: reflexivity.
    - rewrite add_S. simpl. assumption.
  Qed.

Note the proof can look nicer if we also prove n - O = n.

  Lemma sub_O :
    ∀ n,
      n - O = n.
  Proof.
    intros n. destruct n.
    all: reflexivity.
  Qed.

  Lemma add_sub_alt :
    ∀ n m,
      (n + m) - m = n.
  Proof.
    intros n m. induction m as [| m ih].
    - rewrite add_0. apply sub_O.
    - rewrite add_S. simpl. assumption.
  Qed.

End define_nat.

EXERCISE
Define a boolean predicate deciding equality of natural numbers.
Fixpoint eq_nat (x y : nat) : bool :=
  match x, y with
  | 0, 0 ⇒ true
  | 0, S _ ⇒ false
  | S _, 0 ⇒ false
  | S x', S y' ⇒ eq_nat x' y'
  end.

EXERCISE
Lemma eq_nat_spec :
  ∀ n m,
    eq_nat n m = true ↔ n = m.
Proof.
  intros n. (* Note how we do not introduce m yet. *)
  induction n as [| n ih].
  - intros m. destruct m.
    + simpl. split. all: reflexivity.
    + simpl. split. all: discriminate.
  - intros m. destruct m.
    + simpl. split. all: discriminate.
    + simpl. split.
      × intro h. f_equal. apply ih. assumption.
      × intro h. apply ih. inversion h. reflexivity.
Qed.

EXERCISE
Definition cur {X Y Z} (f : X × Y → Z) : X → Y → Z :=
  fun x y ⇒ f (x, y).

EXERCISE
Definition car {X Y Z} (f : X → Y → Z) : X × Y → Z :=
  fun p ⇒
    match p with
    | (x, y) ⇒ f x y
    end.

Note, we can take a shortcut because there is only one constructor so we have so-called an "irrefutable pattern".
Definition car' {X Y Z} (f : X → Y → Z) : X × Y → Z :=
  fun '(x,y) ⇒ f x y.

We could also use fst and snd
Definition car'' {X Y Z} (f : X → Y → Z) : X × Y → Z :=
  fun p ⇒ f (fst p) (snd p).

EXERCISE
Lemma car_cur :
  ∀ {X Y Z} (f : X × Y → Z) p,
    car (cur f) p = f p.
Proof.
  intros X Y Z f p. destruct p.
  reflexivity.
Qed.

EXERCISE
Lemma cur_car :
  ∀ {X Y Z} (f : X → Y → Z) x y,
    cur (car f) x y = f x y.
Proof.
  reflexivity. (* No intros needed, reflexivity does it for us. *)
Qed.

EXERCISE
Definition swap {X Y} (p : X × Y) : Y × X :=
  let '(x, y) := p in (* Irrefutable patterns also work with let *)
  (y, x).

EXERCISE
Lemma swap_invol :
  ∀ {X Y} (p : X × Y),
    swap (swap p) = p.
Proof.
  intros X Y p.
  destruct p.
  reflexivity.
Qed.

EXERCISE
Prove true ≠ false without the tactics inversion or discriminate.
Note: a ≠ b is a notation for a ≠ b, meaning a = b → False.
Lemma true_false :
  true ≠ false.
Proof.
  intro e.
  change (if true then False else True).
  rewrite e.
  constructor.
Qed.

Require Import List.
Import ListNotations.

EXERCISE
We prove a few lemmas before rev_app_distr. They are part of the standard library, but it's for learning.

Lemma app_nil_r :
  ∀ A (l : list A),
    l ++ [] = l.
Proof.
  intros A l.
  induction l as [| a l ih].
  - reflexivity.
  - simpl. rewrite ih. reflexivity.
Qed.

Lemma app_assoc :
  ∀ A (u v w : list A),
    (u ++ v) ++ w = u ++ (v ++ w).
Proof.
  intros A u v w.
  induction u as [| a u ih].
  - reflexivity.
  - simpl. rewrite ih. reflexivity.
Qed.

Lemma rev_app_distr :
  ∀ {A} (l1 l2 : list A),
    rev (l1 ++ l2) = rev l2 ++ rev l1.
Proof.
  intros A l1 l2.
  induction l1 as [| a l1 ih].
  - simpl. rewrite app_nil_r. reflexivity.
  - simpl. rewrite ih. rewrite app_assoc. reflexivity.
Qed.

EXERCISE
Theorem rev_rev {X} (l : list X) :
  rev (rev l) = l.
Proof.
  induction l as [| x l ih].
  - reflexivity.
  - simpl. rewrite rev_app_distr. rewrite ih.
    simpl. reflexivity.
Qed.

Fixpoint fast_rev {A} (l : list A) (acc : list A) :=
  match l with
  | nil ⇒ acc
  | x :: l ⇒ fast_rev l (x :: acc)
  end.

EXERCISE
The idea here is to generalise the goal, we cannot prove it with nil directly. We're going to prove something stronger instead.
Lemma fast_rev_eq :
  ∀ A (l : list A),
    fast_rev l nil = rev l.
Proof.
  intros A l.
  assert (h : ∀ acc, fast_rev l acc = rev l ++ acc).
  { induction l as [| a l ih].
    - intro acc. simpl. reflexivity.
    - intro acc. simpl. rewrite ih.
      rewrite app_assoc. simpl. reflexivity.
  }
  specialize (h []).
  rewrite app_nil_r in h.
  assumption.
Qed.

Note we could have done it without the assert using generalize
Lemma fast_rev_eq_alt :
  ∀ A (l : list A),
    fast_rev l nil = rev l.
Proof.
  intros A l.
  rewrite <- app_nil_r.
  generalize (@nil A) as acc.
  induction l as [| a l ih].
  - intro acc. simpl. reflexivity.
  - intro acc. simpl. rewrite ih.
    rewrite app_assoc. simpl. reflexivity.
Qed.

Require Import Nat.

Fixpoint iter {A : Type} (f : A → A) (n : nat) (x : A) : A :=
  match n with
  | 0 ⇒ x
  | S n' ⇒ f (iter f n' x)
  end.

EXERCISE
As you can guess, x^n is a notation for x to the power of n. You can use Locate "^". to see what the notation unfold to (here pow) and then Print pow. to see the definition.
Fact iter_pow n x :
  x^n = iter (mul x) n 1.
Proof.
  induction n as [| n ih].
  - simpl. reflexivity.
  - simpl. rewrite ih. reflexivity.
Qed.

EXERCISE
Fact iter_shift :
  ∀ A (f : A → A) n x,
    iter f (S n) x = iter f n (f x).
Proof.
  intros A f n x.
  induction n as [| n ih].
  - reflexivity.
  - simpl. rewrite <- ih. reflexivity.
Qed.

Inductive le' : nat → nat → Prop :=
| leO' n : le' 0 n
| leS' n m : le' n m → le' (S n) (S m).

EXERCISE
Spell out the induction principle of le' without checking it. Notice that it's *not* the same definition as in the live coding.
⚠️⚠️⚠️⚠️⚠️⚠️⚠️⚠️⚠️⚠️⚠️⚠️⚠️⚠️⚠️⚠️⚠️⚠️⚠️ Do not forget this one.

Check le'_ind :
  ∀ (P : nat → nat → Prop),
    (∀ n, P 0 n) →
    (∀ n m, le' n m → P n m → P (S n) (S m)) →
    ∀ n m, le' n m → P n m.

EXERCISE
We require a few lemmas to prove le_equiv.

Lemma le_0_n :
  ∀ n, 0 ≤ n.
Proof.
  intro n.
  induction n as [| n ih].
  - constructor.
  - constructor. assumption.
Qed.

Lemma le_n_S :
  ∀ n m,
    n ≤ m →
    S n ≤ S m.
Proof.
  intros n m h.
  induction h.
  - constructor.
  - constructor. assumption.
Qed.

Lemma le'_refl :
  ∀ n,
    le' n n.
Proof.
  intros n.
  induction n as [| n ih].
  - constructor.
  - constructor. assumption.
Qed.

Lemma le'_n_S :
  ∀ n m,
    le' n m →
    le' n (S m).
Proof.
  intros n m h.
  induction h.
  - constructor.
  - constructor. assumption.
Qed.

Lemma le_equiv :
  ∀ n m,
    le' n m ↔ le n m.
Proof.
  intros n m.
  split.
  - intro h. induction h.
    + apply le_0_n.
    + apply le_n_S. assumption.
  - intro h. induction h.
    + apply le'_refl.
    + apply le'_n_S. assumption.
Qed.

EXERCISE
Fixpoint leb (n m : nat) : bool :=
  match n, m with
    | 0, _ ⇒ true
    | _, 0 ⇒ false
    | S n', S m' ⇒ leb n' m'
  end.

EXERCISE
We will show two ways to prove it. The first one proceeds by doing split at the earliest.
Lemma leb_spec :
  ∀ n m,
    leb n m = true ↔ le n m.
Proof.
  intros n m.
  split.
  - intro h. induction n as [| n ih] in m, h |- ×.
    (* The in clause lets us generalise over m and h, like revert *)
    + apply le_0_n.
    + simpl in h. destruct m as [| m]. 1: discriminate.
      apply le_n_S. apply ih. assumption.
  - intro h. apply le_equiv in h. induction h.
    + reflexivity.
    + simpl. assumption.
Qed.

It is also possible to delay the split and get a strong induction hypothesis which is not needed here. In this case we have to perform induction on n globally which results in a more clunky proof (since inversion is now needed).
Lemma leb_spec_alt :
  ∀ n m,
    leb n m = true ↔ le n m.
Proof.
  intros n m.
  induction n as [| n ih] in m |- ×.
  - split.
    + intro. apply le_0_n.
    + intro. simpl. reflexivity.
  - split.
    + intro h. destruct m. 1: discriminate.
      simpl in h. apply le_n_S. apply ih. assumption.
    + intro h. destruct m. 1: inversion h.
      simpl. apply ih. inversion h.
      × constructor.
      × transitivity (S n). (* We exploit transitivity of ≤ *)
        -- constructor. constructor.
        -- assumption.
Qed.

Definition even1 n :=
  ∃ m, n = 2 × m.

Fixpoint even2 (n : nat) :=
  match n with
  | 0 ⇒ true
  | 1 ⇒ false
  | S (S n) ⇒ even2 n
  end.

EXERCISE
Define an even predicate similar to how you would define a boolean predicate but using propositions instead.
Fixpoint even3 (n : nat) : Prop :=
  match n with
  | 0 ⇒ True
  | 1 ⇒ False
  | S (S n) ⇒ even3 n
  end.

Inductive even4 : nat → Prop :=
| evenO : even4 0
| evenS n : even4 n → even4 (S (S n)).

EXERCISE
Spell out the induction principle of even4 without checking it.
⚠️⚠️⚠️⚠️⚠️⚠️⚠️⚠️⚠️⚠️⚠️⚠️⚠️⚠️⚠️⚠️⚠️⚠️⚠️ Do not forget this one.

Check even4_ind :
  ∀ (P : nat → Prop),
    P 0 →
    (∀ n, even4 n → P n → P (S (S n))) →
    ∀ n, even4 n → P n.

Require Import Lia.

EXERCISE
Lemma strong_nat_ind :
  ∀ (P : nat → Prop),
    (∀ n, (∀ m, m < n → P m) → P n) →
    ∀ n, P n.
Proof.
  intros P h n.
  assert (hn : ∀ m, m ≤ n → P m).
  { induction n as [| n ih].
    - intros m hm. inversion hm.
      apply h. intros k hk. lia. (* lia knows there can't be k < 0 *)
    - intros m hm. inversion hm.
      + apply h. intros k hk. apply ih. lia.
      + apply ih. lia.
  }
  apply hn. lia.
Qed.

EXERCISE
Lemma even1_to_even2 : ∀ n, even1 n → even2 n = true.
Proof.
  intros n [m ->]. (* Short for intros n h. destruct h as [m e]. subst e. *)
  (* In fact the → means rewriting e from left to right. *)
  induction m as [| m ih].
  - simpl. reflexivity.
  - replace (2 × S m) with (S (S (2 × m))) by lia.
    (* replace a with b allows us to rewrite with an equality we have yet *)
    (* to prove between a and b *)
    (* by lia tells Coq that lia will prove said equality *)
    (* If this feels like cheating because you didn't know, you could have *)
    (* used assert and then rewrite instead. 😉 *)
    simpl. assumption.
Qed.

EXERCISE
Lemma even2_iff_even3 : ∀ n, even2 n = true ↔ even3 n.
Proof.
  intros n.
  induction n as [n ih] using strong_nat_ind.
  destruct n as [| [| n]].
  - simpl. split.
    + intro. constructor.
    + reflexivity.
  - simpl. split.
    + discriminate.
    + contradiction.
  - simpl. apply ih. lia.
Qed.

EXERCISE
Lemma even3_to_even4 : ∀ n, even3 n → even4 n.
Proof.
  intros n h.
  induction n as [n ih] using strong_nat_ind.
  destruct n as [| [| n]].
  - constructor.
  - simpl in h. contradiction.
  - constructor. apply ih.
    + lia.
    + assumption.
Qed.

EXERCISE
Lemma even4_to_even1 : ∀ n, even4 n → even1 n.
Proof.
  intros n h.
  unfold even1. (* To see what we need to prove *)
  induction h as [| n h ih].
  - ∃ 0. reflexivity.
  - destruct ih as [m ->].
    ∃ (S m). lia.
Qed.

Membership in a list
Fixpoint In {A} (x : A) (l : list A) : Prop :=
  match l with
  | nil ⇒ False
  | y :: m ⇒ y = x ∨ In x m
  end.

EXERCISE
Propose an inductive definition of membership (add the missing constructor(s)).
Inductive In_i {A} : A → list A → Prop :=
| in_hd x l : In_i x (x :: l)
| in_tl x y l : In_i x l → In_i x (y :: l).

EXERCISE
Lemma In_iff :
  ∀ A (x : A) l,
    In x l ↔ In_i x l.
Proof.
  intros A x l.
  split.
  - intros h. induction l as [| a l ih].
    + simpl in h. contradiction.
    + simpl in h. destruct h as [-> | h].
      × constructor.
      × constructor. apply ih. assumption.
  - intros h. induction h.
    + simpl. left. reflexivity.
    + simpl. right. assumption.
Qed.

ADVANCED EXERCISES
Make sure you manage to do the previous exercices before. Do not hesitate to ask for help.
EXERCISE
Define the factorial function in two ways:
  • once using Fixpoint
  • and once using iter
Prove that both yield the same value for all arguments.

Fixpoint fact_fix n :=
  match n with
  | 0 ⇒ 1
  | S n ⇒ S n × fact_fix n
  end.

Definition fact_iter_f '(i,x) :=
  (S i, S i × x).

Definition fact_iter n :=
  snd (iter fact_iter_f n (0,1)).

Lemma fact_equiv :
  ∀ n,
    fact_fix n = fact_iter n.
Proof.
  intros n.
  unfold fact_iter.
  assert (h : (n, fact_fix n) = iter fact_iter_f n (0,1)).
  { induction n as [| n ih].
    - simpl. reflexivity.
    - simpl. rewrite <- ih. simpl. reflexivity.
  }
  apply (f_equal snd) in h. assumption.
Qed.

Module Fib_Iter.

EXERCISE
Define the Fibonnaci function, using only iter (no recursive definition). As a reminder fib 0 = 0, fib 1 = 1 and fib (n+2) = fib (n+1) + fib n.
  Definition sigma c :=
    (snd c, fst c + snd c).

  Definition fib (n : nat) : nat :=
    fst (iter sigma n (0, 1)).

EXERCISE
  Lemma fib_eq0 :
    fib 0 = 0.
  Proof.
    reflexivity.
  Qed.

EXERCISE
  Lemma fib_eq1 :
    fib 1 = 1.
  Proof.
    reflexivity.
  Qed.

EXERCISE
  Lemma fib_eq3 :
    ∀ n,
      fib (S (S n)) = fib n + fib (S n).
  Proof.
    reflexivity.
  Qed.

End Fib_Iter.

Inductive rtclos {A} (R : A → A → Prop) : A → A → Prop :=
| refl x : rtclos R x x
| incl x y : R x y → rtclos R x y
| trans x y z : rtclos R x y → rtclos R y z → rtclos R x z.

Inductive rtclos' {A} (R : A → A → Prop) : A → A → Prop :=
| refl' x : rtclos' R x x
| trans' x y z : R x y → rtclos' R y z → rtclos' R x z.

EXERCISE
Lemma rtclos'_trans :
  ∀ A (R : A → A → Prop) x y z,
    rtclos' R x y →
    rtclos' R y z →
    rtclos' R x z.
Proof.
  intros A R x y z hxy hyz.
  induction hxy as [x | x y w h1 h2 ih].
  - assumption.
  - apply trans' with y. (* The with keyword is to give the argument it can't guess *)
    + assumption.
    + apply ih. assumption.
Qed.

EXERCISE
Lemma rtclos_iff :
  ∀ A (R : A → A → Prop) x y,
    rtclos R x y ↔ rtclos' R x y.
Proof.
  intros A R x y.
  split.
  - intros h. induction h.
    + constructor.
    + apply trans' with y.
      × assumption.
      × constructor.
    + apply rtclos'_trans with y. all: assumption.
  - induction 1. (* To introduce the first argument and induct on it *)
    + constructor.
    + apply trans with y.
      × constructor. assumption.
      × assumption.
Qed.

Implementation of the Cantor pairing and its inverse function
We build a bijection between nat * nat and nat.

Require Import PeanoNat.

Cantor pairing to_nat

Fixpoint to_nat' n :=
  match n with
  | 0 ⇒ 0
  | S i ⇒ S i + to_nat' i
  end.

Note the following notation '(x,y) is performing pattern matching implicitly.
Definition to_nat '(x, y) : nat :=
  y + to_nat' (y + x).

Cantor pairing inverse of_nat

Fixpoint of_nat (n : nat) : nat × nat :=
  match n with
  | 0 ⇒ (0,0)
  | S i ⇒
    let '(x,y) := of_nat i in
    match x with
    | 0 ⇒ (S y, 0)
    | S x ⇒ (x, S y)
    end
  end.

EXERCISE
Show that of_nat is a left inverse for to_nat.
Lemma cancel_of_to :
  ∀ p,
    of_nat (to_nat p) = p.
Proof.
  assert (H : ∀ n p, to_nat p = n → of_nat n = p).
  { intros n p h.
    induction n as [| n ih] in p, h |- ×.
    - simpl. destruct p as [x y].
      simpl in h. destruct y as [| y]. 2: discriminate.
      simpl in h. destruct x as [| x]. 2: discriminate.
      reflexivity.
    - destruct p as [x y].
      simpl in h. destruct y as [| y].
      + simpl in h.
        destruct x as [| x]. 1: discriminate.
        simpl in ×. rewrite (ih (0,x)).
        × reflexivity.
        × simpl. replace (x + 0) with x by lia. lia.
      + simpl in ×. rewrite (ih (S x, y)).
        × reflexivity.
        × simpl. replace (y + S x) with (S y + x) by lia.
          simpl. lia.
  }
  intros p. apply H. reflexivity.
Qed.

EXERCISE
Show to_nat is injective.
Corollary to_nat_inj :
  ∀ p q,
    to_nat p = to_nat q →
    p = q.
Proof.
  intros p q e.
  apply (f_equal of_nat) in e.
  rewrite 2!cancel_of_to in e. (* 2! means do the rewrite twice *)
  assumption.
Qed.

EXERCISE
Show to_nat is a left inverse for of_nat.
Lemma cancel_to_of :
  ∀ n,
    to_nat (of_nat n) = n.
Proof.
  intros n. induction n as [| n ih].
  - reflexivity.
  - simpl. destruct (of_nat n) as [x y].
    destruct x as [| x].
    + simpl in ×. replace (y + 0) with y in ih by lia. lia.
    + simpl in ×. replace (y + S x) with (S y + x) in ih by lia.
      simpl in ih. lia.
Qed.

EXERCISE
Show of_nat is injective.
Corollary of_nat_inj :
  ∀ n m,
    of_nat n = of_nat m →
    n = m.
Proof.
  intros n m e%(f_equal to_nat). (* This notation applies f_equal to_nat to e *)
  rewrite 2!cancel_to_of in e.
  assumption.
Qed.

Church encodings
It is possible to encode natural numbers (and other data types) using so-called Church encodings that you might have seen in a λ-calculus class. Below, num is the definition of Church numerals.

Definition num :=
  ∀ (X : Prop) (s : X → X) (z : X), X.

Definition zero : num :=
  fun X s z ⇒ z.

Definition succ : num → num :=
  fun n X s z ⇒ s (n X s z).

Fixpoint from_nat n : num :=
  match n with
  | 0 ⇒ zero
  | S n ⇒ succ (from_nat n)
  end.

Definition add : num → num → num :=
  fun n m X s z ⇒ n X s (m X s z).

Compute (add (from_nat 3) (from_nat 2)).

EXERCISE
Lemma add_from_nat :
  ∀ n m,
    add (from_nat n) (from_nat m) = from_nat (n + m).
Proof.
  intros n m.
  induction n as [| n ih].
  - reflexivity.
  - simpl. rewrite <- ih. reflexivity.
Qed.

EXERCISE
Definition mul : num → num → num :=
  fun n m X s z ⇒ n X (m X s) z.

EXERCISE
Lemma mul_from_nat :
  ∀ n m,
    mul (from_nat n) (from_nat m) = from_nat (n × m).
Proof.
  intros n m.
  induction n as [| n ih].
  - simpl. reflexivity.
  - simpl. rewrite <- add_from_nat. rewrite <- ih. reflexivity.
Qed.

EXERCISE
Define the power function (check out the next exercise to make sure you see what it should give).
Definition exp : num → num → num :=
  fun n m X ⇒ m _ (n X).

EXERCISE
Lemma exp_from_nat n m :
  exp (from_nat n) (from_nat m) = from_nat (n ^ m).
Proof.
  induction m as [| m ih].
  - reflexivity.
  - simpl. rewrite <- mul_from_nat. rewrite <- ih. reflexivity.
Qed.

EXERCISE
Define a predecessor function.
Definition pred' : num → num ∧ num :=
  fun n ⇒ n (num ∧ num) (fun '(conj a b) ⇒ conj b (succ b)) (conj zero zero).

Definition pred : num → num :=
  fun n ⇒
    let '(conj p _) := pred' n in
    p.

EXERCISE

Lemma pred'_from_nat n :
  pred' (from_nat n) = conj (from_nat (Nat.pred n)) (from_nat n).
Proof.
  induction n as [| n ih].
  - reflexivity.
  - simpl. unfold pred' in ×.
    unfold succ at 1. rewrite ih. reflexivity.
Qed.

Lemma pred_from_nat n :
  pred (from_nat n) = from_nat (Nat.pred n).
Proof.
  unfold pred.
  rewrite pred'_from_nat.
  reflexivity.
Qed.