Inductive predicates

Authors:

Yannick Forster, Théo Winterhalter

Files:

• Source

• Exercise sheet

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 hyoptheses. 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 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 implictly 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.

The "less than" 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.

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 2498-2562

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 2582-2726

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 3946-4013

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.

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 @rclos 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.