Exercise session 1 — Part 2 — Inductive types

Authors:

Yannick Forster

Théo Winterhalter

Files:

Display all goals and responses

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

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.

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.

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.

  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.

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

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 a so-called "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 :
  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.

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.

EXERCISE

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

Irrefutable patterns also work with let.

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

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.

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.