Exercise session 2 — Part 2

🏠 Go back to the course homepage.

Set Default Goal Selector "!".

Axiom REPLACE_ME : forall {A : Type}, A.REPLACE_ME is declared

From Stdlib Require Import Nat List.
Import ListNotations.

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.iter is defined
iter is recursively defined (guarded on 3rd argument)

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.n, x: nat
x ^ n = iter (mul x) n 1
Proof.n, x: nat
x ^ n = iter (mul x) n 1
  induction n as [| n ih].x: nat
x ^ 0 = iter (mul x) 0 1
n, x: nat
ih: x ^ n = iter (mul x) n 1
x ^ S n = iter (mul x) (S n) 1
  -x: nat
x ^ 0 = iter (mul x) 0 1 simpl.x: nat
1 = 1 reflexivity.
  -n, x: nat
ih: x ^ n = iter (mul x) n 1
x ^ S n = iter (mul x) (S n) 1 simpl.n, x: nat
ih: x ^ n = iter (mul x) n 1
x * x ^ n = x * iter (mul x) n 1 rewrite ih.n, x: nat
ih: x ^ n = iter (mul x) n 1
x * iter (mul x) n 1 = x * iter (mul x) n 1 reflexivity.
Qed.iter_pow is defined

EXERCISE

Hint: The rewrite tactic can be used to rewrite an equality in the opposite direction using rewrite <- e. When e : u = v, it will replace v in the goal by u.

Fact iter_shift A (f : A -> A) n x :
  iter f (S n) x = iter f n (f x).A: Type
f: A -> A
n: nat
x: A
iter f (S n) x = iter f n (f x)
Proof.A: Type
f: A -> A
n: nat
x: A
iter f (S n) x = iter f n (f x)
  induction n as [| n ih].A: Type
f: A -> A
x: A
iter f 1 x = iter f 0 (f x)
A: Type
f: A -> A
n: nat
x: A
ih: iter f (S n) x = iter f n (f x)
iter f (S (S n)) x = iter f (S n) (f x)
  -A: Type
f: A -> A
x: A
iter f 1 x = iter f 0 (f x) reflexivity.
  -A: Type
f: A -> A
n: nat
x: A
ih: iter f (S n) x = iter f n (f x)
iter f (S (S n)) x = iter f (S n) (f x) simpl.A: Type
f: A -> A
n: nat
x: A
ih: iter f (S n) x = iter f n (f x)
f (f (iter f n x)) = f (iter f n (f x)) rewrite <- ih.A: Type
f: A -> A
n: nat
x: A
ih: iter f (S n) x = iter f n (f x)
f (f (iter f n x)) = f (iter f (S n) x) reflexivity.
Qed.iter_shift is defined

Inductive le' : nat -> nat -> Prop :=
| leO' n : le' 0 n
| leS' n m : le' n m -> le' (S n) (S m).le' is defined
le'_ind is defined
le'_sind is defined

EXERCISE

Spell out the induction principle of le' without checking it. Notice that it's not the same definition as in the live coding.

Check le'_ind :
  forall (P : nat -> nat -> Prop),
    (forall n, P 0 n) ->
    (forall n m, le' n m -> P n m -> P (S n) (S m)) ->
    forall n m, le' n m -> P n m.le'_ind : forall P : nat -> nat -> Prop, (forall n : nat, P 0 n) -> (forall n m : nat, le' n m -> P n m -> P (S n) (S m)) -> forall n m : nat, le' n m -> P n m
     : forall P : nat -> nat -> Prop, (forall n : nat, P 0 n) -> (forall n m : nat, le' n m -> P n m -> P (S n) (S m)) -> forall n m : nat, le' n m -> P n m

EXERCISE

Prove the following and lemmas that you need by induction. Do not use the standard library or lia!

Lemma le_0_n :
  forall n, 0 <= n.forall n : nat, 0 <= n
Proof.forall n : nat, 0 <= n
  intro n.n: nat
0 <= n
  induction n as [| n ih].0 <= 0
n: nat
ih: 0 <= n
0 <= S n
  -0 <= 0 constructor.
  -n: nat
ih: 0 <= n
0 <= S n constructor.n: nat
ih: 0 <= n
0 <= n assumption.
Qed.le_0_n is defined

Lemma le_n_S :
  forall n m,
    n <= m ->
    S n <= S m.forall n m : nat, n <= m -> S n <= S m
Proof.forall n m : nat, n <= m -> S n <= S m
  intros n m h.n, m: nat
h: n <= m
S n <= S m
  induction h.n: nat
S n <= S n
n, m: nat
h: n <= m
IHh: S n <= S m
S n <= S (S m)
  -n: nat
S n <= S n constructor.
  -n, m: nat
h: n <= m
IHh: S n <= S m
S n <= S (S m) constructor.n, m: nat
h: n <= m
IHh: S n <= S m
S n <= S m assumption.
Qed.le_n_S is defined

Lemma le'_refl :
  forall n,
    le' n n.forall n : nat, le' n n
Proof.forall n : nat, le' n n
  intros n.n: nat
le' n n
  induction n as [| n ih].le' 0 0
n: nat
ih: le' n n
le' (S n) (S n)
  -le' 0 0 constructor.
  -n: nat
ih: le' n n
le' (S n) (S n) constructor.n: nat
ih: le' n n
le' n n assumption.
Qed.le'_refl is defined

Lemma le'_n_S :
  forall n m,
    le' n m ->
    le' n (S m).forall n m : nat, le' n m -> le' n (S m)
Proof.forall n m : nat, le' n m -> le' n (S m)
  intros n m h.n, m: nat
h: le' n m
le' n (S m)
  induction h.n: nat
le' 0 (S n)
n, m: nat
h: le' n m
IHh: le' n (S m)
le' (S n) (S (S m))
  -n: nat
le' 0 (S n) constructor.
  -n, m: nat
h: le' n m
IHh: le' n (S m)
le' (S n) (S (S m)) constructor.n, m: nat
h: le' n m
IHh: le' n (S m)
le' n (S m) assumption.
Qed.le'_n_S is defined

Lemma le_equiv n m :
  le' n m <-> le n m.n, m: nat
le' n m <-> n <= m
Proof.n, m: nat
le' n m <-> n <= m
  split.n, m: nat
le' n m -> n <= m
n, m: nat
n <= m -> le' n m
  -n, m: nat
le' n m -> n <= m intro h.n, m: nat
h: le' n m
n <= m induction h.n: nat
0 <= n
n, m: nat
h: le' n m
IHh: n <= m
S n <= S m
    +n: nat
0 <= n apply le_0_n.
    +n, m: nat
h: le' n m
IHh: n <= m
S n <= S m apply le_n_S.n, m: nat
h: le' n m
IHh: n <= m
n <= m assumption.
  -n, m: nat
n <= m -> le' n m intro h.n, m: nat
h: n <= m
le' n m induction h.n: nat
le' n n
n, m: nat
h: n <= m
IHh: le' n m
le' n (S m)
    +n: nat
le' n n apply le'_refl.
    +n, m: nat
h: n <= m
IHh: le' n m
le' n (S m) apply le'_n_S.n, m: nat
h: n <= m
IHh: le' n m
le' n m assumption.
Qed.le_equiv is defined

EXERCISE

Fixpoint leb (n m : nat) : bool :=
  match n, m with
  | 0, _ => true
  | _, 0 => false
  | S n', S m' => leb n' m'
  end.leb is defined
leb is recursively defined (guarded on 1st argument)

EXERCISE

Lemma leb_spec n m :
  leb n m = true <-> le n m.n, m: nat
leb n m = true <-> n <= m
Proof.n, m: nat
leb n m = true <-> n <= m
  split.n, m: nat
leb n m = true -> n <= m
n, m: nat
n <= m -> leb n m = true
  -n, m: nat
leb n m = true -> n <= m intro h.n, m: nat
h: leb n m = true
n <= m induction n as [| n ih] in m, h |- *.m: nat
h: leb 0 m = true
0 <= m
n, m: nat
h: leb (S n) m = true
ih:= forall m: nat, leb n m = true -> n <= m
S n <= m
    +m: nat
h: leb 0 m = true
0 <= m apply le_0_n.
    +n, m: nat
h: leb (S n) m = true
ih:= forall m: nat, leb n m = true -> n <= m
S n <= m simpl in h.n, m: nat
h: match m with | 0 => false | S m' => leb n m' end = true
ih:= forall m: nat, leb n m = true -> n <= m
S n <= m destruct m as [| m].n: nat
h: false = true
ih:= forall m: nat, leb n m = true -> n <= m
S n <= 0
n, m: nat
h: leb n m = true
ih:= forall m: nat, leb n m = true -> n <= m
S n <= S m 1: discriminate.n, m: nat
h: leb n m = true
ih:= forall m: nat, leb n m = true -> n <= m
S n <= S m
      apply le_n_S.n, m: nat
h: leb n m = true
ih:= forall m: nat, leb n m = true -> n <= m
n <= m apply ih.n, m: nat
h: leb n m = true
ih:= forall m: nat, leb n m = true -> n <= m
leb n m = true assumption.
  -n, m: nat
n <= m -> leb n m = true intro h.n, m: nat
h: n <= m
leb n m = true apply le_equiv in h.n, m: nat
h: le' n m
leb n m = true induction h.n: nat
leb 0 n = true
n, m: nat
h: le' n m
IHh: leb n m = true
leb (S n) (S m) = true
    +n: nat
leb 0 n = true reflexivity.
    +n, m: nat
h: le' n m
IHh: leb n m = true
leb (S n) (S m) = true simpl.n, m: nat
h: le' n m
IHh: leb n m = true
leb n m = true assumption.
Qed.leb_spec is defined

Definition even1 n :=
  exists m, n = 2 * m.even1 is defined

Fixpoint even2 (n : nat) :=
  match n with
  | 0 => true
  | 1 => false
  | S (S n) => even2 n
  end.even2 is defined
even2 is recursively defined (guarded on 1st argument)

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

Inductive even4 : nat -> Prop :=
| evenO : even4 0
| evenS n : even4 n -> even4 (S (S n)).even4 is defined
even4_ind is defined
even4_sind is defined

EXERCISE

Spell out the induction principle of even4 without checking it.

Check even4_ind :
  forall (P : nat -> Prop),
    P 0 ->
    (forall n, even4 n -> P n -> P (S (S n))) ->
    forall n, even4 n -> P n.even4_ind : forall P : nat -> Prop, P 0 -> (forall n : nat, even4 n -> P n -> P (S (S n))) -> forall n : nat, even4 n -> P n
     : forall P : nat -> Prop, P 0 -> (forall n : nat, even4 n -> P n -> P (S (S n))) -> forall n : nat, even4 n -> P n

We now allow you to use lia.

Require Import Lia.

EXERCISE

Lemma strong_nat_ind :
  forall (P : nat -> Prop),
    (forall n, (forall m, m < n -> P m) -> P n) ->
    forall n, P n.forall P : nat -> Prop, (forall n : nat, (forall m : nat, m < n -> P m) -> P n) -> forall n : nat, P n
Proof.forall P : nat -> Prop, (forall n : nat, (forall m : nat, m < n -> P m) -> P n) -> forall n : nat, P n
  intros P h n.P: nat -> Prop
h:= forall n : nat, (forall m: nat, m < n -> P m) -> P n
n: nat
P n
  assert (hn : forall m, m <= n -> P m).P: nat -> Prop
h:= forall n : nat, (forall m: nat, m < n -> P m) -> P n
n: nat
forall m : nat, m <= n -> P m
P: nat -> Prop
h:= forall n : nat, (forall m: nat, m < n -> P m) -> P n
n: nat
hn:= forall m: nat, m <= n -> P m
P n
  {P: nat -> Prop
h:= forall n : nat, (forall m: nat, m < n -> P m) -> P n
n: nat
forall m : nat, m <= n -> P m induction n as [| n ih].P: nat -> Prop
h:= forall n : nat, (forall m: nat, m < n -> P m) -> P n
forall m : nat, m <= 0 -> P m
P: nat -> Prop
h:= forall n : nat, (forall m: nat, m < n -> P m) -> P n
n: nat
ih:= forall m: nat, m <= n -> P m
forall m : nat, m <= S n -> P m
    -P: nat -> Prop
h:= forall n : nat, (forall m: nat, m < n -> P m) -> P n
forall m : nat, m <= 0 -> P m intros m hm.P: nat -> Prop
h:= forall n : nat, (forall m: nat, m < n -> P m) -> P n
m: nat
hm: m <= 0
P m inversion hm.P: nat -> Prop
h:= forall n : nat, (forall m: nat, m < n -> P m) -> P n
m: nat
hm: m <= 0
H: m = 0
P 0
      apply h.P: nat -> Prop
h:= forall n : nat, (forall m: nat, m < n -> P m) -> P n
m: nat
hm: m <= 0
H: m = 0
forall m0 : nat, m0 < 0 -> P m0 intros k hk.P: nat -> Prop
h:= forall n : nat, (forall m: nat, m < n -> P m) -> P n
m: nat
hm: m <= 0
H: m = 0
k: nat
hk: k < 0
P k lia.
    -P: nat -> Prop
h:= forall n : nat, (forall m: nat, m < n -> P m) -> P n
n: nat
ih:= forall m: nat, m <= n -> P m
forall m : nat, m <= S n -> P m intros m hm.P: nat -> Prop
h:= forall n : nat, (forall m: nat, m < n -> P m) -> P n
n: nat
ih:= forall m: nat, m <= n -> P m
m: nat
hm: m <= S n
P m apply h.P: nat -> Prop
h:= forall n : nat, (forall m: nat, m < n -> P m) -> P n
n: nat
ih:= forall m: nat, m <= n -> P m
m: nat
hm: m <= S n
forall m0 : nat, m0 < m -> P m0
      intros k hk.P: nat -> Prop
h:= forall n : nat, (forall m: nat, m < n -> P m) -> P n
n: nat
ih:= forall m: nat, m <= n -> P m
m: nat
hm: m <= S n
k: nat
hk: k < m
P k apply ih.P: nat -> Prop
h:= forall n : nat, (forall m: nat, m < n -> P m) -> P n
n: nat
ih:= forall m: nat, m <= n -> P m
m: nat
hm: m <= S n
k: nat
hk: k < m
k <= n lia.
  }P: nat -> Prop
h:= forall n : nat, (forall m: nat, m < n -> P m) -> P n
n: nat
hn:= forall m: nat, m <= n -> P m
P n
  apply hn.P: nat -> Prop
h:= forall n : nat, (forall m: nat, m < n -> P m) -> P n
n: nat
hn:= forall m: nat, m <= n -> P m
n <= n lia.
Qed.strong_nat_ind is defined

EXERCISE

Hint: If you want to assert an equality (e : a = b) and then use rewrite e, then you can also make use of the replace tactic. replace a with b will replace a with b in the goal and ask you to prove the equality between the two.

Lemma even1_to_even2 n :
  even1 n ->
  even2 n = true.n: nat
even1 n -> even2 n = true
Proof.n: nat
even1 n -> even2 n = true

Short for intros n h. destruct h as [m e]. subst e.:

  intros [m ->].m: nat
even2 (2 * m) = true

In fact the -> means rewriting e from left to right.

  induction m as [| m ih].even2 (2 * 0) = true
m: nat
ih: even2 (2 * m) = true
even2 (2 * S m) = true
  -even2 (2 * 0) = true simpl.true = true reflexivity.
  -m: nat
ih: even2 (2 * m) = true
even2 (2 * S m) = true replace (2 * S m) with (S (S (2 * m))) by lia.m: nat
ih: even2 (2 * m) = true
even2 (S (S (2 * m))) = true

replace a with b allows us to rewrite with an equality we have yet to prove between a and b. by lia tells Rocq that lia will prove said equality.

    simpl.m: nat
ih: even2 (2 * m) = true
even2 (m + (m + 0)) = true assumption.
Qed.even1_to_even2 is defined

EXERCISE

Lemma even2_iff_even3 n :
  even2 n = true <-> even3 n.n: nat
even2 n = true <-> even3 n
Proof.n: nat
even2 n = true <-> even3 n
  induction n as [n ih] using strong_nat_ind.n: nat
ih:= forall m: nat, m < n -> even2 m = true <-> even3 m
even2 n = true <-> even3 n
  destruct n as [| [| n]].ih:= forall m: nat, m < 0 -> even2 m = true <-> even3 m
even2 0 = true <-> even3 0
ih:= forall m: nat, m < 1 -> even2 m = true <-> even3 m
even2 1 = true <-> even3 1
n: nat
ih:= forall m: nat, m < S (S n) -> even2 m = true <-> even3 m
even2 (S (S n)) = true <-> even3 (S (S n))
  -ih:= forall m: nat, m < 0 -> even2 m = true <-> even3 m
even2 0 = true <-> even3 0 simpl.ih:= forall m: nat, m < 0 -> even2 m = true <-> even3 m
true = true <-> True split.ih:= forall m: nat, m < 0 -> even2 m = true <-> even3 m
true = true -> True
ih:= forall m: nat, m < 0 -> even2 m = true <-> even3 m
True -> true = true
    +ih:= forall m: nat, m < 0 -> even2 m = true <-> even3 m
true = true -> True intro.ih:= forall m: nat, m < 0 -> even2 m = true <-> even3 m
H: true = true
True constructor.
    +ih:= forall m: nat, m < 0 -> even2 m = true <-> even3 m
True -> true = true reflexivity.
  -ih:= forall m: nat, m < 1 -> even2 m = true <-> even3 m
even2 1 = true <-> even3 1 simpl.ih:= forall m: nat, m < 1 -> even2 m = true <-> even3 m
false = true <-> False split.ih:= forall m: nat, m < 1 -> even2 m = true <-> even3 m
false = true -> False
ih:= forall m: nat, m < 1 -> even2 m = true <-> even3 m
False -> false = true
    +ih:= forall m: nat, m < 1 -> even2 m = true <-> even3 m
false = true -> False discriminate.
    +ih:= forall m: nat, m < 1 -> even2 m = true <-> even3 m
False -> false = true contradiction.
  -n: nat
ih:= forall m: nat, m < S (S n) -> even2 m = true <-> even3 m
even2 (S (S n)) = true <-> even3 (S (S n)) simpl.n: nat
ih:= forall m: nat, m < S (S n) -> even2 m = true <-> even3 m
even2 n = true <-> even3 n apply ih.n: nat
ih:= forall m: nat, m < S (S n) -> even2 m = true <-> even3 m
n < S (S n) lia.
Qed.even2_iff_even3 is defined

EXERCISE

Hint: The tactic contradiction is useful if you have an obviously false hypothesis.

Lemma even3_to_even4 n :
  even3 n ->
  even4 n.n: nat
even3 n -> even4 n
Proof.n: nat
even3 n -> even4 n
  intros h.n: nat
h: even3 n
even4 n
  induction n as [n ih] using strong_nat_ind.n: nat
ih:= forall m: nat, m < n -> even3 m -> even4 m
h: even3 n
even4 n
  destruct n as [| [| n]].ih:= forall m: nat, m < 0 -> even3 m -> even4 m
h: even3 0
even4 0
ih:= forall m: nat, m < 1 -> even3 m -> even4 m
h: even3 1
even4 1
n: nat
ih:= forall m: nat, m < S (S n) -> even3 m -> even4 m
h: even3 (S (S n))
even4 (S (S n))
  -ih:= forall m: nat, m < 0 -> even3 m -> even4 m
h: even3 0
even4 0 constructor.
  -ih:= forall m: nat, m < 1 -> even3 m -> even4 m
h: even3 1
even4 1 simpl in h.ih:= forall m: nat, m < 1 -> even3 m -> even4 m
h: False
even4 1 contradiction.
  -n: nat
ih:= forall m: nat, m < S (S n) -> even3 m -> even4 m
h: even3 (S (S n))
even4 (S (S n)) constructor.n: nat
ih:= forall m: nat, m < S (S n) -> even3 m -> even4 m
h: even3 (S (S n))
even4 n apply ih.n: nat
ih:= forall m: nat, m < S (S n) -> even3 m -> even4 m
h: even3 (S (S n))
n < S (S n)
n: nat
ih:= forall m: nat, m < S (S n) -> even3 m -> even4 m
h: even3 (S (S n))
even3 n
    +n: nat
ih:= forall m: nat, m < S (S n) -> even3 m -> even4 m
h: even3 (S (S n))
n < S (S n) lia.
    +n: nat
ih:= forall m: nat, m < S (S n) -> even3 m -> even4 m
h: even3 (S (S n))
even3 n assumption.
Qed.even3_to_even4 is defined

EXERCISE

Lemma even4_to_even1 n :
  even4 n ->
  even1 n.n: nat
even4 n -> even1 n
Proof.n: nat
even4 n -> even1 n
  intros h.n: nat
h: even4 n
even1 n
  unfold even1. (* To see what we need to prove *)n: nat
h: even4 n
exists m : nat, n = 2 * m
  induction h as [| n h ih].exists m : nat, 0 = 2 * m
n: nat
h: even4 n
ih:= exists m: nat, n = 2 * m
exists m : nat, S (S n) = 2 * m
  -exists m : nat, 0 = 2 * m exists 0.0 = 2 * 0 reflexivity.
  -n: nat
h: even4 n
ih:= exists m: nat, n = 2 * m
exists m : nat, S (S n) = 2 * m destruct ih as [m ->].m: nat
h: even4 (2 * m)
exists m0 : nat, S (S (2 * m)) = 2 * m0
    exists (S m).m: nat
h: even4 (2 * m)
S (S (2 * m)) = 2 * S m lia.
Qed.even4_to_even1 is defined

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.In is defined
In is recursively defined (guarded on 3rd argument)

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).In_i is defined
In_i_ind is defined
In_i_sind is defined

EXERCISE

Lemma In_iff A (x : A) l :
  In x l <-> In_i x l.A: Type
x: A
l: list A
In x l <-> In_i x l
Proof.A: Type
x: A
l: list A
In x l <-> In_i x l
  split.A: Type
x: A
l: list A
In x l -> In_i x l
A: Type
x: A
l: list A
In_i x l -> In x l
  -A: Type
x: A
l: list A
In x l -> In_i x l intros h.A: Type
x: A
l: list A
h: In x l
In_i x l induction l as [| a l ih].A: Type
x: A
h: In x []
In_i x []
A: Type
x, a: A
l: list A
h:= In x (a :: l)
ih: In x l -> In_i x l
In_i x (a :: l)
    +A: Type
x: A
h: In x []
In_i x [] simpl in h.A: Type
x: A
h: False
In_i x [] contradiction.
    +A: Type
x, a: A
l: list A
h:= In x (a :: l)
ih: In x l -> In_i x l
In_i x (a :: l) simpl in h.A: Type
x, a: A
l: list A
h: a = x \/ In x l
ih: In x l -> In_i x l
In_i x (a :: l) destruct h as [-> | h].A: Type
x: A
l: list A
ih: In x l -> In_i x l
In_i x (x :: l)
A: Type
x, a: A
l: list A
h: In x l
ih: In x l -> In_i x l
In_i x (a :: l)
      *A: Type
x: A
l: list A
ih: In x l -> In_i x l
In_i x (x :: l) constructor.
      *A: Type
x, a: A
l: list A
h: In x l
ih: In x l -> In_i x l
In_i x (a :: l) constructor.A: Type
x, a: A
l: list A
h: In x l
ih: In x l -> In_i x l
In_i x l apply ih.A: Type
x, a: A
l: list A
h: In x l
ih: In x l -> In_i x l
In x l assumption.
  -A: Type
x: A
l: list A
In_i x l -> In x l intros h.A: Type
x: A
l: list A
h: In_i x l
In x l induction h.A: Type
x: A
l: list A
In x (x :: l)
A: Type
x, y: A
l: list A
h: In_i x l
IHh: In x l
In x (y :: l)
    +A: Type
x: A
l: list A
In x (x :: l) simpl.A: Type
x: A
l: list A
x = x \/ In x l left.A: Type
x: A
l: list A
x = x reflexivity.
    +A: Type
x, y: A
l: list A
h: In_i x l
IHh: In x l
In x (y :: l) simpl.A: Type
x, y: A
l: list A
h: In_i x l
IHh: In x l
y = x \/ In x l right.A: Type
x, y: A
l: list A
h: In_i x l
IHh: In x l
In x l assumption.
Qed.In_iff is defined

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

Definition fact_iter_f '(i,x) :=
  (S i, S i * x).fact_iter_f is defined

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

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

Module Fib_Iter.Interactive Module Fib_Iter started

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

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

EXERCISE

  Lemma fib_eq0 :
    fib 0 = 0.fib 0 = 0
  Proof.fib 0 = 0
    reflexivity.
  Qed.fib_eq0 is defined

EXERCISE

  Lemma fib_eq1 :
    fib 1 = 1.fib 1 = 1
  Proof.fib 1 = 1
    reflexivity.
  Qed.fib_eq1 is defined

EXERCISE

Note. It's proven by reflexivity directly!

  Lemma fib_eq3 :
    forall n,
      fib (S (S n)) = fib n + fib (S n).forall n : nat, fib (S (S n)) = fib n + fib (S n)
  Proof.forall n : nat, fib (S (S n)) = fib n + fib (S n)
    reflexivity.
  Qed.fib_eq3 is defined

End Fib_Iter.Module Fib_Iter is defined

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.rtclos is defined
rtclos_ind is defined
rtclos_sind is defined

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.rtclos' is defined
rtclos'_ind is defined
rtclos'_sind is defined

EXERCISE

Hint: You can use apply f with u to provide u as argument to f when Rocq can't guess it on its own.

Lemma rtclos'_trans :
  forall A (R : A -> A -> Prop) x y z,
    rtclos' R x y ->
    rtclos' R y z ->
    rtclos' R x z.forall (A : Type) (R : A -> A -> Prop) (x y z : A), rtclos' R x y -> rtclos' R y z -> rtclos' R x z
Proof.forall (A : Type) (R : A -> A -> Prop) (x y z : A), rtclos' R x y -> rtclos' R y z -> rtclos' R x z
  intros A R x y z hxy hyz.A: Type
R: A -> A -> Prop
x, y, z: A
hxy: rtclos' R x y
hyz: rtclos' R y z
rtclos' R x z
  induction hxy as [x | x y w h1 h2 ih].A: Type
R: A -> A -> Prop
z, x: A
hyz: rtclos' R x z
rtclos' R x z
A: Type
R: A -> A -> Prop
z, x, y, w: A
h1: R x y
h2: rtclos' R y w
hyz: rtclos' R w z
ih: rtclos' R w z -> rtclos' R y z
rtclos' R x z
  -A: Type
R: A -> A -> Prop
z, x: A
hyz: rtclos' R x z
rtclos' R x z assumption.

The with keyword is to give the argument it can't guess.

  -A: Type
R: A -> A -> Prop
z, x, y, w: A
h1: R x y
h2: rtclos' R y w
hyz: rtclos' R w z
ih: rtclos' R w z -> rtclos' R y z
rtclos' R x z apply trans' with y.A: Type
R: A -> A -> Prop
z, x, y, w: A
h1: R x y
h2: rtclos' R y w
hyz: rtclos' R w z
ih: rtclos' R w z -> rtclos' R y z
R x y
A: Type
R: A -> A -> Prop
z, x, y, w: A
h1: R x y
h2: rtclos' R y w
hyz: rtclos' R w z
ih: rtclos' R w z -> rtclos' R y z
rtclos' R y z
    +A: Type
R: A -> A -> Prop
z, x, y, w: A
h1: R x y
h2: rtclos' R y w
hyz: rtclos' R w z
ih: rtclos' R w z -> rtclos' R y z
R x y assumption.
    +A: Type
R: A -> A -> Prop
z, x, y, w: A
h1: R x y
h2: rtclos' R y w
hyz: rtclos' R w z
ih: rtclos' R w z -> rtclos' R y z
rtclos' R y z apply ih.A: Type
R: A -> A -> Prop
z, x, y, w: A
h1: R x y
h2: rtclos' R y w
hyz: rtclos' R w z
ih: rtclos' R w z -> rtclos' R y z
rtclos' R w z assumption.
Qed.rtclos'_trans is defined

EXERCISE

Lemma rtclos_iff :
  forall A (R : A -> A -> Prop) x y,
    rtclos R x y <-> rtclos' R x y.forall (A : Type) (R : A -> A -> Prop) (x y : A), rtclos R x y <-> rtclos' R x y
Proof.forall (A : Type) (R : A -> A -> Prop) (x y : A), rtclos R x y <-> rtclos' R x y
  intros A R x y.A: Type
R: A -> A -> Prop
x, y: A
rtclos R x y <-> rtclos' R x y
  split.A: Type
R: A -> A -> Prop
x, y: A
rtclos R x y -> rtclos' R x y
A: Type
R: A -> A -> Prop
x, y: A
rtclos' R x y -> rtclos R x y
  -A: Type
R: A -> A -> Prop
x, y: A
rtclos R x y -> rtclos' R x y intros h.A: Type
R: A -> A -> Prop
x, y: A
h: rtclos R x y
rtclos' R x y induction h.A: Type
R: A -> A -> Prop
x: A
rtclos' R x x
A: Type
R: A -> A -> Prop
x, y: A
H: R x y
rtclos' R x y
A: Type
R: A -> A -> Prop
x, y, z: A
h1: rtclos R x y
h2: rtclos R y z
IHh1: rtclos' R x y
IHh2: rtclos' R y z
rtclos' R x z
    +A: Type
R: A -> A -> Prop
x: A
rtclos' R x x constructor.
    +A: Type
R: A -> A -> Prop
x, y: A
H: R x y
rtclos' R x y apply trans' with y.A: Type
R: A -> A -> Prop
x, y: A
H: R x y
R x y
A: Type
R: A -> A -> Prop
x, y: A
H: R x y
rtclos' R y y
      *A: Type
R: A -> A -> Prop
x, y: A
H: R x y
R x y assumption.
      *A: Type
R: A -> A -> Prop
x, y: A
H: R x y
rtclos' R y y constructor.
    +A: Type
R: A -> A -> Prop
x, y, z: A
h1: rtclos R x y
h2: rtclos R y z
IHh1: rtclos' R x y
IHh2: rtclos' R y z
rtclos' R x z apply rtclos'_trans with y.A: Type
R: A -> A -> Prop
x, y, z: A
h1: rtclos R x y
h2: rtclos R y z
IHh1: rtclos' R x y
IHh2: rtclos' R y z
rtclos' R x y
A: Type
R: A -> A -> Prop
x, y, z: A
h1: rtclos R x y
h2: rtclos R y z
IHh1: rtclos' R x y
IHh2: rtclos' R y z
rtclos' R y z all: assumption.
  -A: Type
R: A -> A -> Prop
x, y: A
rtclos' R x y -> rtclos R x y induction 1. (* To introduce the first argument and induct on it *)A: Type
R: A -> A -> Prop
x: A
rtclos R x x
A: Type
R: A -> A -> Prop
x, y, z: A
H: R x y
H0: rtclos' R y z
IHrtclos': rtclos R y z
rtclos R x z
    +A: Type
R: A -> A -> Prop
x: A
rtclos R x x constructor.
    +A: Type
R: A -> A -> Prop
x, y, z: A
H: R x y
H0: rtclos' R y z
IHrtclos': rtclos R y z
rtclos R x z apply trans with y.A: Type
R: A -> A -> Prop
x, y, z: A
H: R x y
H0: rtclos' R y z
IHrtclos': rtclos R y z
rtclos R x y
A: Type
R: A -> A -> Prop
x, y, z: A
H: R x y
H0: rtclos' R y z
IHrtclos': rtclos R y z
rtclos R y z
      *A: Type
R: A -> A -> Prop
x, y, z: A
H: R x y
H0: rtclos' R y z
IHrtclos': rtclos R y z
rtclos R x y constructor.A: Type
R: A -> A -> Prop
x, y, z: A
H: R x y
H0: rtclos' R y z
IHrtclos': rtclos R y z
R x y assumption.
      *A: Type
R: A -> A -> Prop
x, y, z: A
H: R x y
H0: rtclos' R y z
IHrtclos': rtclos R y z
rtclos R y z assumption.
Qed.rtclos_iff is defined

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

Note the following notation '(x,y) is performing pattern matching implicitly.

Definition to_nat '(x, y) : nat :=
  y + to_nat' (y + x).to_nat is defined

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

EXERCISE

Show that of_nat is a left inverse of to_nat.

Lemma cancel_of_to :
  forall p,
    of_nat (to_nat p) = p.forall p : nat * nat, of_nat (to_nat p) = p
Proof.forall p : nat * nat, of_nat (to_nat p) = p
  assert (H : forall n p, to_nat p = n -> of_nat n = p).forall (n : nat) (p : nat * nat), to_nat p = n -> of_nat n = p
H:= forall (n : nat) (p: nat * nat), to_nat p = n -> of_nat n = p
forall p : nat * nat, of_nat (to_nat p) = p
  {forall (n : nat) (p : nat * nat), to_nat p = n -> of_nat n = p intros n p h.n: nat
p: nat * nat
h: to_nat p = n
of_nat n = p
    induction n as [| n ih] in p, h |- *.p: nat * nat
h: to_nat p = 0
of_nat 0 = p
n: nat
p: nat * nat
h: to_nat p = S n
ih:= forall p: nat * nat, to_nat p = n -> of_nat n = p
of_nat (S n) = p
    -p: nat * nat
h: to_nat p = 0
of_nat 0 = p simpl.p: nat * nat
h: to_nat p = 0
(0, 0) = p destruct p as [x y].x, y: nat
h: to_nat (x, y) = 0
(0, 0) = (x, y)
      simpl in h.x, y: nat
h: y + to_nat' (y + x) = 0
(0, 0) = (x, y) destruct y as [| y].x: nat
h: 0 + to_nat' (0 + x) = 0
(0, 0) = (x, 0)
x, y: nat
h: S y + to_nat' (S y + x) = 0
(0, 0) = (x, S y) 2: discriminate.x: nat
h: 0 + to_nat' (0 + x) = 0
(0, 0) = (x, 0)
      simpl in h.x: nat
h: to_nat' x = 0
(0, 0) = (x, 0) destruct x as [| x].h: to_nat' 0 = 0
(0, 0) = (0, 0)
x: nat
h: to_nat' (S x) = 0
(0, 0) = (S x, 0) 2: discriminate.h: to_nat' 0 = 0
(0, 0) = (0, 0)
      reflexivity.
    -n: nat
p: nat * nat
h: to_nat p = S n
ih:= forall p: nat * nat, to_nat p = n -> of_nat n = p
of_nat (S n) = p destruct p as [x y].n, x, y: nat
h: to_nat (x, y) = S n
ih:= forall p: nat * nat, to_nat p = n -> of_nat n = p
of_nat (S n) = (x, y)
      simpl in h.n, x, y: nat
h: y + to_nat' (y + x) = S n
ih:= forall p: nat * nat, to_nat p = n -> of_nat n = p
of_nat (S n) = (x, y) destruct y as [| y].n, x: nat
h: 0 + to_nat' (0 + x) = S n
ih:= forall p: nat * nat, to_nat p = n -> of_nat n = p
of_nat (S n) = (x, 0)
n, x, y: nat
h: S y + to_nat' (S y + x) = S n
ih:= forall p: nat * nat, to_nat p = n -> of_nat n = p
of_nat (S n) = (x, S y)
      +n, x: nat
h: 0 + to_nat' (0 + x) = S n
ih:= forall p: nat * nat, to_nat p = n -> of_nat n = p
of_nat (S n) = (x, 0) simpl in h.n, x: nat
h: to_nat' x = S n
ih:= forall p: nat * nat, to_nat p = n -> of_nat n = p
of_nat (S n) = (x, 0)
        destruct x as [| x].n: nat
h: to_nat' 0 = S n
ih:= forall p: nat * nat, to_nat p = n -> of_nat n = p
of_nat (S n) = (0, 0)
n, x: nat
h: to_nat' (S x) = S n
ih:= forall p: nat * nat, to_nat p = n -> of_nat n = p
of_nat (S n) = (S x, 0) 1: discriminate.n, x: nat
h: to_nat' (S x) = S n
ih:= forall p: nat * nat, to_nat p = n -> of_nat n = p
of_nat (S n) = (S x, 0)
        simpl in *.n, x: nat
h: S (x + to_nat' x) = S n
ih:= forall p: nat * nat, to_nat p = n -> of_nat n = p
match of_nat n with | (0, y) => (S y, 0) | (S x1, y) => (x1, S y) end = (S x, 0) rewrite (ih (0,x)).n, x: nat
h: S (x + to_nat' x) = S n
ih:= forall p: nat * nat, to_nat p = n -> of_nat n = p
(S x, 0) = (S x, 0)
n, x: nat
h: S (x + to_nat' x) = S n
ih:= forall p: nat * nat, to_nat p = n -> of_nat n = p
to_nat (0, x) = n
        *n, x: nat
h: S (x + to_nat' x) = S n
ih:= forall p: nat * nat, to_nat p = n -> of_nat n = p
(S x, 0) = (S x, 0) reflexivity.
        *n, x: nat
h: S (x + to_nat' x) = S n
ih:= forall p: nat * nat, to_nat p = n -> of_nat n = p
to_nat (0, x) = n simpl.n, x: nat
h: S (x + to_nat' x) = S n
ih:= forall p: nat * nat, to_nat p = n -> of_nat n = p
x + to_nat' (x + 0) = n replace (x + 0) with x by lia.n, x: nat
h: S (x + to_nat' x) = S n
ih:= forall p: nat * nat, to_nat p = n -> of_nat n = p
x + to_nat' x = n lia.
      +n, x, y: nat
h: S y + to_nat' (S y + x) = S n
ih:= forall p: nat * nat, to_nat p = n -> of_nat n = p
of_nat (S n) = (x, S y) simpl in *.n, x, y: nat
h: S (y + S (y + x + to_nat' (y + x))) = S n
ih:= forall p: nat * nat, to_nat p = n -> of_nat n = p
match of_nat n with | (0, y0) => (S y0, 0) | (S x1, y0) => (x1, S y0) end = (x, S y) rewrite (ih (S x, y)).n, x, y: nat
h: S (y + S (y + x + to_nat' (y + x))) = S n
ih:= forall p: nat * nat, to_nat p = n -> of_nat n = p
(x, S y) = (x, S y)
n, x, y: nat
h: S (y + S (y + x + to_nat' (y + x))) = S n
ih:= forall p: nat * nat, to_nat p = n -> of_nat n = p
to_nat (S x, y) = n
        *n, x, y: nat
h: S (y + S (y + x + to_nat' (y + x))) = S n
ih:= forall p: nat * nat, to_nat p = n -> of_nat n = p
(x, S y) = (x, S y) reflexivity.
        *n, x, y: nat
h: S (y + S (y + x + to_nat' (y + x))) = S n
ih:= forall p: nat * nat, to_nat p = n -> of_nat n = p
to_nat (S x, y) = n simpl.n, x, y: nat
h: S (y + S (y + x + to_nat' (y + x))) = S n
ih:= forall p: nat * nat, to_nat p = n -> of_nat n = p
y + to_nat' (y + S x) = n replace (y + S x) with (S y + x) by lia.n, x, y: nat
h: S (y + S (y + x + to_nat' (y + x))) = S n
ih:= forall p: nat * nat, to_nat p = n -> of_nat n = p
y + to_nat' (S y + x) = n
          simpl.n, x, y: nat
h: S (y + S (y + x + to_nat' (y + x))) = S n
ih:= forall p: nat * nat, to_nat p = n -> of_nat n = p
y + S (y + x + to_nat' (y + x)) = n lia.
  }H:= forall (n : nat) (p: nat * nat), to_nat p = n -> of_nat n = p
forall p : nat * nat, of_nat (to_nat p) = p
  intros p.H:= forall (n : nat) (p: nat * nat), to_nat p = n -> of_nat n = p
p: nat * nat
of_nat (to_nat p) = p apply H.H:= forall (n : nat) (p: nat * nat), to_nat p = n -> of_nat n = p
p: nat * nat
to_nat p = to_nat p reflexivity.
Qed.cancel_of_to is defined

EXERCISE

Show to_nat is injective.

Corollary to_nat_inj :
  forall p q,
    to_nat p = to_nat q ->
    p = q.forall p q : nat * nat, to_nat p = to_nat q -> p = q
Proof.forall p q : nat * nat, to_nat p = to_nat q -> p = q
  intros p q e.p, q: nat * nat
e: to_nat p = to_nat q
p = q
  apply (f_equal of_nat) in e.p, q: nat * nat
e: of_nat (to_nat p) = of_nat (to_nat q)
p = q

[2!] means do the rewrite twice.

  rewrite 2!cancel_of_to in e.p, q: nat * nat
e: p = q
p = q
  assumption.
Qed.to_nat_inj is defined

EXERCISE

Show to_nat is a left inverse to of_nat.

Lemma cancel_to_of :
  forall n,
    to_nat (of_nat n) = n.forall n : nat, to_nat (of_nat n) = n
Proof.forall n : nat, to_nat (of_nat n) = n
  intros n.n: nat
to_nat (of_nat n) = n induction n as [| n ih].to_nat (of_nat 0) = 0
n: nat
ih: to_nat (of_nat n) = n
to_nat (of_nat (S n)) = S n
  -to_nat (of_nat 0) = 0 reflexivity.
  -n: nat
ih: to_nat (of_nat n) = n
to_nat (of_nat (S n)) = S n simpl.n: nat
ih: to_nat (of_nat n) = n
to_nat match of_nat n with | (0, y) => (S y, 0) | (S x0, y) => (x0, S y) end = S n destruct (of_nat n) as [x y].n, x, y: nat
ih: to_nat (x, y) = n
to_nat match x with | 0 => (S y, 0) | S x0 => (x0, S y) end = S n
    destruct x as [| x].n, y: nat
ih: to_nat (0, y) = n
to_nat (S y, 0) = S n
n, x, y: nat
ih: to_nat (S x, y) = n
to_nat (x, S y) = S n
    +n, y: nat
ih: to_nat (0, y) = n
to_nat (S y, 0) = S n simpl in *.n, y: nat
ih: y + to_nat' (y + 0) = n
S (y + to_nat' y) = S n replace (y + 0) with y in ih by lia.n, y: nat
ih: y + to_nat' y = n
S (y + to_nat' y) = S n lia.
    +n, x, y: nat
ih: to_nat (S x, y) = n
to_nat (x, S y) = S n simpl in *.n, x, y: nat
ih: y + to_nat' (y + S x) = n
S (y + S (y + x + to_nat' (y + x))) = S n replace (y + S x) with (S y + x) in ih by lia.n, x, y: nat
ih: y + to_nat' (S y + x) = n
S (y + S (y + x + to_nat' (y + x))) = S n
      simpl in ih.n, x, y: nat
ih: y + S (y + x + to_nat' (y + x)) = n
S (y + S (y + x + to_nat' (y + x))) = S n lia.
Qed.cancel_to_of is defined

EXERCISE

Show of_nat is injective.

Corollary of_nat_inj :
  forall n m,
    of_nat n = of_nat m ->
    n = m.forall n m : nat, of_nat n = of_nat m -> n = m
Proof.forall n m : nat, of_nat n = of_nat m -> n = m

The following notation applies f_equal to_nat to e.

  intros n m e%(f_equal to_nat).n, m: nat
e: to_nat (of_nat n) = to_nat (of_nat m)
n = m
  rewrite 2!cancel_to_of in e.n, m: nat
e: n = m
n = m
  assumption.
Qed.of_nat_inj is defined

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 :=
  forall (X : Prop) (s : X -> X) (z : X), X.num is defined

Definition zero : num :=
  fun X s z => z.zero is defined

Definition succ : num -> num :=
  fun n X s z => s (n X s z).succ is defined

Fixpoint from_nat n : num :=
  match n with
  | 0 => zero
  | S n => succ (from_nat n)
  end.from_nat is defined
from_nat is recursively defined (guarded on 1st argument)

Definition add : num -> num -> num :=
  fun n m X s z => n X s (m X s z).add is defined

Compute (add (from_nat 3) (from_nat 2)).= fun (X : Prop) (s : X -> X) (z : X) => s (s (s (s (s z))))
: num

EXERCISE

Lemma add_from_nat :
  forall n m,
    add (from_nat n) (from_nat m) = from_nat (n + m).forall n m : nat, add (from_nat n) (from_nat m) = from_nat (n + m)
Proof.forall n m : nat, add (from_nat n) (from_nat m) = from_nat (n + m)
  intros n m.n, m: nat
add (from_nat n) (from_nat m) = from_nat (n + m)
  induction n as [| n ih].m: nat
add (from_nat 0) (from_nat m) = from_nat (0 + m)
n, m: nat
ih: add (from_nat n) (from_nat m) = from_nat (n + m)
add (from_nat (S n)) (from_nat m) = from_nat (S n + m)
  -m: nat
add (from_nat 0) (from_nat m) = from_nat (0 + m) reflexivity.
  -n, m: nat
ih: add (from_nat n) (from_nat m) = from_nat (n + m)
add (from_nat (S n)) (from_nat m) = from_nat (S n + m) simpl.n, m: nat
ih: add (from_nat n) (from_nat m) = from_nat (n + m)
add (succ (from_nat n)) (from_nat m) = succ (from_nat (n + m)) rewrite <- ih.n, m: nat
ih: add (from_nat n) (from_nat m) = from_nat (n + m)
add (succ (from_nat n)) (from_nat m) = succ (add (from_nat n) (from_nat m)) reflexivity.
Qed.add_from_nat is defined

EXERCISE

Definition mul : num -> num -> num :=
  fun n m X s z => n X (m X s) z.mul is defined

EXERCISE

Lemma mul_from_nat :
  forall n m,
    mul (from_nat n) (from_nat m) = from_nat (n * m).forall n m : nat, mul (from_nat n) (from_nat m) = from_nat (n * m)
Proof.forall n m : nat, mul (from_nat n) (from_nat m) = from_nat (n * m)
  intros n m.n, m: nat
mul (from_nat n) (from_nat m) = from_nat (n * m)
  induction n as [| n ih].m: nat
mul (from_nat 0) (from_nat m) = from_nat (0 * m)
n, m: nat
ih: mul (from_nat n) (from_nat m) = from_nat (n * m)
mul (from_nat (S n)) (from_nat m) = from_nat (S n * m)
  -m: nat
mul (from_nat 0) (from_nat m) = from_nat (0 * m) simpl.m: nat
mul zero (from_nat m) = zero reflexivity.
  -n, m: nat
ih: mul (from_nat n) (from_nat m) = from_nat (n * m)
mul (from_nat (S n)) (from_nat m) = from_nat (S n * m) simpl.n, m: nat
ih: mul (from_nat n) (from_nat m) = from_nat (n * m)
mul (succ (from_nat n)) (from_nat m) = from_nat (m + n * m) rewrite <- add_from_nat.n, m: nat
ih: mul (from_nat n) (from_nat m) = from_nat (n * m)
mul (succ (from_nat n)) (from_nat m) = add (from_nat m) (from_nat (n * m)) rewrite <- ih.n, m: nat
ih: mul (from_nat n) (from_nat m) = from_nat (n * m)
mul (succ (from_nat n)) (from_nat m) = add (from_nat m) (mul (from_nat n) (from_nat m)) reflexivity.
Qed.mul_from_nat is defined

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

EXERCISE

Lemma exp_from_nat n m :
  exp (from_nat n) (from_nat m) = from_nat (n ^ m).n, m: nat
exp (from_nat n) (from_nat m) = from_nat (n ^ m)
Proof.n, m: nat
exp (from_nat n) (from_nat m) = from_nat (n ^ m)
  induction m as [| m ih].n: nat
exp (from_nat n) (from_nat 0) = from_nat (n ^ 0)
n, m: nat
ih: exp (from_nat n) (from_nat m) = from_nat (n ^ m)
exp (from_nat n) (from_nat (S m)) = from_nat (n ^ S m)
  -n: nat
exp (from_nat n) (from_nat 0) = from_nat (n ^ 0) reflexivity.
  -n, m: nat
ih: exp (from_nat n) (from_nat m) = from_nat (n ^ m)
exp (from_nat n) (from_nat (S m)) = from_nat (n ^ S m) simpl.n, m: nat
ih: exp (from_nat n) (from_nat m) = from_nat (n ^ m)
exp (from_nat n) (succ (from_nat m)) = from_nat (n * n ^ m) rewrite <- mul_from_nat.n, m: nat
ih: exp (from_nat n) (from_nat m) = from_nat (n ^ m)
exp (from_nat n) (succ (from_nat m)) = mul (from_nat n) (from_nat (n ^ m)) rewrite <- ih.n, m: nat
ih: exp (from_nat n) (from_nat m) = from_nat (n ^ m)
exp (from_nat n) (succ (from_nat m)) = mul (from_nat n) (exp (from_nat n) (from_nat m)) reflexivity.
Qed.exp_from_nat is defined

EXERCISE

Define a predecessor function.

For the solution we also encode pairs.

Definition prod (A B : Prop) :=
  forall (X : Prop) (c : A -> B -> X), X.prod is defined

Definition pair {A B} a b : prod A B :=
  fun X c => c a b.pair is defined

Definition fst {A B} (p : prod A B) : A :=
  p _ (fun a b => a).fst is defined

Definition snd {A B} (p : prod A B) : B :=
  p _ (fun a b => b).snd is defined

Definition pred' : num -> prod num num :=
  fun n => n _ (fun p => pair (snd p) (succ (snd p))) (pair zero zero).pred' is defined

Definition pred : num -> num :=
  fun n =>
    fst (pred' n).pred is defined

EXERCISE

Lemma pred'_from_nat n :
  pred' (from_nat n) = pair (from_nat (Nat.pred n)) (from_nat n).n: nat
pred' (from_nat n) = pair (from_nat (Nat.pred n)) (from_nat n)
Proof.n: nat
pred' (from_nat n) = pair (from_nat (Nat.pred n)) (from_nat n)
  induction n as [| n ih].pred' (from_nat 0) = pair (from_nat (Nat.pred 0)) (from_nat 0)
n: nat
ih: pred' (from_nat n) = pair (from_nat (Nat.pred n)) (from_nat n)
pred' (from_nat (S n)) = pair (from_nat (Nat.pred (S n))) (from_nat (S n))
  -pred' (from_nat 0) = pair (from_nat (Nat.pred 0)) (from_nat 0) reflexivity.
  -n: nat
ih: pred' (from_nat n) = pair (from_nat (Nat.pred n)) (from_nat n)
pred' (from_nat (S n)) = pair (from_nat (Nat.pred (S n))) (from_nat (S n)) simpl.n: nat
ih: pred' (from_nat n) = pair (from_nat (Nat.pred n)) (from_nat n)
pred' (succ (from_nat n)) = pair (from_nat n) (succ (from_nat n)) unfold pred' in *.n: nat
ih:= from_nat n (prod num num) (fun p: prod num num => pair (snd p) (succ (snd p))) (pair zero zero) = pair (from_nat (Nat.pred n)) (from_nat n)
succ (from_nat n) (prod num num) (fun p : prod num num => pair (snd p) (succ (snd p))) (pair zero zero) = pair (from_nat n) (succ (from_nat n))
    unfold succ at 1.n: nat
ih:= from_nat n (prod num num) (fun p: prod num num => pair (snd p) (succ (snd p))) (pair zero zero) = pair (from_nat (Nat.pred n)) (from_nat n)
pair (snd (from_nat n (prod num num) (fun p : prod num num => pair (snd p) (succ (snd p))) (pair zero zero))) (succ (snd (from_nat n (prod num num) (fun p : prod num num => pair (snd p) (succ (snd p))) (pair zero zero)))) = pair (from_nat n) (succ (from_nat n)) rewrite ih.n: nat
ih:= from_nat n (prod num num) (fun p: prod num num => pair (snd p) (succ (snd p))) (pair zero zero) = pair (from_nat (Nat.pred n)) (from_nat n)
pair (snd (pair (from_nat (Nat.pred n)) (from_nat n))) (succ (snd (pair (from_nat (Nat.pred n)) (from_nat n)))) = pair (from_nat n) (succ (from_nat n)) reflexivity.
Qed.pred'_from_nat is defined

Lemma pred_from_nat n :
  pred (from_nat n) = from_nat (Nat.pred n).n: nat
pred (from_nat n) = from_nat (Nat.pred n)
Proof.n: nat
pred (from_nat n) = from_nat (Nat.pred n)
  unfold pred.n: nat
fst (pred' (from_nat n)) = from_nat (Nat.pred n)
  rewrite pred'_from_nat.n: nat
fst (pair (from_nat (Nat.pred n)) (from_nat n)) = from_nat (Nat.pred n)
  reflexivity.
Qed.pred_from_nat is defined