Exercise session 2 — Part 1

🏠 Go back to the course homepage.

Module define_nat.Interactive Module define_nat started

Inductive types can be defined using the Inductive keyword

  Inductive nat :=
  | O : nat
  | S : nat -> nat.nat is defined
nat_rect is defined
nat_ind is defined
nat_rec is defined
nat_sind is defined

EXERCISE

Define addition.

  Fixpoint add (n m : nat) {struct n} : nat :=
    match n with
    | O => m
    | S n => S (add n m)
    end.add is defined
add is recursively defined (guarded on 1st argument)

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.sub is defined
sub is recursively defined (guarded on 1st argument)

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 :
    forall n,
      add n O = n.forall n : nat, add n O = n
  Proof.forall n : nat, add n O = n
    intros n.n: nat
add n O = n induction n as [| n ih].add O O = O
n: nat
ih: add n O = n
add (S n) O = S n
    -add O O = O reflexivity.
    -n: nat
ih: add n O = n
add (S n) O = S n simpl.n: nat
ih: add n O = n
S (add n O) = S n rewrite ih.n: nat
ih: add n O = n
S n = S n reflexivity.
  Qed.add_0 is defined

EXERCISE

  Lemma add_S :
    forall n m,
      add n (S m) = S (add n m).forall n m : nat, add n (S m) = S (add n m)
  Proof.forall n m : nat, add n (S m) = S (add n m)
    intros n m.n, m: nat
add n (S m) = S (add n m) induction n as [| n ih].m: nat
add O (S m) = S (add O m)
n, m: nat
ih: add n (S m) = S (add n m)
add (S n) (S m) = S (add (S n) m)
    -m: nat
add O (S m) = S (add O m) reflexivity.
    -n, m: nat
ih: add n (S m) = S (add n m)
add (S n) (S m) = S (add (S n) m) simpl.n, m: nat
ih: add n (S m) = S (add n m)
S (add n (S m)) = S (S (add n m)) rewrite ih.n, m: nat
ih: add n (S m) = S (add n m)
S (S (add n m)) = S (S (add n m)) reflexivity.
  Qed.add_S is defined

With the following commands we declare notations for add and sub.

  Infix "+" := add.
  Infix "-" := sub.

EXERCISE

  Lemma add_sub :
    forall n m,
      (n + m) - m = n.forall n m : nat, n + m - m = n
  Proof.forall n m : nat, n + m - m = n
    intros n m.n, m: nat
n + m - m = n induction m as [| m ih].n: nat
n + O - O = n
n, m: nat
ih: n + m - m = n
n + S m - S m = n
    -n: nat
n + O - O = n rewrite add_0.n: nat
n - O = n destruct n.O - O = O
n: nat
S n - O = S n all: reflexivity.
    -n, m: nat
ih: n + m - m = n
n + S m - S m = n rewrite add_S.n, m: nat
ih: n + m - m = n
S (n + m) - S m = n simpl.n, m: nat
ih: n + m - m = n
n + m - m = n assumption.
  Qed.add_sub is defined

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

  Lemma sub_O :
    forall n,
      n - O = n.forall n : nat, n - O = n
  Proof.forall n : nat, n - O = n
    intros n.n: nat
n - O = n destruct n.O - O = O
n: nat
S n - O = S n
    all: reflexivity.
  Qed.sub_O is defined

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

End define_nat.Module define_nat is defined

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.eq_nat is defined
eq_nat is recursively defined (guarded on 1st argument)

EXERCISE

Lemma eq_nat_spec :
  forall n m,
    eq_nat n m = true <-> n = m.forall n m : nat, eq_nat n m = true <-> n = m
Proof.forall n m : nat, eq_nat n m = true <-> n = m
  intros n m.n, m: nat
eq_nat n m = true <-> n = m
  induction n as [| n ih] in m |- *.m: nat
eq_nat 0 m = true <-> 0 = m
n, m: nat
ih:= forall m: nat, eq_nat n m = true <-> n = m
eq_nat (S n) m = true <-> S n = m
  -m: nat
eq_nat 0 m = true <-> 0 = m destruct m.eq_nat 0 0 = true <-> 0 = 0
m: nat
eq_nat 0 (S m) = true <-> 0 = S m
    +eq_nat 0 0 = true <-> 0 = 0 simpl.true = true <-> 0 = 0 split.true = true -> 0 = 0
0 = 0 -> true = true all: reflexivity.
    +m: nat
eq_nat 0 (S m) = true <-> 0 = S m simpl.m: nat
false = true <-> 0 = S m split.m: nat
false = true -> 0 = S m
m: nat
0 = S m -> false = true all: discriminate.
  -n, m: nat
ih:= forall m: nat, eq_nat n m = true <-> n = m
eq_nat (S n) m = true <-> S n = m destruct m.n: nat
ih:= forall m: nat, eq_nat n m = true <-> n = m
eq_nat (S n) 0 = true <-> S n = 0
n, m: nat
ih:= forall m: nat, eq_nat n m = true <-> n = m
eq_nat (S n) (S m) = true <-> S n = S m
    +n: nat
ih:= forall m: nat, eq_nat n m = true <-> n = m
eq_nat (S n) 0 = true <-> S n = 0 simpl.n: nat
ih:= forall m: nat, eq_nat n m = true <-> n = m
false = true <-> S n = 0 split.n: nat
ih:= forall m: nat, eq_nat n m = true <-> n = m
false = true -> S n = 0
n: nat
ih:= forall m: nat, eq_nat n m = true <-> n = m
S n = 0 -> false = true all: discriminate.
    +n, m: nat
ih:= forall m: nat, eq_nat n m = true <-> n = m
eq_nat (S n) (S m) = true <-> S n = S m simpl.n, m: nat
ih:= forall m: nat, eq_nat n m = true <-> n = m
eq_nat n m = true <-> S n = S m split.n, m: nat
ih:= forall m: nat, eq_nat n m = true <-> n = m
eq_nat n m = true -> S n = S m
n, m: nat
ih:= forall m: nat, eq_nat n m = true <-> n = m
S n = S m -> eq_nat n m = true
      *n, m: nat
ih:= forall m: nat, eq_nat n m = true <-> n = m
eq_nat n m = true -> S n = S m intro h.n, m: nat
ih:= forall m: nat, eq_nat n m = true <-> n = m
h: eq_nat n m = true
S n = S m f_equal.n, m: nat
ih:= forall m: nat, eq_nat n m = true <-> n = m
h: eq_nat n m = true
n = m apply ih.n, m: nat
ih:= forall m: nat, eq_nat n m = true <-> n = m
h: eq_nat n m = true
eq_nat n m = true assumption.
      *n, m: nat
ih:= forall m: nat, eq_nat n m = true <-> n = m
S n = S m -> eq_nat n m = true intro h.n, m: nat
ih:= forall m: nat, eq_nat n m = true <-> n = m
h: S n = S m
eq_nat n m = true apply ih.n, m: nat
ih:= forall m: nat, eq_nat n m = true <-> n = m
h: S n = S m
n = m inversion h.n, m: nat
ih:= forall m: nat, eq_nat n m = true <-> n = m
h: S n = S m
H0: n = m
m = m reflexivity.
Qed.eq_nat_spec is defined

EXERCISE

Definition cur {X Y Z} (f : X * Y -> Z) : X -> Y -> Z :=
  fun x y => f (x, y).cur is defined

EXERCISE

Definition car {X Y Z} (f : X -> Y -> Z) : X * Y -> Z :=
  fun p =>
    match p with
    | (x, y) => f x y
    end.car is defined

Note, we can take a shortcut because there is only one constructor so we have a so-called "irrefutable pattern".

Definition car' {X Y Z} (f : X -> Y -> Z) : X * Y -> Z :=
  fun '(x,y) => f x y.car' is defined

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).car'' is defined

EXERCISE

Lemma car_cur :
  forall {X Y Z} (f : X * Y -> Z) p,
    car (cur f) p = f p.forall (X Y Z : Type) (f : X * Y -> Z) (p : X * Y), car (cur f) p = f p
Proof.forall (X Y Z : Type) (f : X * Y -> Z) (p : X * Y), car (cur f) p = f p
  intros X Y Z f p.X, Y, Z: Type
f: X * Y -> Z
p: X * Y
car (cur f) p = f p destruct p.X, Y, Z: Type
f: X * Y -> Z
x: X
y: Y
car (cur f) (x, y) = f (x, y)
  reflexivity.
Qed.car_cur is defined

EXERCISE

Lemma cur_car :
  forall {X Y Z} (f : X -> Y -> Z) x y,
    cur (car f) x y = f x y.forall (X Y Z : Type) (f : X -> Y -> Z) (x : X) (y : Y), cur (car f) x y = f x y
Proof.forall (X Y Z : Type) (f : X -> Y -> Z) (x : X) (y : Y), cur (car f) x y = f x y

No intros needed, reflexivity does it for us.

  reflexivity.
Qed.cur_car is defined

EXERCISE

Definition swap {X Y} (p : X * Y) : Y * X :=

Irrefutable patterns also work with let.

  let '(x, y) := p in
  (y, x).swap is defined

EXERCISE

Lemma swap_invol :
  forall {X Y} (p : X * Y),
    swap (swap p) = p.forall (X Y : Type) (p : X * Y), swap (swap p) = p
Proof.forall (X Y : Type) (p : X * Y), swap (swap p) = p
  intros X Y p.X, Y: Type
p: X * Y
swap (swap p) = p
  destruct p.X, Y: Type
x: X
y: Y
swap (swap (x, y)) = (x, y)
  reflexivity.
Qed.swap_invol is defined

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.true <> false
Proof.true <> false
  intro e.e: true = false
False
  change (if true then False else True).e: true = false
if true then False else True
  rewrite e.e: true = false
True
  constructor.
Qed.true_false is defined

From Stdlib Require Import List.
Import ListNotations.

EXERCISE

Prove the following. You will need lemmas, prove them yourself by induction and do not use lemmas from the standard library.

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

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

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

EXERCISE

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

Fixpoint fast_rev {A} (l : list A) (acc : list A) :=
  match l with
  | nil => acc
  | x :: l => fast_rev l (x :: acc)
  end.fast_rev is defined
fast_rev is recursively defined (guarded on 2nd argument)

EXERCISE

Lemma fast_rev_eq :
  forall A (l : list A),
    fast_rev l nil = rev l.forall (A : Type) (l : list A), fast_rev l [] = rev l
Proof.forall (A : Type) (l : list A), fast_rev l [] = rev l
  intros A l.A: Type
l: list A
fast_rev l [] = rev l
  assert (h : forall acc, fast_rev l acc = rev l ++ acc).A: Type
l: list A
forall acc : list A, fast_rev l acc = rev l ++ acc
A: Type
l: list A
h:= forall acc: list A, fast_rev l acc = rev l ++ acc
fast_rev l [] = rev l
  {A: Type
l: list A
forall acc : list A, fast_rev l acc = rev l ++ acc induction l as [| a l ih].A: Type
forall acc : list A, fast_rev [] acc = rev [] ++ acc
A: Type
a: A
l: list A
ih:= forall acc: list A, fast_rev l acc = rev l ++ acc
forall acc : list A, fast_rev (a :: l) acc = rev (a :: l) ++ acc
    -A: Type
forall acc : list A, fast_rev [] acc = rev [] ++ acc intro acc.A: Type
acc: list A
fast_rev [] acc = rev [] ++ acc simpl.A: Type
acc: list A
acc = acc reflexivity.
    -A: Type
a: A
l: list A
ih:= forall acc: list A, fast_rev l acc = rev l ++ acc
forall acc : list A, fast_rev (a :: l) acc = rev (a :: l) ++ acc intro acc.A: Type
a: A
l: list A
ih:= forall acc: list A, fast_rev l acc = rev l ++ acc
acc: list A
fast_rev (a :: l) acc = rev (a :: l) ++ acc simpl.A: Type
a: A
l: list A
ih:= forall acc: list A, fast_rev l acc = rev l ++ acc
acc: list A
fast_rev l (a :: acc) = (rev l ++ [a]) ++ acc rewrite ih.A: Type
a: A
l: list A
ih:= forall acc: list A, fast_rev l acc = rev l ++ acc
acc: list A
rev l ++ a :: acc = (rev l ++ [a]) ++ acc
      rewrite app_assoc.A: Type
a: A
l: list A
ih:= forall acc: list A, fast_rev l acc = rev l ++ acc
acc: list A
rev l ++ a :: acc = rev l ++ [a] ++ acc simpl.A: Type
a: A
l: list A
ih:= forall acc: list A, fast_rev l acc = rev l ++ acc
acc: list A
rev l ++ a :: acc = rev l ++ a :: acc reflexivity.
  }A: Type
l: list A
h:= forall acc: list A, fast_rev l acc = rev l ++ acc
fast_rev l [] = rev l
  specialize (h []).A: Type
l: list A
h: fast_rev l [] = rev l ++ []
fast_rev l [] = rev l
  rewrite app_nil_r in h.A: Type
l: list A
h: fast_rev l [] = rev l
fast_rev l [] = rev l
  assumption.
Qed.fast_rev_eq is defined

Note we could have done it without the assert using generalize.

Lemma fast_rev_eq_alt :
  forall A (l : list A),
    fast_rev l nil = rev l.forall (A : Type) (l : list A), fast_rev l [] = rev l
Proof.forall (A : Type) (l : list A), fast_rev l [] = rev l
  intros A l.A: Type
l: list A
fast_rev l [] = rev l
  rewrite <- app_nil_r.A: Type
l: list A
fast_rev l [] = rev l ++ []
  generalize (@nil A) as acc.A: Type
l: list A
forall acc : list A, fast_rev l acc = rev l ++ acc
  induction l as [| a l ih].A: Type
forall acc : list A, fast_rev [] acc = rev [] ++ acc
A: Type
a: A
l: list A
ih:= forall acc: list A, fast_rev l acc = rev l ++ acc
forall acc : list A, fast_rev (a :: l) acc = rev (a :: l) ++ acc
  -A: Type
forall acc : list A, fast_rev [] acc = rev [] ++ acc intro acc.A: Type
acc: list A
fast_rev [] acc = rev [] ++ acc simpl.A: Type
acc: list A
acc = acc reflexivity.
  -A: Type
a: A
l: list A
ih:= forall acc: list A, fast_rev l acc = rev l ++ acc
forall acc : list A, fast_rev (a :: l) acc = rev (a :: l) ++ acc intro acc.A: Type
a: A
l: list A
ih:= forall acc: list A, fast_rev l acc = rev l ++ acc
acc: list A
fast_rev (a :: l) acc = rev (a :: l) ++ acc simpl.A: Type
a: A
l: list A
ih:= forall acc: list A, fast_rev l acc = rev l ++ acc
acc: list A
fast_rev l (a :: acc) = (rev l ++ [a]) ++ acc rewrite ih.A: Type
a: A
l: list A
ih:= forall acc: list A, fast_rev l acc = rev l ++ acc
acc: list A
rev l ++ a :: acc = (rev l ++ [a]) ++ acc
    rewrite app_assoc.A: Type
a: A
l: list A
ih:= forall acc: list A, fast_rev l acc = rev l ++ acc
acc: list A
rev l ++ a :: acc = rev l ++ [a] ++ acc simpl.A: Type
a: A
l: list A
ih:= forall acc: list A, fast_rev l acc = rev l ++ acc
acc: list A
rev l ++ a :: acc = rev l ++ a :: acc reflexivity.
Qed.fast_rev_eq_alt is defined