lesson2_part2.v

Inductive predicates

Authors:

Yannick Forster, Théo Winterhalter

Files:

We can define predicates using the Inductive keyword as well.

Inductive even : nat -> Prop :=
| evenO : even 0
| evenS n : even n -> even (S (S n)).

Being inductive, their proofs can be constructed using the constructor tactic.

Note: The Goal command is similar to Lemma except it doesn't require a name for a lemma which is useful when just checking things that are not useful later such as the fact the 4 is even…

Goal even 4.even 4
Proof.even 4
  constructor.even 2 constructor.even 0 constructor.
Qed.

Case analysis works using inversion.

Goal ~ even 3.~ even 3
Proof.~ even 3
  intros h.h: even 3
False
  inversion h.h: even 3
n: nat
H0: even 1
H: n = 1
False

Here we learnt from even 3 that to build it we must have had even 1 first.

  inversion H0.

But there is no rule (neither evenO nor evenS) that can unify with even 1 so there is no goal left, we are done!

Qed.

inversion is useful but it is hard to predict its behaviour and to name the resulting hypotheses. So we might want to use regular case analysis instead, ie. use destruct.

Goal ~ even 3.~ even 3
Proof.~ even 3
  intro h.h: even 3
False
  destruct h.False
n: nat
h: even n
False

Here this is quite terrible because destruct completely forgets about the fact we had 3 so we are left with an unprovable goal.

Abort.

There is a way to recover this information by telling Rocq to remember it as an equality using the remember tactic.

Goal ~ even 3.~ even 3
Proof.~ even 3
  intro h.h: even 3
False
  remember 3 as n eqn: e.n: nat
e: n = 3
h: even n
False
  destruct h.e: 0 = 3
False
n: nat
e: S (S n) = 3
h: even n
False
  -e: 0 = 3
False

See that n has been replaced by 0 but since we also kept the equality e we know this case is impossible.

    discriminate.
  -n: nat
e: S (S n) = 3
h: even n
False

In the other branch, we have that 3 must be 2 + n for some even n which is also impossible but requires noticing that n must be 1. inversion on the equality will give us that.

    inversion e.n: nat
e: S (S n) = 3
h: even n
H0: n = 1
False

We can then use subst to automatically substitute n by 1.

    subst.h: even 1
e: 3 = 3
False

We can now rely on inversion again to discharge the goal.

    inversion h.
Qed.

Rather than an inductive predicate, we can also define a Boolean function that checks whether its argument is even.

Fixpoint evenb n :=
  match n with
  | 0 => true
  | 1 => false
  | S (S n) => evenb n
  end.

We can show that the two are equivalent.

Lemma even_to_evenb n :
  even n ->
  evenb n = true.n: nat
even n -> evenb n = true
Proof.n: nat
even n -> evenb n = true
  intros h.n: nat
h: even n
evenb n = true

We can perform induction on the proof!

  induction h.evenb 0 = true
n: nat
h: even n
IHh: evenb n = true
evenb (S (S n)) = true
  -evenb 0 = true reflexivity.
  -n: nat
h: even n
IHh: evenb n = true
evenb (S (S n)) = true simpl.n: nat
h: even n
IHh: evenb n = true
evenb n = true assumption.
Qed.

And now the other direction.

Lemma evenb_to_even n :
  evenb n = true ->
  even n.n: nat
evenb n = true -> even n
Proof.n: nat
evenb n = true -> even n
  intros h.n: nat
h: evenb n = true
even n

This time we have to perform the induction on n.

  induction n as [ | n ih].h: evenb 0 = true
even 0
n: nat
h: evenb (S n) = true
ih: evenb n = true -> even n
even (S n)
  -h: evenb 0 = true
even 0 constructor.
  -n: nat
h: evenb (S n) = true
ih: evenb n = true -> even n
even (S n) destruct n.h: evenb 1 = true
ih: evenb 0 = true -> even 0
even 1
n: nat
h: evenb (S (S n)) = true
ih: evenb (S n) = true -> even (S n)
even (S (S n))
    +h: evenb 1 = true
ih: evenb 0 = true -> even 0
even 1 simpl in h.h: false = true
ih: evenb 0 = true -> even 0
even 1 discriminate.
    +n: nat
h: evenb (S (S n)) = true
ih: evenb (S n) = true -> even (S n)
even (S (S n)) constructor.n: nat
h: evenb (S (S n)) = true
ih: evenb (S n) = true -> even (S n)
even n

Note how we are stuck here: The inductive hypothesis talks about S n instead of n. But this we cannot generalise.

Abort.

The solution is to use a stronger form of induction that lets you conclude about any smaller argument. We'll require Lia which provides the lia tactic (for linear integer arithmetic) to help us deal with some arithmetic goals.

From Stdlib Require Import Lia.

In the induction principle below we use forall which is used to quantify over anything from natural numbers to propositions. We can use intros to introduce those variables, the same way we do it for implication.

The strong induction principle is as you'd expect: to prove some property P about n, you can assume it holds for all natural numbers that are smaller.

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

We'll show a stronger property by induction, that P is valid for n and everything below.

  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.

lia knows there can't be k < 0 so it solves the goal for us. It is implicitly using a proof of ~ k < 0 together with False elimination.

    -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 inversion 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
H: m = S n
P (S n)
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
m0: nat
H0: m <= n
H: m0 = n
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
m: nat
hm: m <= S n
H: m = S n
P (S n) 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
H: m = S n
forall m0 : nat, m0 < S n -> 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
H: m = S n
k: nat
hk: k < S n
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
H: m = S n
k: nat
hk: k < S n
k <= n 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
m: nat
hm: m <= S n
m0: nat
H0: m <= n
H: m0 = n
P m 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
m0: nat
H0: m <= n
H: m0 = n
m <= 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.

Back to even. We can now use our stronger induction principle thanks to the using clause of the induction tactic. Indeed, the tactic can use anything that looks like an induction principle (which is admittedly a vague notion) which can be very handy!

Lemma evenb_to_even n :
  evenb n = true -> even n.n: nat
evenb n = true -> even n
Proof.n: nat
evenb n = true -> even n
  intros h.n: nat
h: evenb n = true
even n
  induction n as [n ih] using strong_nat_ind.n: nat
ih: forall m : nat, m < n -> evenb m = true -> even m
h: evenb n = true
even n

As opposed to regular induction, we only have one case to consider: an arbitrary n but for which we have an induction hypothesis. We still need to perform case analysis, so we'll do it manually. We have to consider the cases 0, 1 and S (S n). We could perform destruct n once to get cases 0 and S n and then in the second branch do destruct again, but we can do it all at once by using square brackets within square brackets.

  destruct n as [| [| n]].ih: forall m : nat, m < 0 -> evenb m = true -> even m
h: evenb 0 = true
even 0
ih: forall m : nat, m < 1 -> evenb m = true -> even m
h: evenb 1 = true
even 1
n: nat
ih: forall m : nat, m < S (S n) -> evenb m = true -> even m
h: evenb (S (S n)) = true
even (S (S n))
  -ih: forall m : nat, m < 0 -> evenb m = true -> even m
h: evenb 0 = true
even 0 constructor.
  -ih: forall m : nat, m < 1 -> evenb m = true -> even m
h: evenb 1 = true
even 1 simpl in h.ih: forall m : nat, m < 1 -> evenb m = true -> even m
h: false = true
even 1 discriminate.
  -n: nat
ih: forall m : nat, m < S (S n) -> evenb m = true -> even m
h: evenb (S (S n)) = true
even (S (S n)) simpl in h.n: nat
ih: forall m : nat, m < S (S n) -> evenb m = true -> even m
h: evenb n = true
even (S (S n)) constructor.n: nat
ih: forall m : nat, m < S (S n) -> evenb m = true -> even m
h: evenb n = true
even n
    apply ih.n: nat
ih: forall m : nat, m < S (S n) -> evenb m = true -> even m
h: evenb n = true
n < S (S n)
n: nat
ih: forall m : nat, m < S (S n) -> evenb m = true -> even m
h: evenb n = true
evenb n = true
    +n: nat
ih: forall m : nat, m < S (S n) -> evenb m = true -> even m
h: evenb n = true
n < S (S n) lia.
    +n: nat
ih: forall m : nat, m < S (S n) -> evenb m = true -> even m
h: evenb n = true
evenb n = true assumption.
Qed.

Exercise: Strong induction

We now allow you to use lia. Prove strong induction yourself, without looking at the proof above.

Module StrongInd.

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

End StrongInd.

Exercise: Evenness

Here are two definitions of even numbers.

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

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

Define an even predicate similar to how you would define a Boolean predicate but using propositions instead.

Fixpoint even3 (n : nat) : Prop :=
  REPLACE_ME.Not a truly recursive fixpoint. [non-recursive,fixpoints,default]

And a fourth one, as an inductive predicate.

Inductive even4 : nat -> Prop :=
| even4O : even4 0
| even4S n : even4 n -> even4 (S (S n)).

Spell out the induction principle of even4 without checking it.

⚠️ Do not forget this one.

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

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
Admitted.
Lemma even4_to_even1 n :
  even4 n ->
  even1 n.n: nat
even4 n -> even1 n
Proof.n: nat
even4 n -> even1 n
Admitted.

The "less than or equal" predicate <= we have used above is defined as follows.

The idea is that n ≤ n always holds, and if n ≤ m then n ≤ S m. In other words, if you can remove successors S from m and reach n then n ≤ m.

Inductive le : nat -> nat -> Prop :=
| leO n : le n n
| leS n m : le n m -> le n (S m).

We build the proof as hinted above, by removing S from 5 until we reach 3 which takes only two steps.

Goal le 3 5.le 3 5
Proof.le 3 5
  constructor.le 3 4 constructor.le 3 3 constructor.
Qed.

To show that 1 is not below 0 we can use inversion again.

Goal ~ le 1 0.~ le 1 0
Proof.~ le 1 0
  intros h.h: le 1 0
False inversion h.
Qed.

As for even we can also do it more manually.

Goal ~ le 1 0.~ le 1 0
Proof.~ le 1 0
  intros h.h: le 1 0
False remember 1 as n1 eqn: e1.n1: nat
e1: n1 = 1
h: le n1 0
False remember 0 as n0 eqn: e0.n1, n0: nat
e0: n0 = 0
e1: n1 = S n0
h: le n1 n0
False
  destruct h.n: nat
e0: n = 0
e1: n = S n
False
m: nat
e0: S m = 0
n: nat
e1: n = S (S m)
h: le n m
False
  -n: nat
e0: n = 0
e1: n = S n
False subst.e1: 0 = 1
False discriminate.
  -m: nat
e0: S m = 0
n: nat
e1: n = S (S m)
h: le n m
False subst.m: nat
e0: S m = 0
h: le (S (S m)) m
False discriminate.
Qed.

As a sanity check, we can verify the following property.

Below exists (x : A), P x is very similar to sigT P except that P x is a proposition. We can prove exists x, P x by e.g., using exists 0 and then proving P 0.

Lemma le_iff n m :
  le n m <-> exists k, k + n = m.n, m: nat
le n m <-> (exists k : nat, k + n = m)
Proof.n, m: nat
le n m <-> (exists k : nat, k + n = m)
  split.n, m: nat
le n m -> exists k : nat, k + n = m
n, m: nat
(exists k : nat, k + n = m) -> le n m
  -n, m: nat
le n m -> exists k : nat, k + n = m intros h.n, m: nat
h: le n m
exists k : nat, k + n = m induction h as [n | n m h ih].n: nat
exists k : nat, k + n = n
n, m: nat
h: le n m
ih: exists k : nat, k + n = m
exists k : nat, k + n = S m
    +n: nat
exists k : nat, k + n = n exists 0.n: nat
0 + n = n reflexivity.
    +n, m: nat
h: le n m
ih: exists k : nat, k + n = m
exists k : nat, k + n = S m destruct ih as [k ih].n, m: nat
h: le n m
k: nat
ih: k + n = m
exists k0 : nat, k0 + n = S m subst.n, k: nat
h: le n (k + n)
exists k0 : nat, k0 + n = S (k + n)
      exists (S k).n, k: nat
h: le n (k + n)
S k + n = S (k + n) simpl.n, k: nat
h: le n (k + n)
S (k + n) = S (k + n) reflexivity.
  -n, m: nat
(exists k : nat, k + n = m) -> le n m

Instead of doing intro x and then destruct x as [a b] we can do intros [a b].

    intros [k h].n, m, k: nat
h: k + n = m
le n m subst.n, k: nat
le n (k + n)
    induction k as [| k ih].n: nat
le n (0 + n)
n, k: nat
ih: le n (k + n)
le n (S k + n)
    +n: nat
le n (0 + n) simpl.n: nat
le n n constructor.
    +n, k: nat
ih: le n (k + n)
le n (S k + n) simpl.n, k: nat
ih: le n (k + n)
le n (S (k + n)) constructor.n, k: nat
ih: le n (k + n)
le n (k + n) assumption.
Qed.

We can also show transitivity.

Lemma le_trans n m k :
  le n m ->
  le m k ->
  le n k.n, m, k: nat
le n m -> le m k -> le n k
Proof.n, m, k: nat
le n m -> le m k -> le n k
  intros hnm hmk.n, m, k: nat
hnm: le n m
hmk: le m k
le n k induction hmk as [ m | m k hmk ih ].n, m: nat
hnm: le n m
le n m
n, m: nat
hnm: le n m
k: nat
hmk: le m k
ih: le n m -> le n k
le n (S k)
  -n, m: nat
hnm: le n m
le n m assumption.
  -n, m: nat
hnm: le n m
k: nat
hmk: le m k
ih: le n m -> le n k
le n (S k) constructor.n, m: nat
hnm: le n m
k: nat
hmk: le m k
ih: le n m -> le n k
le n k apply ih.n, m: nat
hnm: le n m
k: nat
hmk: le m k
ih: le n m -> le n k
le n m assumption.
Qed.

Exercise: Another definition of le

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

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

⚠️ Do not forget this one.

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

Lemma le_equiv n m :
  le' n m <-> le n m.n, m: nat
le' n m <-> le n m
Proof.n, m: nat
le' n m <-> le n m
Admitted.

Exercise: Boolean comparison

Fixpoint leb (n m : nat) : bool :=
  REPLACE_ME.Not a truly recursive fixpoint. [non-recursive,fixpoints,default]

Lemma leb_spec n m :
  leb n m = true <-> le n m.n, m: nat
leb n m = true <-> le n m
Proof.n, m: nat
leb n m = true <-> le n m
Admitted.

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.

From Stdlib Require Import Lia List.
Import ListNotations.

Inductive rtree (A : Type) :=
| N (a : A) (ts : list (rtree A)).rtree is nested using list. No scheme for list is registered as All. It can
be generated using command "Scheme All" e.g. "Scheme All for list.".
[register-all,automation,default]
rtree is nested using list. No scheme for list is registered as All. It can
be generated using command "Scheme All" e.g. "Scheme All for list.".
[register-all,automation,default]
rtree is nested using list. No scheme for list is registered as All. It can
be generated using command "Scheme All" e.g. "Scheme All for list.".
[register-all,automation,default]
rtree is nested using list. No scheme for list is registered as All. It can
be generated using command "Scheme All" e.g. "Scheme All for list.".
[register-all,automation,default]
rtree is nested using list. No scheme for list is registered as All. It can
be generated using command "Scheme All" e.g. "Scheme All for list.".
[register-all,automation,default]
rtree is nested using list. No scheme for list is registered as All. It can
be generated using command "Scheme All" e.g. "Scheme All for list.".
[register-all,automation,default]
rtree is nested using list. No scheme for list is registered as All. It can
be generated using command "Scheme All" e.g. "Scheme All for list.".
[register-all,automation,default]
rtree is nested using list. No scheme for list is registered as All. It can
be generated using command "Scheme All" e.g. "Scheme All for list.".
[register-all,automation,default]
rtree is nested using list. No scheme for list is registered as All. It can
be generated using command "Scheme All" e.g. "Scheme All for list.".
[register-all,automation,default]
rtree is nested using list. No scheme for list is registered as All. It can
be generated using command "Scheme All" e.g. "Scheme All for list.".
[register-all,automation,default]
rtree is nested using list. No scheme for list is registered as All. It can
be generated using command "Scheme All" e.g. "Scheme All for list.".
[register-all,automation,default]
rtree is nested using list. No scheme for list is registered as All. It can
be generated using command "Scheme All" e.g. "Scheme All for list.".
[register-all,automation,default]

About rtree_ind.rtree_ind :
forall (A : Type) (P : rtree A -> Prop),
(forall (a : A) (ts : list (rtree A)), P (N A a ts)) ->
forall r : rtree A, P r

rtree_ind is not universe polymorphic
Arguments rtree_ind A%_type_scope (P N)%_function_scope r
rtree_ind is transparent
Expands to: Constant lesson2_part2.rtree_ind
Declared in toplevel input, characters 3638-3702

Inductive Forall {A} (P : A -> Prop) : list A -> Prop :=
| Forall_nil : Forall P nil
| Forall_cons a l : P a -> Forall P l -> Forall P (a :: l).

About Forall_ind.Forall_ind :
forall (A : Type) (P : A -> Prop) (P0 : list A -> Prop),
P0 [] ->
(forall (a : A) (l : list A), P a -> Forall P l -> P0 l -> P0 (a :: l)) ->
forall l : list A, Forall P l -> P0 l

Forall_ind is not universe polymorphic
Arguments Forall_ind A%_type_scope (P P0)%_function_scope 
  Forall_nil Forall_cons%_function_scope l%_list_scope 
  f
Forall_ind is transparent
Expands to: Constant lesson2_part2.Forall_ind
Declared in toplevel input, characters 3722-3866

Fixpoint rtree_ind' :
  forall (A : Type) (P : rtree A -> Prop),
    (forall (a : A) (ts : list (rtree A)), @Forall (rtree A) P ts -> P (N A a ts)) ->
    forall r : rtree A, P r.rtree_ind': forall (A : Type) (P : rtree A -> Prop),
(forall (a : A) (ts : list (rtree A)), Forall P ts -> P (N A a ts)) ->
forall r : rtree A, P r
forall (A : Type) (P : rtree A -> Prop),
(forall (a : A) (ts : list (rtree A)), Forall P ts -> P (N A a ts)) ->
forall r : rtree A, P r
Proof.rtree_ind': forall (A : Type) (P : rtree A -> Prop),
(forall (a : A) (ts : list (rtree A)), Forall P ts -> P (N A a ts)) ->
forall r : rtree A, P r
forall (A : Type) (P : rtree A -> Prop),
(forall (a : A) (ts : list (rtree A)), Forall P ts -> P (N A a ts)) ->
forall r : rtree A, P r
  intros A P IH r.rtree_ind': forall (A : Type) (P : rtree A -> Prop),
(forall (a : A) (ts : list (rtree A)), Forall P ts -> P (N A a ts)) ->
forall r : rtree A, P r
A: Type
P: rtree A -> Prop
IH: forall (a : A) (ts : list (rtree A)), Forall P ts -> P (N A a ts)
r: rtree A
P r
  destruct r.rtree_ind': forall (A : Type) (P : rtree A -> Prop),
(forall (a : A) (ts : list (rtree A)), Forall P ts -> P (N A a ts)) ->
forall r : rtree A, P r
A: Type
P: rtree A -> Prop
IH: forall (a : A) (ts : list (rtree A)), Forall P ts -> P (N A a ts)
a: A
ts: list (rtree A)
P (N A a ts)
  apply IH.rtree_ind': forall (A : Type) (P : rtree A -> Prop),
(forall (a : A) (ts : list (rtree A)), Forall P ts -> P (N A a ts)) ->
forall r : rtree A, P r
A: Type
P: rtree A -> Prop
IH: forall (a : A) (ts : list (rtree A)), Forall P ts -> P (N A a ts)
a: A
ts: list (rtree A)
Forall P ts induction ts.rtree_ind': forall (A : Type) (P : rtree A -> Prop),
(forall (a : A) (ts : list (rtree A)), Forall P ts -> P (N A a ts)) ->
forall r : rtree A, P r
A: Type
P: rtree A -> Prop
IH: forall (a : A) (ts : list (rtree A)), Forall P ts -> P (N A a ts)
a: A
Forall P []
rtree_ind': forall (A : Type) (P : rtree A -> Prop),
(forall (a : A) (ts : list (rtree A)), Forall P ts -> P (N A a ts)) ->
forall r : rtree A, P r
A: Type
P: rtree A -> Prop
IH: forall (a : A) (ts : list (rtree A)), Forall P ts -> P (N A a ts)
a: A
a0: rtree A
ts: list (rtree A)
IHts: Forall P ts
Forall P (a0 :: ts)
  -rtree_ind': forall (A : Type) (P : rtree A -> Prop),
(forall (a : A) (ts : list (rtree A)), Forall P ts -> P (N A a ts)) ->
forall r : rtree A, P r
A: Type
P: rtree A -> Prop
IH: forall (a : A) (ts : list (rtree A)), Forall P ts -> P (N A a ts)
a: A
Forall P [] econstructor.
  -rtree_ind': forall (A : Type) (P : rtree A -> Prop),
(forall (a : A) (ts : list (rtree A)), Forall P ts -> P (N A a ts)) ->
forall r : rtree A, P r
A: Type
P: rtree A -> Prop
IH: forall (a : A) (ts : list (rtree A)), Forall P ts -> P (N A a ts)
a: A
a0: rtree A
ts: list (rtree A)
IHts: Forall P ts
Forall P (a0 :: ts) econstructor.rtree_ind': forall (A : Type) (P : rtree A -> Prop),
(forall (a : A) (ts : list (rtree A)), Forall P ts -> P (N A a ts)) ->
forall r : rtree A, P r
A: Type
P: rtree A -> Prop
IH: forall (a : A) (ts : list (rtree A)), Forall P ts -> P (N A a ts)
a: A
a0: rtree A
ts: list (rtree A)
IHts: Forall P ts
P a0
rtree_ind': forall (A : Type) (P : rtree A -> Prop),
(forall (a : A) (ts : list (rtree A)), Forall P ts -> P (N A a ts)) ->
forall r : rtree A, P r
A: Type
P: rtree A -> Prop
IH: forall (a : A) (ts : list (rtree A)), Forall P ts -> P (N A a ts)
a: A
a0: rtree A
ts: list (rtree A)
IHts: Forall P ts
Forall P ts
    +rtree_ind': forall (A : Type) (P : rtree A -> Prop),
(forall (a : A) (ts : list (rtree A)), Forall P ts -> P (N A a ts)) ->
forall r : rtree A, P r
A: Type
P: rtree A -> Prop
IH: forall (a : A) (ts : list (rtree A)), Forall P ts -> P (N A a ts)
a: A
a0: rtree A
ts: list (rtree A)
IHts: Forall P ts
P a0 eapply rtree_ind'.rtree_ind': forall (A : Type) (P : rtree A -> Prop),
(forall (a : A) (ts : list (rtree A)), Forall P ts -> P (N A a ts)) ->
forall r : rtree A, P r
A: Type
P: rtree A -> Prop
IH: forall (a : A) (ts : list (rtree A)), Forall P ts -> P (N A a ts)
a: A
a0: rtree A
ts: list (rtree A)
IHts: Forall P ts
forall (a1 : A) (ts0 : list (rtree A)), Forall P ts0 -> P (N A a1 ts0) assumption.
    +rtree_ind': forall (A : Type) (P : rtree A -> Prop),
(forall (a : A) (ts : list (rtree A)), Forall P ts -> P (N A a ts)) ->
forall r : rtree A, P r
A: Type
P: rtree A -> Prop
IH: forall (a : A) (ts : list (rtree A)), Forall P ts -> P (N A a ts)
a: A
a0: rtree A
ts: list (rtree A)
IHts: Forall P ts
Forall P ts assumption.
Qed.

Fixpoint size_rtree {A} (t : rtree A) {struct t} : nat :=
  let size_list := fix size_list {A} (l : list (rtree A)) {struct l} : nat :=
      match l with
      | nil => 0
      | cons t tl => size_rtree t + size_list tl
      end in
  match t with
  | N _ a l => 1 + size_list l
  end.

Fixpoint nodes_rtree {A} (t : rtree A) {struct t} : list A :=
  let nodes_list := fix nodes_list {A} (l : list (rtree A)) {struct l} : list A :=
      match l with
      | nil => nil
      | cons t tl => nodes_rtree t ++ nodes_list tl
      end in
  match t with
  | N _ a l => a :: nodes_list l
  end.

Lemma nodes_size_rtree {A} (t : rtree A) :
  length (nodes_rtree t) = size_rtree t.A: Type
t: rtree A
length (nodes_rtree t) = size_rtree t
Proof.A: Type
t: rtree A
length (nodes_rtree t) = size_rtree t
  revert t.A: Type
forall t : rtree A, length (nodes_rtree t) = size_rtree t apply rtree_ind'.A: Type
forall (a : A) (ts : list (rtree A)),
Forall (fun r : rtree A => length (nodes_rtree r) = size_rtree r) ts ->
length (nodes_rtree (N A a ts)) = size_rtree (N A a ts)
  intros a ts IH.A: Type
a: A
ts: list (rtree A)
IH: Forall (fun r : rtree A => length (nodes_rtree r) = size_rtree r) ts
length (nodes_rtree (N A a ts)) = size_rtree (N A a ts)
  induction IH.A: Type
a: A
length (nodes_rtree (N A a [])) = size_rtree (N A a [])
A: Type
a: A
a0: rtree A
l: list (rtree A)
H: length (nodes_rtree a0) = size_rtree a0
IH: Forall (fun r : rtree A => length (nodes_rtree r) = size_rtree r) l
IHIH: length (nodes_rtree (N A a l)) = size_rtree (N A a l)
length (nodes_rtree (N A a (a0 :: l))) = size_rtree (N A a (a0 :: l))
  -A: Type
a: A
length (nodes_rtree (N A a [])) = size_rtree (N A a []) cbn.A: Type
a: A
1 = 1 reflexivity.
  -A: Type
a: A
a0: rtree A
l: list (rtree A)
H: length (nodes_rtree a0) = size_rtree a0
IH: Forall (fun r : rtree A => length (nodes_rtree r) = size_rtree r) l
IHIH: length (nodes_rtree (N A a l)) = size_rtree (N A a l)
length (nodes_rtree (N A a (a0 :: l))) = size_rtree (N A a (a0 :: l)) cbn.A: Type
a: A
a0: rtree A
l: list (rtree A)
H: length (nodes_rtree a0) = size_rtree a0
IH: Forall (fun r : rtree A => length (nodes_rtree r) = size_rtree r) l
IHIH: length (nodes_rtree (N A a l)) = size_rtree (N A a l)
S
  (length
     (nodes_rtree a0 ++
      (fix nodes_list (A0 : Type) (l0 : list (rtree A0)) {struct l0} :
           list A0 :=
         match l0 with
         | [] => []
         | t :: tl => nodes_rtree t ++ nodes_list A0 tl
         end)
        A l)) =
S
  (size_rtree a0 +
   (fix size_list (A0 : Type) (l0 : list (rtree A0)) {struct l0} : nat :=
      match l0 with
      | [] => 0
      | t :: tl => size_rtree t + size_list A0 tl
      end)
     A l) rewrite !length_app.A: Type
a: A
a0: rtree A
l: list (rtree A)
H: length (nodes_rtree a0) = size_rtree a0
IH: Forall (fun r : rtree A => length (nodes_rtree r) = size_rtree r) l
IHIH: length (nodes_rtree (N A a l)) = size_rtree (N A a l)
S
  (length (nodes_rtree a0) +
   length
     ((fix nodes_list (A0 : Type) (l0 : list (rtree A0)) {struct l0} :
           list A0 :=
         match l0 with
         | [] => []
         | t :: tl => nodes_rtree t ++ nodes_list A0 tl
         end)
        A l)) =
S
  (size_rtree a0 +
   (fix size_list (A0 : Type) (l0 : list (rtree A0)) {struct l0} : nat :=
      match l0 with
      | [] => 0
      | t :: tl => size_rtree t + size_list A0 tl
      end)
     A l)
    rewrite H.A: Type
a: A
a0: rtree A
l: list (rtree A)
H: length (nodes_rtree a0) = size_rtree a0
IH: Forall (fun r : rtree A => length (nodes_rtree r) = size_rtree r) l
IHIH: length (nodes_rtree (N A a l)) = size_rtree (N A a l)
S
  (size_rtree a0 +
   length
     ((fix nodes_list (A0 : Type) (l0 : list (rtree A0)) {struct l0} :
           list A0 :=
         match l0 with
         | [] => []
         | t :: tl => nodes_rtree t ++ nodes_list A0 tl
         end)
        A l)) =
S
  (size_rtree a0 +
   (fix size_list (A0 : Type) (l0 : list (rtree A0)) {struct l0} : nat :=
      match l0 with
      | [] => 0
      | t :: tl => size_rtree t + size_list A0 tl
      end)
     A l) cbn in *.A: Type
a: A
a0: rtree A
l: list (rtree A)
H: length (nodes_rtree a0) = size_rtree a0
IH: Forall (fun r : rtree A => length (nodes_rtree r) = size_rtree r) l
IHIH: S
  (length
     ((fix nodes_list (A : Type) (l : list (rtree A)) {struct l} : list A :=
         match l with
         | [] => []
         | t :: tl => nodes_rtree t ++ nodes_list A tl
         end)
        A l)) =
S
  ((fix size_list (A : Type) (l : list (rtree A)) {struct l} : nat :=
      match l with
      | [] => 0
      | t :: tl => size_rtree t + size_list A tl
      end)
     A l)
S
  (size_rtree a0 +
   length
     ((fix nodes_list (A0 : Type) (l0 : list (rtree A0)) {struct l0} :
           list A0 :=
         match l0 with
         | [] => []
         | t :: tl => nodes_rtree t ++ nodes_list A0 tl
         end)
        A l)) =
S
  (size_rtree a0 +
   (fix size_list (A0 : Type) (l0 : list (rtree A0)) {struct l0} : nat :=
      match l0 with
      | [] => 0
      | t :: tl => size_rtree t + size_list A0 tl
      end)
     A l) lia.
Qed.

Scheme All for list.
Inductive rtree' (A : Type) :=
| N' (a : A) (ts : list (rtree' A)).

About rtree'_ind.rtree'_ind :
forall (A : Type) (P : rtree' A -> Prop),
(forall (a : A) (ts : list (rtree' A)),
 list_all (rtree' A) P ts -> P (N' A a ts)) ->
forall r : rtree' A, P r

rtree'_ind is not universe polymorphic
Arguments rtree'_ind A%_type_scope (P N')%_function_scope r
rtree'_ind is transparent
Expands to: Constant lesson2_part2.rtree'_ind
Declared in toplevel input, characters 5086-5153

Fixpoint size_rtree' {A} (t : rtree' A) {struct t} : nat :=
  let size_list := fix size_list {A} (l : list (rtree' A)) {struct l} : nat :=
      match l with
      | nil => 0
      | cons t tl => size_rtree' t + size_list tl
      end in
  match t with
  | N' _ a l => 1 + size_list l
  end.

Fixpoint nodes_rtree' {A} (t : rtree' A) {struct t} : list A :=
  let nodes_list := fix nodes_list {A} (l : list (rtree' A)) {struct l} : list A :=
      match l with
      | nil => nil
      | cons t tl => nodes_rtree' t ++ nodes_list tl
      end in
  match t with
  | N' _ a l => a :: nodes_list l
  end.

Lemma nodes_size_rtree' {A} (t : rtree' A) :
  length (nodes_rtree' t) = size_rtree' t.A: Type
t: rtree' A
length (nodes_rtree' t) = size_rtree' t
Proof.A: Type
t: rtree' A
length (nodes_rtree' t) = size_rtree' t
  induction t.A: Type
a: A
ts: list (rtree' A)
X: list_all (rtree' A)
  (fun t : rtree' A => length (nodes_rtree' t) = size_rtree' t) ts
length (nodes_rtree' (N' A a ts)) = size_rtree' (N' A a ts)
  induction X.A: Type
a: A
length (nodes_rtree' (N' A a [])) = size_rtree' (N' A a [])
A: Type
a: A
a0: rtree' A
p: length (nodes_rtree' a0) = size_rtree' a0
l: list (rtree' A)
X: list_all (rtree' A)
  (fun t : rtree' A => length (nodes_rtree' t) = size_rtree' t) l
IHX: length (nodes_rtree' (N' A a l)) = size_rtree' (N' A a l)
length (nodes_rtree' (N' A a (a0 :: l))) = size_rtree' (N' A a (a0 :: l))
  -A: Type
a: A
length (nodes_rtree' (N' A a [])) = size_rtree' (N' A a []) cbn.A: Type
a: A
1 = 1 reflexivity.
  -A: Type
a: A
a0: rtree' A
p: length (nodes_rtree' a0) = size_rtree' a0
l: list (rtree' A)
X: list_all (rtree' A)
  (fun t : rtree' A => length (nodes_rtree' t) = size_rtree' t) l
IHX: length (nodes_rtree' (N' A a l)) = size_rtree' (N' A a l)
length (nodes_rtree' (N' A a (a0 :: l))) = size_rtree' (N' A a (a0 :: l)) cbn.A: Type
a: A
a0: rtree' A
p: length (nodes_rtree' a0) = size_rtree' a0
l: list (rtree' A)
X: list_all (rtree' A)
  (fun t : rtree' A => length (nodes_rtree' t) = size_rtree' t) l
IHX: length (nodes_rtree' (N' A a l)) = size_rtree' (N' A a l)
S
  (length
     (nodes_rtree' a0 ++
      (fix nodes_list (A0 : Type) (l0 : list (rtree' A0)) {struct l0} :
           list A0 :=
         match l0 with
         | [] => []
         | t :: tl => nodes_rtree' t ++ nodes_list A0 tl
         end)
        A l)) =
S
  (size_rtree' a0 +
   (fix size_list (A0 : Type) (l0 : list (rtree' A0)) {struct l0} : nat :=
      match l0 with
      | [] => 0
      | t :: tl => size_rtree' t + size_list A0 tl
      end)
     A l) rewrite !length_app.A: Type
a: A
a0: rtree' A
p: length (nodes_rtree' a0) = size_rtree' a0
l: list (rtree' A)
X: list_all (rtree' A)
  (fun t : rtree' A => length (nodes_rtree' t) = size_rtree' t) l
IHX: length (nodes_rtree' (N' A a l)) = size_rtree' (N' A a l)
S
  (length (nodes_rtree' a0) +
   length
     ((fix nodes_list (A0 : Type) (l0 : list (rtree' A0)) {struct l0} :
           list A0 :=
         match l0 with
         | [] => []
         | t :: tl => nodes_rtree' t ++ nodes_list A0 tl
         end)
        A l)) =
S
  (size_rtree' a0 +
   (fix size_list (A0 : Type) (l0 : list (rtree' A0)) {struct l0} : nat :=
      match l0 with
      | [] => 0
      | t :: tl => size_rtree' t + size_list A0 tl
      end)
     A l)
    rewrite p.A: Type
a: A
a0: rtree' A
p: length (nodes_rtree' a0) = size_rtree' a0
l: list (rtree' A)
X: list_all (rtree' A)
  (fun t : rtree' A => length (nodes_rtree' t) = size_rtree' t) l
IHX: length (nodes_rtree' (N' A a l)) = size_rtree' (N' A a l)
S
  (size_rtree' a0 +
   length
     ((fix nodes_list (A0 : Type) (l0 : list (rtree' A0)) {struct l0} :
           list A0 :=
         match l0 with
         | [] => []
         | t :: tl => nodes_rtree' t ++ nodes_list A0 tl
         end)
        A l)) =
S
  (size_rtree' a0 +
   (fix size_list (A0 : Type) (l0 : list (rtree' A0)) {struct l0} : nat :=
      match l0 with
      | [] => 0
      | t :: tl => size_rtree' t + size_list A0 tl
      end)
     A l) cbn in *.A: Type
a: A
a0: rtree' A
p: length (nodes_rtree' a0) = size_rtree' a0
l: list (rtree' A)
X: list_all (rtree' A)
  (fun t : rtree' A => length (nodes_rtree' t) = size_rtree' t) l
IHX: S
  (length
     ((fix nodes_list (A : Type) (l : list (rtree' A)) {struct l} : list A :=
         match l with
         | [] => []
         | t :: tl => nodes_rtree' t ++ nodes_list A tl
         end)
        A l)) =
S
  ((fix size_list (A : Type) (l : list (rtree' A)) {struct l} : nat :=
      match l with
      | [] => 0
      | t :: tl => size_rtree' t + size_list A tl
      end)
     A l)
S
  (size_rtree' a0 +
   length
     ((fix nodes_list (A0 : Type) (l0 : list (rtree' A0)) {struct l0} :
           list A0 :=
         match l0 with
         | [] => []
         | t :: tl => nodes_rtree' t ++ nodes_list A0 tl
         end)
        A l)) =
S
  (size_rtree' a0 +
   (fix size_list (A0 : Type) (l0 : list (rtree' A0)) {struct l0} : nat :=
      match l0 with
      | [] => 0
      | t :: tl => size_rtree' t + size_list A0 tl
      end)
     A l) lia.
Qed.

Exercise: Unlabelled trees

Consider the following type of trees, without labels. Can you give an element of type tree?

Module Unlabelled.

Inductive tree :=
| N (ts : list tree).

Definition ex4 : tree :=
  REPLACE_ME.

End Unlabelled.

Exercise: All and Forall

Here is a variant of Forall in Type. We also make the arguments of the constructors of All and Forall implicit.

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}.
Arguments Forall_nil {A P}.
Arguments Forall_cons {A P}.

Give the induction principles for both All and Forall. For every argument, state whether it is a parameter, non-uniform parameter, or index.

Prove the following.

Lemma All_Forall {A} (P : A -> Prop) (l : list A) :
  All P l -> Forall P l.A: Type
P: A -> Prop
l: list A
All P l -> Forall P l
Proof.A: Type
P: A -> Prop
l: list A
All P l -> Forall P l
Admitted.

Lemma Forall_app {A} (P : A -> Prop) (l1 l2 : list A) :
  Forall P l1 -> Forall P l2 -> Forall P (l1 ++ l2).A: Type
P: A -> Prop
l1, l2: list A
Forall P l1 -> Forall P l2 -> Forall P (l1 ++ l2)
Proof.A: Type
P: A -> Prop
l1, l2: list A
Forall P l1 -> Forall P l2 -> Forall P (l1 ++ l2)
Admitted.

Fixpoint All_app {A} (P : A -> Prop) (l1 l2 : list A) (h1 : All P l1) (h2 : All P l2) {struct h1} : All P (l1 ++ l2) :=
  REPLACE_ME.Not a truly recursive fixpoint. [non-recursive,fixpoints,default]

Exercise: Labelled trees

Extend the type Unlabelled.tree to have labelled nodes.
Prove a bijection between the new type and the mutual tree from the first part, ie. define functions from one to the other and show that they invert each other.

Non-uniform parameters

We can also define the notion of reflexive transitive closure of a relation R : A -> A -> Prop on A like so.

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

In @rtclos A R x y we have

A is a parameter. It is marked as implicit, because it can be inferred from the type of R.
R is a parameter.
x is a non-uniform parameter. That means it looks like a parameter in the conclusion of constructors, and it does not need to be repeatedly introduced for every constructor.
y is an index.

Arguments trans {A R}.

Then le is just the closure of being the successor.

Lemma le_rtclos n m :
  le n m <-> rtclos (fun n m => m = S n) n m.n, m: nat
le n m <-> rtclos (fun n0 m0 : nat => m0 = S n0) n m
Proof.n, m: nat
le n m <-> rtclos (fun n0 m0 : nat => m0 = S n0) n m
  split.n, m: nat
le n m -> rtclos (fun n0 m0 : nat => m0 = S n0) n m
n, m: nat
rtclos (fun n0 m0 : nat => m0 = S n0) n m -> le n m
  -n, m: nat
le n m -> rtclos (fun n0 m0 : nat => m0 = S n0) n m intros h.n, m: nat
h: le n m
rtclos (fun n0 m0 : nat => m0 = S n0) n m induction h as [ n | n m h ih ].n: nat
rtclos (fun n0 m : nat => m = S n0) n n
n, m: nat
h: le n m
ih: rtclos (fun n m : nat => m = S n) n m
rtclos (fun n0 m0 : nat => m0 = S n0) n (S m)
    +n: nat
rtclos (fun n0 m : nat => m = S n0) n n constructor.
    +n, m: nat
h: le n m
ih: rtclos (fun n m : nat => m = S n) n m
rtclos (fun n0 m0 : nat => m0 = S n0) n (S m)

If we just apply constructor then it's going to pick incl which is not what we want. What we want is to use trans:

      apply (trans _ m _).n, m: nat
h: le n m
ih: rtclos (fun n m : nat => m = S n) n m
rtclos (fun n0 m0 : nat => m0 = S n0) n m
n, m: nat
h: le n m
ih: rtclos (fun n m : nat => m = S n) n m
rtclos (fun n0 m0 : nat => m0 = S n0) m (S m) 1: assumption.n, m: nat
h: le n m
ih: rtclos (fun n m : nat => m = S n) n m
rtclos (fun n0 m0 : nat => m0 = S n0) m (S m)

We just applied assumption to the first goal this way.

It can be nicer than having many levels of nested bullets.

      constructor.n, m: nat
h: le n m
ih: rtclos (fun n m : nat => m = S n) n m
S m = S m reflexivity.
  -n, m: nat
rtclos (fun n0 m0 : nat => m0 = S n0) n m -> le n m intros h.n, m: nat
h: rtclos (fun n m : nat => m = S n) n m
le n m induction h as [ n | n m h | n m k hnm ihnm hmk ihmk ].n: nat
le n n
n, m: nat
h: m = S n
le n m
n, m, k: nat
hnm: rtclos (fun n m : nat => m = S n) n m
hmk: rtclos (fun n m : nat => m = S n) m k
ihnm: le n m
ihmk: le m k
le n k
    +n: nat
le n n constructor.
    +n, m: nat
h: m = S n
le n m subst.n: nat
le n (S n) constructor.n: nat
le n n constructor.
    +n, m, k: nat
hnm: rtclos (fun n m : nat => m = S n) n m
hmk: rtclos (fun n m : nat => m = S n) m k
ihnm: le n m
ihmk: le m k
le n k apply (le_trans _ m _).n, m, k: nat
hnm: rtclos (fun n m : nat => m = S n) n m
hmk: rtclos (fun n m : nat => m = S n) m k
ihnm: le n m
ihmk: le m k
le n m
n, m, k: nat
hnm: rtclos (fun n m : nat => m = S n) n m
hmk: rtclos (fun n m : nat => m = S n) m k
ihnm: le n m
ihmk: le m k
le m k all: assumption.
Qed.

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

Propose an inductive definition of membership (add the missing constructor(s)).

Inductive In_i {A} : A -> list A -> Prop := .
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
Admitted.

Exercise: Reflexive transitive closure

Here is another definition of the reflexive transitive closure.

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.

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

Exercise: Factorial and Fibonacci (advanced)

This and the following exercises are more advanced. Make sure you manage to do the previous exercises before. Do not hesitate to ask for help.

Define the factorial function in two ways:

once using Fixpoint
and once using iter

Prove that both yield the same value for all arguments.

⚠️ Do not forget this one. We have not stated the lemmas this time.

Define the Fibonacci 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. Then prove that it satisfies these equations.

Module Fib_Iter.

  Definition fib (n : nat) : nat :=
    REPLACE_ME.

  Lemma fib_eq0 :
    fib 0 = 0.fib 0 = 0
  Proof.fib 0 = 0
  Admitted.

  Lemma fib_eq1 :
    fib 1 = 1.fib 1 = 1
  Proof.fib 1 = 1
  Admitted.

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

End Fib_Iter.

Exercise: Cantor pairing (advanced)

Here is an implementation of the Cantor pairing and its inverse function, a bijection between nat * nat and nat.

From Stdlib Require Import PeanoNat.

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

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.

Show that of_nat is a left inverse for to_nat.

Hint: First show forall n p, to_nat p = n -> of_nat n = p.

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

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

Show to_nat is a left inverse for 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
Admitted.

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

Exercise: Church encodings (advanced)

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.

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)).= fun (X : Prop) (s : X -> X) (z : X) => s (s (s (s (s z))))
: num

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)
Admitted.
Definition mul : num -> num -> num :=
  REPLACE_ME.

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

Define the power function (check out the lemma to make sure you see what it should give).

Definition exp : num -> num -> num :=
  REPLACE_ME.

Lemma exp_from_nat n m :
  exp (from_nat n) (from_nat m) = from_nat (Nat.pow 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)
Admitted.

Define a predecessor function.

Definition pred : num -> num :=
  REPLACE_ME.

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