MPRI PRFA — Proof Assistants

Inductive types — part 2

We continue after part 1, still looking at inductive types.

From Stdlib  Require Import List.
Import ListNotations.

Set Default Goal Selector "!".

Dependent pairs

We define the type of dependent pairs, where the second component can depend on the first. We often call those Σ-types (hence the name sigT).

Inductive sigT {A} (B : A -> Type) :=
| existT (a : A) (b : B a) : sigT B.sigT is defined
sigT_rect is defined
sigT_ind is defined
sigT_rec is defined
sigT_sind is defined

Arguments existT {A B}.

For instance, we can create a type of pairs, where the first component is always a boolean b, but the second is of type nat when b is true and of type list nat otherwise.

Definition T := sigT (fun (b : bool) => if b then nat else list nat).T is defined

We can then create two elements of type T, a pair (true, 17) and a pair (false, [ 90 ; 4 ; 8 ]). This is something you could not do without dependent types (so for instance, not in OCaml).

Definition pair1 : T :=
  existT true 17.pair1 is defined

Definition pair2 : T :=
  existT false [ 90 ; 4 ; 8 ].pair2 is defined

Important, you should have a look at the induction principle for dependent pairs.

Check sigT_ind.sigT_ind
     : forall (A : Type) (B : A -> Type) (P : sigT B -> Prop), (forall (a : A) (b : B a), P (existT a b)) -> forall s : sigT B, P s

Remark. In the standard library, you have a notation for sigT: you can write { x : A & B x } for sigT B. This looks like the usual subset notation.

Similar to how a function of type A * B -> C is the same as A -> B -> C (which we call currying), we can turn a function of type sigT {A} B -> C to a (dependent) function of type forall (x : A), B x -> C.

Notice that forall can work for dependent functions and not just for propositions.

Definition cur {A} {B : A -> Type} {C} (f : sigT B -> C) :
  forall (x : A), B x -> C :=
  fun a b => f (existT a b).cur is defined

We can perform the opposite transformation.

Definition car {A} {B : A -> Type} {C} (f : forall x, B x -> C) :
  sigT B -> C :=
  fun p =>
    match p with
    | existT a b => f a b
    end.car is defined

And now we can prove that they are indeed inverse of each other.

Lemma car_cur A (B : A -> Type) C (f : sigT B -> C) p :
  car (cur f) p = f p.A: Type
B: A -> Type
C: Type
f: sigT B -> C
p: sigT B
car (cur f) p = f p
Proof.A: Type
B: A -> Type
C: Type
f: sigT B -> C
p: sigT B
car (cur f) p = f p
  destruct p as [a b].A: Type
B: A -> Type
C: Type
f: sigT B -> C
a: A
b: B a
car (cur f) (existT a b) = f (existT a b) reflexivity.
Qed.car_cur is defined

The other direction is even simpler, there is nothing to destruct so the proof is direct by reflexivity.

Lemma cur_car A (B : A -> Type) C (f : forall (x : A), B x -> C) a b :
  cur (car f) a b = f a b.A: Type
B: A -> Type
C: Type
f:= forall x: A, B x -> C
a: A
b: B a
cur (car f) a b = f a b
Proof.A: Type
B: A -> Type
C: Type
f:= forall x: A, B x -> C
a: A
b: B a
cur (car f) a b = f a b
  reflexivity.
Qed.cur_car is defined

Polymorphic iteration

We will now have a look at iter, a function such that iter f n x applies n times the function f, starting with the argument x. For instance iter f 2 x is f (f x).

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)

We can show that iterating the successor n times is the same as adding n.

Lemma iter_add n x :
  n + x = iter S n x.n, x: nat
n + x = iter S n x
Proof.n, x: nat
n + x = iter S n x
  induction n as [|n IH].x: nat
0 + x = iter S 0 x
n, x: nat
IH: n + x = iter S n x
S n + x = iter S (S n) x all: simpl.x: nat
x = x
n, x: nat
IH: n + x = iter S n x
S (n + x) = S (iter S n x)
  -x: nat
x = x reflexivity.
  -n, x: nat
IH: n + x = iter S n x
S (n + x) = S (iter S n x) f_equal.n, x: nat
IH: n + x = iter S n x
n + x = iter S n x assumption.
Qed.iter_add is defined

Similarly, multiplication is iterated addition.

Lemma iter_mul n x :
  n * x = iter (Nat.add x) n 0.n, x: nat
n * x = iter (Nat.add x) n 0
Proof.n, x: nat
n * x = iter (Nat.add x) n 0
  induction n as [|n IH].x: nat
0 * x = iter (Nat.add x) 0 0
n, x: nat
IH: n * x = iter (Nat.add x) n 0
S n * x = iter (Nat.add x) (S n) 0 all: simpl.x: nat
0 = 0
n, x: nat
IH: n * x = iter (Nat.add x) n 0
x + n * x = x + iter (Nat.add x) n 0
  -x: nat
0 = 0 reflexivity.
  -n, x: nat
IH: n * x = iter (Nat.add x) n 0
x + n * x = x + iter (Nat.add x) n 0 f_equal.n, x: nat
IH: n * x = iter (Nat.add x) n 0
n * x = iter (Nat.add x) n 0 assumption.
Qed.iter_mul is defined

Indexed inductive types

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)).even is defined
even_ind is defined
even_sind is defined

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.Unnamed_thm is defined

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.Unnamed_thm0 is defined

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.Unnamed_thm1 is defined

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

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.even_to_evenb is defined

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.strong_nat_ind is defined

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.evenb_to_even is defined

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).le is defined
le_ind is defined
le_sind is defined

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.Unnamed_thm2 is defined

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.Unnamed_thm3 is defined

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.Unnamed_thm4 is defined

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.le_iff is defined

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.le_trans is defined

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

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.le_rtclos is defined