MPRI PRFA — Proof Assistants

Advanced elimination / induction

The goal of this lecture is to:

Understand more about sorts in Rocq, i.e. about Type and Prop. This is helpful to decipher certain error messages that occasionally occur in practical developments.
Understand how induction principles are implemented and use this knowledge to implement induction principles for inductive types where Rocq's automatic generation is too weak.

Let us start with sorts.

From Stdlib Require Import Arith Lia List.
Import ListNotations.

Sorts

We have already seen Type and Prop. They are also called universes or sorts. You have seen that seemingly Type : Type:

Check (Type : Type).Type : Type
     : Type

But also that Type is actually a hierarchy of universes Type@{i} in order to avoid inconsistencies with Type : Type, which becomes visible once universe printing is enabled.

Set Printing Universes.

Check (Type : Type).Type@{lesson5.24} : Type@{lesson5.23}
     : Type@{lesson5.23}
(* {lesson5.24 lesson5.23} |= lesson5.24 < lesson5.23 *)

Below we will see more about the typing rules of Type, in particular a reminder how the typing rule of forall works.

We use the section mechanism which allows us to declare universe levels and so on.

Section Universes.

Command Universes declares universe levels, while Constraint lets us add (in)equalities between them. Below we declare levels i and j together with constraint i < j. We can see that Type@{i} is of type Type@{j} but not the converse.

  Universes i j.
  Constraint i < j.
  Check Type@{i} : Type@{j}.Type@{i} : Type@{j}
     : Type@{j}
(* {} |= i < j *)
  Fail Check Type@{j} : Type@{i}.The command has indeed failed with message:
The term "Type@{j}" has type "Type@{j+1}" while it is expected to have type "Type@{i}" (universe inconsistency: Cannot enforce j < i because i < j).

Universe of a ∀ quantifier

Let us now have a look at the type of a forall in Rocq. For this we're going to use another feature of the section mechanism: the Context command allows us to add assumptions in our context, similar to assumptions for a lemma.

  Universe k.

  Context (A : Type@{i}) (B : Type@{k}).A is declared
B is declared

As you can see below, the type of a forall is the maximum of the types of the domain and codomain. See what it means for a forall containing Type.

  Check forall (a : A), B.A -> B
     : Type@{max(i,k)}

  Check forall (X : Type@{i}), Type@{k}.Type@{i} -> Type@{k}
     : Type@{max(i+1,k+1)}

Cumulativity

By the way, above, we've just seen a use of so-called cumulativity which says that Type@{i} lives in Type@{j} for any j that's bigger than i. By contrast, in Agda or Lean, we have uniqueness of the type and thus Type@{i} is of Type@{i+1} and that's it.

Cumulativity is actually more than that. It is in fact a form of subtyping that says that Type@{i} is a subtype of Type@{j} whenever i ≤ j.

See how A : Type@{i} also lives in Type@{j} but how the converse wouldn't work.

  Check (A : Type@{j}).A : Type@{j}
     : Type@{j}
(* {} |= i <= j *)

  Context (C : Type@{j}).C is declared

  Fail Check (C : Type@{i}).The command has indeed failed with message:
In environment
A : Type@{i}
B : Type@{k}
C : Type@{j}
The term "C" has type "Type@{j}" while it is expected to have type "Type@{i}" (universe inconsistency: Cannot enforce j <= i because i < j).

Prop lives in Type@{i} for all i.

  Check (Prop : Type@{i}).Prop : Type@{i}
     : Type@{i}
(* {} |= Set < i *)

Here you see Rocq mentions a constraint that Set < i. There is indeed a third kind of universe which we did not mention but you may have seen already. It's called Set. You can think of it as the lowest Type universe: Type@{0}, but in Rocq it's actually Type@{Set} because the universe levels (i, j, k etc.) are not natural numbers but abstract variables with constraints like the one we added above.

Set is the smallest Type and it is the only one which does not contain Prop. We do have cumulativity going from Prop to Set and Type however.

An overview:

Prop : Type@{Set+1}
Set :  Type@{Set+1}
Prop <= Type@{Set+1}
Set <= Type@{Set+1}
Type@{i} : Type@{i+1}
Type@{i} <= Type@{i+1}

See how it goes in practice:

  Fail Check (Prop : Set).The command has indeed failed with message:
In environment
A : Type@{i}
B : Type@{k}
C : Type@{j}
The term "Prop" has type "Type@{Set+1}" while it is expected to have type "Set" (universe inconsistency: Cannot enforce Set+1 <= Set).
  Fail Check (Prop : Type@{Set}).The command has indeed failed with message:
In environment
A : Type@{i}
B : Type@{k}
C : Type@{j}
The term "Prop" has type "Type@{Set+1}" while it is expected to have type "Set" (universe inconsistency: Cannot enforce Set+1 <= Set).

  Variable (P : Prop).P is declared

  Check (P : Type@{i}).P : Type@{i}
     : Type@{i}
  Check (P : Set).P : Set
     : Set

Impredicativity

Prop has other particularities. When considering a forall that ends in a proposition, then the whole forall stays a proposition. This means that things like forall (n : nat), n = n or forall (P : Prop), P are propositions. This property is called impredicativity because things like forall (P : Prop), P are actually quantifying over themselves (P can be instantiated with forall (P : Prop), P).

This is another big difference with Agda which is predicative instead. To remedy this they have to also add universe levels to Prop like Prop@{i}. Lean on the other hands does things the same way as Rocq. In fact, impredicativity is very strong and necessary to achieve the full power of ZFC.

In Rocq, the universe of a forall ending in a proposition is always a proposition, regardless of the size of what we quantify over. This comes from the intuition (and models) that Prop is proof-irrelevant: all propositions are morally either empty (False) or contain only one element (True) so Prop can be seen (modelled) as a set with two elements so it is always small.

The commands below illustrate all we just said.

  Fail Check (Prop : Prop).The command has indeed failed with message:
In environment
A : Type@{i}
B : Type@{k}
C : Type@{j}
P : Prop
The term "Prop" has type "Type@{Set+1}" while it is expected to have type "Prop" (universe inconsistency: Cannot enforce Set+1 <= Prop).

  Check forall (P : Prop), P.forall P : Prop, P
     : Prop
  Check forall (n : nat), n = n.forall n : nat, n = n
     : Prop

  Variable (Q : A -> Prop).Q is declared

  Check forall (x : A), Q x.forall x : A, Q x
     : Prop

  Check forall (X : Type@{j}), P.Type@{j} -> P
     : Prop

  Unset Printing Universes.

End Universes.

Elimination restrictions

Universes are also important when defining inductive types. You may wonder when to put your type in Prop or in Type. We have seen several examples: things like disjunction and conjunction are placed in Prop, but bool is a Type for instance.

The central reasons are the Prop is an impredicative sort (more on that below), but also that Prop can be axiomatically assumed to be proof irrelevant. Proof irrelevance is expressed as follows.

Definition PI :=
  forall (P : Prop) (p q : P), p = q.PI is defined

It states that any two proofs of a given proposition are always equal. In other words, PI being consistent means that proofs cannot impact computation in a meaningful way. That is, we cannot analyse a proof to build a a function that is supposed to compute a Boolean.

Consider a variant of bool in Prop below.

Inductive prop_bool : Prop :=
| ptrue
| pfalse.prop_bool is defined
prop_bool_ind is defined
prop_bool_sind is defined

As long as we remain in Prop, we can do pretty much the same as before.

Definition pneg (b : prop_bool) : prop_bool :=
  match b with
  | ptrue => pfalse
  | pfalse => ptrue
  end.pneg is defined

Lemma pneg_invol :
  forall b, pneg (pneg b) = b.forall b : prop_bool, pneg (pneg b) = b
Proof.forall b : prop_bool, pneg (pneg b) = b
  intros [].pneg (pneg ptrue) = ptrue
pneg (pneg pfalse) = pfalse all: reflexivity.
Qed.pneg_invol is defined

We can also map the usual Booleans into them.

Definition to_prop_bool (b : bool) : prop_bool :=
  if b then ptrue else pfalse.to_prop_bool is defined

But, crucially, we can't do the converse!

Fail Definition to_bool (b : prop_bool) : bool :=
  match b with
  | ptrue => true
  | pfalse => false
  end.The command has indeed failed with message:
Incorrect elimination of "b" in the inductive type "prop_bool":
the return type has sort "Set" while it should be SProp or Prop.
Elimination of an inductive object of sort Prop is not allowed on a predicate in sort "Set"
because proofs can be eliminated only to build proofs.

Rocq complains that proofs can only be eliminated to build other proofs. The same happens in proof mode of course.

Lemma to_bool : prop_bool -> bool.prop_bool -> bool
Proof.prop_bool -> bool
  intro b.b: prop_bool
bool Fail destruct b.The command has indeed failed with message:
Incorrect elimination in the inductive type "prop_bool":
the return type has sort "Set" while it should be SProp or Prop.
Elimination of an inductive object of sort Prop is not allowed on a predicate in sort "Set"
because proofs can be eliminated only to build proofs.
b: prop_bool
bool
Abort.

We can instead prove something weaker like this:

Lemma to_bool :
  forall (p : prop_bool),
    exists (b : bool), to_prop_bool b = p.forall p : prop_bool, exists b : bool, to_prop_bool b = p
Proof.forall p : prop_bool, exists b : bool, to_prop_bool b = p
  intros [].exists b : bool, to_prop_bool b = ptrue
exists b : bool, to_prop_bool b = pfalse
  -exists b : bool, to_prop_bool b = ptrue exists true.to_prop_bool true = ptrue reflexivity.
  -exists b : bool, to_prop_bool b = pfalse exists false.to_prop_bool false = pfalse reflexivity.
Qed.to_bool is defined

We can however not prove that there is a function inverting to_prop_bool because this would be inconsistent with PI:

Lemma to_bool_function_not_PI (f : prop_bool -> bool) :
  (forall b, f (to_prop_bool b) = b) -> ~ PI.f: prop_bool -> bool
(forall b : bool, f (to_prop_bool b) = b) -> ~ PI
Proof.f: prop_bool -> bool
(forall b : bool, f (to_prop_bool b) = b) -> ~ PI
  intros H pi.f: prop_bool -> bool
H:= forall b: bool, f (to_prop_bool b) = b
pi: PI
False
  specialize (pi prop_bool ptrue pfalse).f: prop_bool -> bool
H:= forall b: bool, f (to_prop_bool b) = b
pi: ptrue = pfalse
False
  specialize (H true) as e1.f: prop_bool -> bool
H:= forall b: bool, f (to_prop_bool b) = b
pi: ptrue = pfalse
e1: f (to_prop_bool true) = true
False
  specialize (H false) as e2.f: prop_bool -> bool
H:= forall b: bool, f (to_prop_bool b) = b
pi: ptrue = pfalse
e1: f (to_prop_bool true) = true
e2: f (to_prop_bool false) = false
False
  simpl in *.f: prop_bool -> bool
H:= forall b: bool, f (to_prop_bool b) = b
pi: ptrue = pfalse
e1: f ptrue = true
e2: f pfalse = false
False
  rewrite pi in e1.f: prop_bool -> bool
H:= forall b: bool, f (to_prop_bool b) = b
pi: ptrue = pfalse
e1: f pfalse = true
e2: f pfalse = false
False
  congruence.
Qed.to_bool_function_not_PI is defined

Subsingleton criterion

However, there are crucial exceptions to the rule: If a type has at most one constructor and all the non-parameter arguments of the constructor are proofs, then such eliminations are allowed.

This property is called (sub)singleton criterion because it essentially says that you can inspect (as in case analysis) a proof, as long as there can be at most one such proof. So a term that depends on it, doesn't really depend on it in the end, but merely on the fact that there exists a proof.

This is thanks to this property that we can eliminate a proof of False to produce anything else.

Goal False -> nat.False -> nat
Proof.False -> nat
  intro bot.bot: False
nat destruct bot.
Qed.Unnamed_thm is defined

Definition exfalso' {A : Type} (bot : False) : A :=
  match bot with end.exfalso' is defined

It also works with True, but it's not so interesting. Another more interesting case is equality. This means, you can use tactics such as rewrite on any type.

Goal forall n m (P : nat -> Type), P (n + m) -> P (m + n).forall (n m : nat) (P : nat -> Type), P (n + m) -> P (m + n)
Proof.forall (n m : nat) (P : nat -> Type), P (n + m) -> P (m + n)
  intros n m P x.n, m: nat
P: nat -> Type
x: P (n + m)
P (m + n)
  rewrite Nat.add_comm.n, m: nat
P: nat -> Type
x: P (n + m)
P (n + m) assumption.
Qed.Unnamed_thm0 is defined

The above we can do in general:

Goal forall {A} (P : A -> Type) {u v} (e : u = v) (t : P u), P v.forall (A : Type) (P : A -> Type) (u v : A), u = v -> P u -> P v
Proof.forall (A : Type) (P : A -> Type) (u v : A), u = v -> P u -> P v
  intros A P u v e.A: Type
P: A -> Type
u, v: A
e: u = v
P u -> P v
  now rewrite e.
Qed.Unnamed_thm1 is defined

Disjunction for instance does not fall under the criterion:

Goal forall P Q, P \/ Q -> bool.forall P Q : Prop, P \/ Q -> bool
Proof.forall P Q : Prop, P \/ Q -> bool
  intros P Q h.P, Q: Prop
h: P \/ Q
bool
  Fail destruct h.The command has indeed failed with message:
Incorrect elimination in the inductive type "or":
the return type has sort "Set" while it should be SProp or Prop.
Elimination of an inductive object of sort Prop is not allowed on a predicate in sort "Set"
because proofs can be eliminated only to build proofs.
P, Q: Prop
h: P \/ Q
bool
Abort.

We could try to cheat by boxing a proposition so it only has one constructor but it doesn't actually help.

Inductive Box (P : Prop) : Prop :=
| box (p : P).Box is defined
Box_rect is defined
Box_ind is defined
Box_rec is defined
Box_sind is defined

Goal forall P Q, Box (P \/ Q) -> bool.forall P Q : Prop, Box (P \/ Q) -> bool
Proof.forall P Q : Prop, Box (P \/ Q) -> bool
  intros P Q h.P, Q: Prop
h: Box (P \/ Q)
bool
  destruct h.P, Q: Prop
p: P \/ Q
bool
  Fail destruct h.The command has indeed failed with message:
The variable h was not found in the current environment.
P, Q: Prop
p: P \/ Q
bool
Abort.

Induction principles

Let us now move to induction principles. For this, we'll start with trees.

We can easily define binary trees (with labels in A) as follows.

Inductive bintree A :=
| bt_leaf (a : A)
| bt_node (a : A) (l r : bintree A).bintree is defined
bintree_rect is defined
bintree_ind is defined
bintree_rec is defined
bintree_sind is defined

Arguments bt_leaf {A}.
Arguments bt_node {A}.

As for every inductive type, Rocq generates induction principles corresponding to the various sorts:

bintree_ind for Prop

bintree_rect for Type

bintree_rec for Set (but you can ignore it and use bintree_rect)

They only vary in the return type of the motive (the return predicate).

Check bintree_rect.bintree_rect
     : forall (A : Type) (P : bintree A -> Type), (forall a : A, P (bt_leaf a)) -> (forall (a : A) (l : bintree A), P l -> forall r : bintree A, P r -> P (bt_node a l r)) -> forall b : bintree A, P b

Now consider the following map function on bintree.

Fixpoint bt_map {A B} (f : A -> B) (t : bintree A) : bintree B :=
  match t with
  | bt_leaf a => bt_leaf (f a)
  | bt_node a l r => bt_node (f a) (bt_map f l) (bt_map f r)
  end.bt_map is defined
bt_map is recursively defined (guarded on 4th argument)

When proving properties about it, we will use the induction tactic which picks up the corresponding induction principle, below bintree_ind and apply it for us.

Lemma bt_map_id :
  forall A (t : bintree A),
    bt_map (fun x => x) t = t.forall (A : Type) (t : bintree A), bt_map (fun x : A => x) t = t
Proof.forall (A : Type) (t : bintree A), bt_map (fun x : A => x) t = t
  intros A t.A: Type
t: bintree A
bt_map (fun x : A => x) t = t
  induction t as [a | a l ihl r ihr].A: Type
a: A
bt_map (fun x : A => x) (bt_leaf a) = bt_leaf a
A: Type
a: A
l, r: bintree A
ihl:= bt_map (fun x: A => x) l = l
ihr:= bt_map (fun x: A => x) r = r
bt_map (fun x : A => x) (bt_node a l r) = bt_node a l r
  -A: Type
a: A
bt_map (fun x : A => x) (bt_leaf a) = bt_leaf a reflexivity.
  -A: Type
a: A
l, r: bintree A
ihl:= bt_map (fun x: A => x) l = l
ihr:= bt_map (fun x: A => x) r = r
bt_map (fun x : A => x) (bt_node a l r) = bt_node a l r cbn.A: Type
a: A
l, r: bintree A
ihl:= bt_map (fun x: A => x) l = l
ihr:= bt_map (fun x: A => x) r = r
bt_node a (bt_map (fun x : A => x) l) (bt_map (fun x : A => x) r) = bt_node a l r rewrite ihl, ihr.A: Type
a: A
l, r: bintree A
ihl:= bt_map (fun x: A => x) l = l
ihr:= bt_map (fun x: A => x) r = r
bt_node a l r = bt_node a l r reflexivity.
Qed.bt_map_id is defined

If you print the term, you will see that it indeed starts with an application of bintree_ind. No need to read the rest for now.

Print bt_map_id.bt_map_id = fun (A : Type) (t : bintree A) => bintree_ind A (fun t0 : bintree A => bt_map (fun x : A => x) t0 = t0) (fun a : A => eq_refl) (fun (a : A) (l : bintree A) (ihl : bt_map (fun x : A => x) l = l) (r : bintree A) (ihr : bt_map (fun x : A => x) r = r) => eq_ind_r (fun b : bintree A => bt_node a b (bt_map (fun x : A => x) r) = bt_node a l r) (eq_ind_r (fun b : bintree A => bt_node a l b = bt_node a l r) eq_refl ihr) ihl : bt_map (fun x : A => x) (bt_node a l r) = bt_node a l r) t
     : forall (A : Type) (t : bintree A), bt_map (fun x : A => x) t = t

Arguments bt_map_id A%type_scope t

General trees.

Now say we don't want to limit ourselves to binary trees. The obvious way to define trees is to have nodes take a list of subtrees. Now as we're going to see, the induction principle that Rocq generates is insufficient (although there is hope that the situation improves in the future).

Inductive tree A :=
| node (a : A) (children : list (tree A)).tree is defined
tree_rect is defined
tree_ind is defined
tree_rec is defined
tree_sind is defined

Arguments node {A}.

Now cpnsider a map from bintree to tree, as well as a map function for tree.

Fixpoint bt_to_tree {A} (t : bintree A) : tree A :=
  match t with
  | bt_leaf a => node a []
  | bt_node a l r => node a [ bt_to_tree l ; bt_to_tree r ]
  end.bt_to_tree is defined
bt_to_tree is recursively defined (guarded on 2nd argument)

Fixpoint tree_map {A B} (f : A -> B) (t : tree A) : tree B :=
  match t with
  | node a l => node (f a) (map (tree_map f) l)
  end.tree_map is defined
tree_map is recursively defined (guarded on 4th argument)

We can prove the following property by induction on bintree.

Lemma to_tree_map :
  forall A B (f : A -> B) t,
    tree_map f (bt_to_tree t) = bt_to_tree (bt_map f t).forall (A B : Type) (f : A -> B) (t : bintree A), tree_map f (bt_to_tree t) = bt_to_tree (bt_map f t)
Proof.forall (A B : Type) (f : A -> B) (t : bintree A), tree_map f (bt_to_tree t) = bt_to_tree (bt_map f t)
  intros A B f t.A, B: Type
f: A -> B
t: bintree A
tree_map f (bt_to_tree t) = bt_to_tree (bt_map f t)
  induction t as [a | a l ihl r ihr].A, B: Type
f: A -> B
a: A
tree_map f (bt_to_tree (bt_leaf a)) = bt_to_tree (bt_map f (bt_leaf a))
A, B: Type
f: A -> B
a: A
l, r: bintree A
ihl: tree_map f (bt_to_tree l) = bt_to_tree (bt_map f l)
ihr: tree_map f (bt_to_tree r) = bt_to_tree (bt_map f r)
tree_map f (bt_to_tree (bt_node a l r)) = bt_to_tree (bt_map f (bt_node a l r))
  -A, B: Type
f: A -> B
a: A
tree_map f (bt_to_tree (bt_leaf a)) = bt_to_tree (bt_map f (bt_leaf a)) reflexivity.
  -A, B: Type
f: A -> B
a: A
l, r: bintree A
ihl: tree_map f (bt_to_tree l) = bt_to_tree (bt_map f l)
ihr: tree_map f (bt_to_tree r) = bt_to_tree (bt_map f r)
tree_map f (bt_to_tree (bt_node a l r)) = bt_to_tree (bt_map f (bt_node a l r)) cbn.A, B: Type
f: A -> B
a: A
l, r: bintree A
ihl: tree_map f (bt_to_tree l) = bt_to_tree (bt_map f l)
ihr: tree_map f (bt_to_tree r) = bt_to_tree (bt_map f r)
node (f a) [tree_map f (bt_to_tree l); tree_map f (bt_to_tree r)] = node (f a) [bt_to_tree (bt_map f l); bt_to_tree (bt_map f r)] rewrite ihl, ihr.A, B: Type
f: A -> B
a: A
l, r: bintree A
ihl: tree_map f (bt_to_tree l) = bt_to_tree (bt_map f l)
ihr: tree_map f (bt_to_tree r) = bt_to_tree (bt_map f r)
node (f a) [bt_to_tree (bt_map f l); bt_to_tree (bt_map f r)] = node (f a) [bt_to_tree (bt_map f l); bt_to_tree (bt_map f r)] reflexivity.
Qed.to_tree_map is defined

However, for the following lemma, we'll see induction fails us.

Lemma tree_map_id :
  forall A (t : tree A),
    tree_map (fun x => x) t = t.forall (A : Type) (t : tree A), tree_map (fun x : A => x) t = t
Proof.forall (A : Type) (t : tree A), tree_map (fun x : A => x) t = t
  intros A t.A: Type
t: tree A
tree_map (fun x : A => x) t = t
  induction t.A: Type
a: A
children: list (tree A)
tree_map (fun x : A => x) (node a children) = node a children
  cbn.A: Type
a: A
children: list (tree A)
node a (map (tree_map (fun x : A => x)) children) = node a children f_equal.A: Type
a: A
children: list (tree A)
map (tree_map (fun x : A => x)) children = children

We have no induction hypopthesis at all!!

Abort.

Indeed, see what Rocq generated for us:

Check tree_rect.tree_rect
     : forall (A : Type) (P : tree A -> Type), (forall (a : A) (children : list (tree A)), P (node a children)) -> forall t : tree A, P t

It essentially corresponds to a case analysis, but no induction hypotesis is avaiable. This is because we are using what we call nested inductive types (because in the definition of tree, tree appears again below—or nested in—the list type former). Rocq does not know what to do with assumptions of type list so it just does nothing.

Of course, this is silly and we probably still have to suffer it because of backwards compatibility. Let's see how we can do better.

First, notice that Rocq still supports this kind of induction by using fixpoints. We can actually use them interactively.

Fixpoint tree_map_id A (t : tree A) {struct t} :
  tree_map (fun x => x) t = t.tree_map_id:= forall (A : Type) (t : tree A), tree_map (fun x: A => x) t = t
A: Type
t: tree A
tree_map (fun x : A => x) t = t
Proof.tree_map_id:= forall (A : Type) (t : tree A), tree_map (fun x: A => x) t = t
A: Type
t: tree A
tree_map (fun x : A => x) t = t
  destruct t.tree_map_id:= forall (A : Type) (t : tree A), tree_map (fun x: A => x) t = t
A: Type
a: A
children: list (tree A)
tree_map (fun x : A => x) (node a children) = node a children
  cbn.tree_map_id:= forall (A : Type) (t : tree A), tree_map (fun x: A => x) t = t
A: Type
a: A
children: list (tree A)
node a (map (tree_map (fun x : A => x)) children) = node a children f_equal.tree_map_id:= forall (A : Type) (t : tree A), tree_map (fun x: A => x) t = t
A: Type
a: A
children: list (tree A)
map (tree_map (fun x : A => x)) children = children
  erewrite map_ext.tree_map_id:= forall (A : Type) (t : tree A), tree_map (fun x: A => x) t = t
A: Type
a: A
children: list (tree A)
map ?g children = children
tree_map_id:= forall (A : Type) (t : tree A), tree_map (fun x: A => x) t = t
A: Type
a: A
children: list (tree A)
forall a0 : tree A, tree_map (fun x : A => x) a0 = ?g a0
  -tree_map_id:= forall (A : Type) (t : tree A), tree_map (fun x: A => x) t = t
A: Type
a: A
children: list (tree A)
map ?g children = children apply map_id.
  -tree_map_id:= forall (A : Type) (t : tree A), tree_map (fun x: A => x) t = t
A: Type
a: A
children: list (tree A)
forall a0 : tree A, tree_map (fun x : A => x) a0 = (fun x : tree A => x) a0 cbn.tree_map_id:= forall (A : Type) (t : tree A), tree_map (fun x: A => x) t = t
A: Type
a: A
children: list (tree A)
forall a0 : tree A, tree_map (fun x : A => x) a0 = a0 intros x.tree_map_id:= forall (A : Type) (t : tree A), tree_map (fun x: A => x) t = t
A: Type
a: A
children: list (tree A)
x: tree A
tree_map (fun x0 : A => x0) x = x apply tree_map_id.
Fail Qed.The command has indeed failed with message:
Recursive definition of tree_map_id is ill-formed.
In environment
tree_map_id : forall (A : Type) (t : tree A), tree_map (fun x : A => x) t = t
A : Type
t : tree A
a : A
children : list (tree A)
a0 := a : A
children0 := children : list (tree A)
H := eq_refl : A = A
H0 := eq_refl : a0 = a0
A0 := tree A : Type
x := node a0 (map (tree_map (fun x : A => x)) children0) : A0
y := node a0 (map (tree_map (fun x : A => x)) children0) : A0
z := node a0 children0 : A0
H1 := f_equal (fun f : list (tree A) -> tree A => f (map (tree_map (fun x : A => x)) children0)) eq_refl : x = y
A1 := list (tree A) : Type
B := tree A : Type
f := node a0 : A1 -> B
x0 := map (tree_map (fun x : A => x)) children0 : A1
y0 := children0 : A1
A2 := list (tree A) : Type
x1 := map (fun x : tree A => x) children0 : A2
P := fun l : list (tree A) => l = children0 : A2 -> Prop
H2 := map_id children0 : P x1
y1 := map (tree_map (fun x : A => x)) children0 : A2
A3 := A2 : Type
x2 := x1 : A3
P0 := fun y : A2 => P y : A3 -> Prop
f0 := H2 : P0 x2
a1 := y1 : A3
A4 := A2 : Type
x3 := y1 : A4
y2 := x1 : A4
x4 : tree A
Recursive call to tree_map_id has principal argument equal to "x4" instead of one of the following variables: "children" "children0" "y0".
Recursive definition is: "fun (A : Type) (t : tree A) => match t as t0 return (tree_map (fun x : A => x) t0 = t0) with | node a children => (fun (a0 : A) (children0 : list (tree A)) => (let H : map (tree_map (fun x : A => x)) children0 = children0 := eq_ind_r (fun l : list (tree A) => l = children0) (map_id children0) (map_ext (tree_map (fun x : A => x)) (fun x : tree A => x) ((fun x : tree A => tree_map_id A x) : forall a1 : tree A, tree_map (fun x : A => x) a1 = (fun x : tree A => x) a1) children0) in (let H0 : a0 = a0 := eq_refl in (let H1 : A = A := eq_refl in (fun (_ : A = A) (_ : a0 = a0) (H2 : map (tree_map (fun x : A => x)) children0 = children0) => eq_trans (f_equal (fun f : list (tree A) -> tree A => f (map (tree_map (fun x : A => x)) children0)) eq_refl) (f_equal (node a0) H2)) H1) H0) H) : tree_map (fun x : A => x) (node a0 children0) = node a0 children0) a children end".
Abort.

Qed fails here because Rocq cannot see our fixpoint terminates. Indeed, we used a recursive call on something completely unrelated. We are only told now because Rocq only checks for termination at Qed time, and not before. There is a way to know beforehand though: the Guarded command checks that the guard condition (which verifies termination) holds up to the point where it's called.

Fixpoint tree_map_id A (t : tree A) {struct t} :
  tree_map (fun x => x) t = t.tree_map_id:= forall (A : Type) (t : tree A), tree_map (fun x: A => x) t = t
A: Type
t: tree A
tree_map (fun x : A => x) t = t
Proof.tree_map_id:= forall (A : Type) (t : tree A), tree_map (fun x: A => x) t = t
A: Type
t: tree A
tree_map (fun x : A => x) t = t
  destruct t.tree_map_id:= forall (A : Type) (t : tree A), tree_map (fun x: A => x) t = t
A: Type
a: A
children: list (tree A)
tree_map (fun x : A => x) (node a children) = node a children
  cbn.tree_map_id:= forall (A : Type) (t : tree A), tree_map (fun x: A => x) t = t
A: Type
a: A
children: list (tree A)
node a (map (tree_map (fun x : A => x)) children) = node a children f_equal.tree_map_id:= forall (A : Type) (t : tree A), tree_map (fun x: A => x) t = t
A: Type
a: A
children: list (tree A)
map (tree_map (fun x : A => x)) children = children
  Guarded.The condition holds up to here.
tree_map_id:= forall (A : Type) (t : tree A), tree_map (fun x: A => x) t = t
A: Type
a: A
children: list (tree A)
map (tree_map (fun x : A => x)) children = children
  erewrite map_ext_in.tree_map_id:= forall (A : Type) (t : tree A), tree_map (fun x: A => x) t = t
A: Type
a: A
children: list (tree A)
map ?g children = children
tree_map_id:= forall (A : Type) (t : tree A), tree_map (fun x: A => x) t = t
A: Type
a: A
children: list (tree A)
forall a0 : tree A, In a0 children -> tree_map (fun x : A => x) a0 = ?g a0
  -tree_map_id:= forall (A : Type) (t : tree A), tree_map (fun x: A => x) t = t
A: Type
a: A
children: list (tree A)
map ?g children = children apply map_id.
  -tree_map_id:= forall (A : Type) (t : tree A), tree_map (fun x: A => x) t = t
A: Type
a: A
children: list (tree A)
forall a0 : tree A, In a0 children -> tree_map (fun x : A => x) a0 = (fun x : tree A => x) a0 Guarded.The condition holds up to here.
tree_map_id:= forall (A : Type) (t : tree A), tree_map (fun x: A => x) t = t
A: Type
a: A
children: list (tree A)
forall a0 : tree A, In a0 children -> tree_map (fun x : A => x) a0 = (fun x : tree A => x) a0 cbn.tree_map_id:= forall (A : Type) (t : tree A), tree_map (fun x: A => x) t = t
A: Type
a: A
children: list (tree A)
forall a0 : tree A, In a0 children -> tree_map (fun x : A => x) a0 = a0 intros x h.tree_map_id:= forall (A : Type) (t : tree A), tree_map (fun x: A => x) t = t
A: Type
a: A
children: list (tree A)
x: tree A
h: In x children
tree_map (fun x0 : A => x0) x = x Guarded.The condition holds up to here.
tree_map_id:= forall (A : Type) (t : tree A), tree_map (fun x: A => x) t = t
A: Type
a: A
children: list (tree A)
x: tree A
h: In x children
tree_map (fun x0 : A => x0) x = x apply tree_map_id.
Fail Qed.The command has indeed failed with message:
Recursive definition of tree_map_id is ill-formed.
In environment
tree_map_id : forall (A : Type) (t : tree A), tree_map (fun x : A => x) t = t
A : Type
t : tree A
a : A
children : list (tree A)
a0 := a : A
children0 := children : list (tree A)
H := eq_refl : A = A
H0 := eq_refl : a0 = a0
A0 := tree A : Type
x := node a0 (map (tree_map (fun x : A => x)) children0) : A0
y := node a0 (map (tree_map (fun x : A => x)) children0) : A0
z := node a0 children0 : A0
H1 := f_equal (fun f : list (tree A) -> tree A => f (map (tree_map (fun x : A => x)) children0)) eq_refl : x = y
A1 := list (tree A) : Type
B := tree A : Type
f := node a0 : A1 -> B
x0 := map (tree_map (fun x : A => x)) children0 : A1
y0 := children0 : A1
A2 := list (tree A) : Type
x1 := map (fun x : tree A => x) children0 : A2
P := fun l : list (tree A) => l = children0 : A2 -> Prop
H2 := map_id children0 : P x1
y1 := map (tree_map (fun x : A => x)) children0 : A2
A3 := A2 : Type
x2 := x1 : A3
P0 := fun y : A2 => P y : A3 -> Prop
f0 := H2 : P0 x2
a1 := y1 : A3
A4 := A2 : Type
x3 := y1 : A4
y2 := x1 : A4
x4 : tree A
h : In x4 children0
Recursive call to tree_map_id has principal argument equal to "x4" instead of one of the following variables: "children" "children0" "y0".
Recursive definition is: "fun (A : Type) (t : tree A) => match t as t0 return (tree_map (fun x : A => x) t0 = t0) with | node a children => (fun (a0 : A) (children0 : list (tree A)) => (let H : map (tree_map (fun x : A => x)) children0 = children0 := eq_ind_r (fun l : list (tree A) => l = children0) (map_id children0) (map_ext_in (tree_map (fun x : A => x)) (fun x : tree A => x) children0 ((fun (x : tree A) (_ : In x children0) => tree_map_id A x) : forall a1 : tree A, In a1 children0 -> tree_map (fun x : A => x) a1 = (fun x : tree A => x) a1)) in (let H0 : a0 = a0 := eq_refl in (let H1 : A = A := eq_refl in (fun (_ : A = A) (_ : a0 = a0) (H2 : map (tree_map (fun x : A => x)) children0 = children0) => eq_trans (f_equal (fun f : list (tree A) -> tree A => f (map (tree_map (fun x : A => x)) children0)) eq_refl) (f_equal (node a0) H2)) H1) H0) H) : tree_map (fun x : A => x) (node a0 children0) = node a0 children0) a children end".
Abort.

This time it should actually work because morally we only use recursive calls on elements inside the list, but Rocq doesn't know it.

We in fact need to be able to recurse on the list, so we the same way we nested inductive types, we need to nest fixpoints. For this we can use the fix tactic which introduces a fixed point. We need to revert the argument on which we want to recurse (to put it back into the goal) and then fix aux 1 will introduce a new hypothesis named aux corresponding to potential recursive calls.

Fixpoint tree_map_id A (t : tree A) {struct t} :
  tree_map (fun x => x) t = t.tree_map_id:= forall (A : Type) (t : tree A), tree_map (fun x: A => x) t = t
A: Type
t: tree A
tree_map (fun x : A => x) t = t
Proof.tree_map_id:= forall (A : Type) (t : tree A), tree_map (fun x: A => x) t = t
A: Type
t: tree A
tree_map (fun x : A => x) t = t
  destruct t.tree_map_id:= forall (A : Type) (t : tree A), tree_map (fun x: A => x) t = t
A: Type
a: A
children: list (tree A)
tree_map (fun x : A => x) (node a children) = node a children
  cbn.tree_map_id:= forall (A : Type) (t : tree A), tree_map (fun x: A => x) t = t
A: Type
a: A
children: list (tree A)
node a (map (tree_map (fun x : A => x)) children) = node a children f_equal.tree_map_id:= forall (A : Type) (t : tree A), tree_map (fun x: A => x) t = t
A: Type
a: A
children: list (tree A)
map (tree_map (fun x : A => x)) children = children
  revert children.tree_map_id:= forall (A : Type) (t : tree A), tree_map (fun x: A => x) t = t
A: Type
a: A
forall children : list (tree A), map (tree_map (fun x : A => x)) children = children fix aux 1.tree_map_id:= forall (A : Type) (t : tree A), tree_map (fun x: A => x) t = t
A: Type
a: A
aux:= forall children : list (tree A), map (tree_map (fun x: A => x)) children = children
forall children : list (tree A), map (tree_map (fun x : A => x)) children = children intro l.tree_map_id:= forall (A : Type) (t : tree A), tree_map (fun x: A => x) t = t
A: Type
a: A
aux:= forall children : list (tree A), map (tree_map (fun x: A => x)) children = children
l: list (tree A)
map (tree_map (fun x : A => x)) l = l
  destruct l as [| x l].tree_map_id:= forall (A : Type) (t : tree A), tree_map (fun x: A => x) t = t
A: Type
a: A
aux:= forall children : list (tree A), map (tree_map (fun x: A => x)) children = children
map (tree_map (fun x : A => x)) [] = []
tree_map_id:= forall (A : Type) (t : tree A), tree_map (fun x: A => x) t = t
A: Type
a: A
aux:= forall children : list (tree A), map (tree_map (fun x: A => x)) children = children
x: tree A
l: list (tree A)
map (tree_map (fun x0 : A => x0)) (x :: l) = x :: l
  -tree_map_id:= forall (A : Type) (t : tree A), tree_map (fun x: A => x) t = t
A: Type
a: A
aux:= forall children : list (tree A), map (tree_map (fun x: A => x)) children = children
map (tree_map (fun x : A => x)) [] = [] reflexivity.
  -tree_map_id:= forall (A : Type) (t : tree A), tree_map (fun x: A => x) t = t
A: Type
a: A
aux:= forall children : list (tree A), map (tree_map (fun x: A => x)) children = children
x: tree A
l: list (tree A)
map (tree_map (fun x0 : A => x0)) (x :: l) = x :: l cbn.tree_map_id:= forall (A : Type) (t : tree A), tree_map (fun x: A => x) t = t
A: Type
a: A
aux:= forall children : list (tree A), map (tree_map (fun x: A => x)) children = children
x: tree A
l: list (tree A)
tree_map (fun x0 : A => x0) x :: map (tree_map (fun x0 : A => x0)) l = x :: l f_equal.tree_map_id:= forall (A : Type) (t : tree A), tree_map (fun x: A => x) t = t
A: Type
a: A
aux:= forall children : list (tree A), map (tree_map (fun x: A => x)) children = children
x: tree A
l: list (tree A)
tree_map (fun x0 : A => x0) x = x
tree_map_id:= forall (A : Type) (t : tree A), tree_map (fun x: A => x) t = t
A: Type
a: A
aux:= forall children : list (tree A), map (tree_map (fun x: A => x)) children = children
x: tree A
l: list (tree A)
map (tree_map (fun x0 : A => x0)) l = l
    +tree_map_id:= forall (A : Type) (t : tree A), tree_map (fun x: A => x) t = t
A: Type
a: A
aux:= forall children : list (tree A), map (tree_map (fun x: A => x)) children = children
x: tree A
l: list (tree A)
tree_map (fun x0 : A => x0) x = x apply tree_map_id.
    +tree_map_id:= forall (A : Type) (t : tree A), tree_map (fun x: A => x) t = t
A: Type
a: A
aux:= forall children : list (tree A), map (tree_map (fun x: A => x)) children = children
x: tree A
l: list (tree A)
map (tree_map (fun x0 : A => x0)) l = l apply aux.
Qed.tree_map_id is defined

This was rather painful because we had to manually ensure that Rocq recognises the proof as structurally recursive. Ideally we would like to be able to do induction like always. In order to do so, we are going to use fixpoints to prove our own induction principle for trees.

We'll start by copying the type of tree_ind.

Check tree_ind.tree_ind
     : forall (A : Type) (P : tree A -> Prop), (forall (a : A) (children : list (tree A)), P (node a children)) -> forall t : tree A, P t

We then add an induction hypothesis for all elements of the children list. Note that we again have to use fix to be able to prove it, but we only have to go through that once and for all.

Lemma good_tree_ind' :
  forall A (P : tree A -> Prop),
    (forall a l, (forall x, In x l -> P x) -> P (node a l)) ->
    forall t, P t.forall (A : Type) (P : tree A -> Prop), (forall (a : A) (l : list (tree A)), (forall x : tree A, In x l -> P x) -> P (node a l)) -> forall t : tree A, P t
Proof.forall (A : Type) (P : tree A -> Prop), (forall (a : A) (l : list (tree A)), (forall x : tree A, In x l -> P x) -> P (node a l)) -> forall t : tree A, P t
  intros A P h.A: Type
P: tree A -> Prop
h:= forall (a : A) (l : list (tree A)), (forall x: tree A, In x l -> P x) -> P (node a l)
forall t : tree A, P t
  fix ind 1.A: Type
P: tree A -> Prop
h:= forall (a : A) (l : list (tree A)), (forall x: tree A, In x l -> P x) -> P (node a l)
ind:= forall t: tree A, P t
forall t : tree A, P t
  intros [ a l ].A: Type
P: tree A -> Prop
h:= forall (a : A) (l : list (tree A)), (forall x: tree A, In x l -> P x) -> P (node a l)
ind:= forall t: tree A, P t
a: A
l: list (tree A)
P (node a l)
  apply h.A: Type
P: tree A -> Prop
h:= forall (a : A) (l : list (tree A)), (forall x: tree A, In x l -> P x) -> P (node a l)
ind:= forall t: tree A, P t
a: A
l: list (tree A)
forall x : tree A, In x l -> P x
  revert l.A: Type
P: tree A -> Prop
h:= forall (a : A) (l : list (tree A)), (forall x: tree A, In x l -> P x) -> P (node a l)
ind:= forall t: tree A, P t
a: A
forall (l : list (tree A)) (x : tree A), In x l -> P x fix aux 1.A: Type
P: tree A -> Prop
h:= forall (a : A) (l : list (tree A)), (forall x: tree A, In x l -> P x) -> P (node a l)
ind:= forall t: tree A, P t
a: A
aux:= forall (l : list (tree A)) (x: tree A), In x l -> P x
forall (l : list (tree A)) (x : tree A), In x l -> P x intro l.A: Type
P: tree A -> Prop
h:= forall (a : A) (l : list (tree A)), (forall x: tree A, In x l -> P x) -> P (node a l)
ind:= forall t: tree A, P t
a: A
aux:= forall (l : list (tree A)) (x: tree A), In x l -> P x
l: list (tree A)
forall x : tree A, In x l -> P x
  destruct l as [| x l].A: Type
P: tree A -> Prop
h:= forall (a : A) (l : list (tree A)), (forall x: tree A, In x l -> P x) -> P (node a l)
ind:= forall t: tree A, P t
a: A
aux:= forall (l : list (tree A)) (x: tree A), In x l -> P x
forall x : tree A, In x [] -> P x
A: Type
P: tree A -> Prop
h:= forall (a : A) (l : list (tree A)), (forall x: tree A, In x l -> P x) -> P (node a l)
ind:= forall t: tree A, P t
a: A
aux:= forall (l : list (tree A)) (x: tree A), In x l -> P x
x: tree A
l: list (tree A)
forall x0 : tree A, In x0 (x :: l) -> P x0
  -A: Type
P: tree A -> Prop
h:= forall (a : A) (l : list (tree A)), (forall x: tree A, In x l -> P x) -> P (node a l)
ind:= forall t: tree A, P t
a: A
aux:= forall (l : list (tree A)) (x: tree A), In x l -> P x
forall x : tree A, In x [] -> P x intros y Hy.A: Type
P: tree A -> Prop
h:= forall (a : A) (l : list (tree A)), (forall x: tree A, In x l -> P x) -> P (node a l)
ind:= forall t: tree A, P t
a: A
aux:= forall (l : list (tree A)) (x: tree A), In x l -> P x
y: tree A
Hy: In y []
P y destruct Hy.
  -A: Type
P: tree A -> Prop
h:= forall (a : A) (l : list (tree A)), (forall x: tree A, In x l -> P x) -> P (node a l)
ind:= forall t: tree A, P t
a: A
aux:= forall (l : list (tree A)) (x: tree A), In x l -> P x
x: tree A
l: list (tree A)
forall x0 : tree A, In x0 (x :: l) -> P x0 intros y Hy.A: Type
P: tree A -> Prop
h:= forall (a : A) (l : list (tree A)), (forall x: tree A, In x l -> P x) -> P (node a l)
ind:= forall t: tree A, P t
a: A
aux:= forall (l : list (tree A)) (x: tree A), In x l -> P x
x: tree A
l: list (tree A)
y: tree A
Hy:= In y (x :: l)
P y
    destruct Hy as [ <- | Hy].A: Type
P: tree A -> Prop
h:= forall (a : A) (l : list (tree A)), (forall x: tree A, In x l -> P x) -> P (node a l)
ind:= forall t: tree A, P t
a: A
aux:= forall (l : list (tree A)) (x: tree A), In x l -> P x
x: tree A
l: list (tree A)
P x
A: Type
P: tree A -> Prop
h:= forall (a : A) (l : list (tree A)), (forall x: tree A, In x l -> P x) -> P (node a l)
ind:= forall t: tree A, P t
a: A
aux:= forall (l : list (tree A)) (x: tree A), In x l -> P x
x: tree A
l: list (tree A)
y: tree A
Hy: In y l
P y
    +A: Type
P: tree A -> Prop
h:= forall (a : A) (l : list (tree A)), (forall x: tree A, In x l -> P x) -> P (node a l)
ind:= forall t: tree A, P t
a: A
aux:= forall (l : list (tree A)) (x: tree A), In x l -> P x
x: tree A
l: list (tree A)
P x apply ind.
    +A: Type
P: tree A -> Prop
h:= forall (a : A) (l : list (tree A)), (forall x: tree A, In x l -> P x) -> P (node a l)
ind:= forall t: tree A, P t
a: A
aux:= forall (l : list (tree A)) (x: tree A), In x l -> P x
x: tree A
l: list (tree A)
y: tree A
Hy: In y l
P y apply (aux l).A: Type
P: tree A -> Prop
h:= forall (a : A) (l : list (tree A)), (forall x: tree A, In x l -> P x) -> P (node a l)
ind:= forall t: tree A, P t
a: A
aux:= forall (l : list (tree A)) (x: tree A), In x l -> P x
x: tree A
l: list (tree A)
y: tree A
Hy: In y l
In y l assumption.
Qed.good_tree_ind' is defined

Instead of using In, we can also use the Forall predicate.

Print Forall.Inductive Forall (A : Type) (P : A -> Prop) : list A -> Prop :=  Forall_nil : Forall P [] | Forall_cons : forall (x : A) (l : list A), P x -> Forall P l -> Forall P (x :: l).

Arguments Forall [A]%type_scope P%function_scope _%list_scopeArguments Forall_nil [A]%type_scope P%function_scopeArguments Forall_cons [A]%type_scope [P]%function_scope x [l]%list_scope _ _

Lemma good_tree_ind :
  forall A (P : tree A -> Prop),
    (forall a l, Forall P l -> P (node a l)) ->
    forall t, P t.forall (A : Type) (P : tree A -> Prop), (forall (a : A) (l : list (tree A)), Forall P l -> P (node a l)) -> forall t : tree A, P t
Proof.forall (A : Type) (P : tree A -> Prop), (forall (a : A) (l : list (tree A)), Forall P l -> P (node a l)) -> forall t : tree A, P t
  intros A P h.A: Type
P: tree A -> Prop
h:= forall (a : A) (l: list (tree A)), Forall P l -> P (node a l)
forall t : tree A, P t
  fix ind 1.A: Type
P: tree A -> Prop
h:= forall (a : A) (l: list (tree A)), Forall P l -> P (node a l)
ind:= forall t: tree A, P t
forall t : tree A, P t
  intros [ a l ].A: Type
P: tree A -> Prop
h:= forall (a : A) (l: list (tree A)), Forall P l -> P (node a l)
ind:= forall t: tree A, P t
a: A
l: list (tree A)
P (node a l)
  apply h.A: Type
P: tree A -> Prop
h:= forall (a : A) (l: list (tree A)), Forall P l -> P (node a l)
ind:= forall t: tree A, P t
a: A
l: list (tree A)
Forall P l
  revert l.A: Type
P: tree A -> Prop
h:= forall (a : A) (l: list (tree A)), Forall P l -> P (node a l)
ind:= forall t: tree A, P t
a: A
forall l : list (tree A), Forall P l fix aux 1.A: Type
P: tree A -> Prop
h:= forall (a : A) (l: list (tree A)), Forall P l -> P (node a l)
ind:= forall t: tree A, P t
a: A
aux:= forall l: list (tree A), Forall P l
forall l : list (tree A), Forall P l intro l.A: Type
P: tree A -> Prop
h:= forall (a : A) (l: list (tree A)), Forall P l -> P (node a l)
ind:= forall t: tree A, P t
a: A
aux:= forall l: list (tree A), Forall P l
l: list (tree A)
Forall P l
  destruct l as [| x l].A: Type
P: tree A -> Prop
h:= forall (a : A) (l: list (tree A)), Forall P l -> P (node a l)
ind:= forall t: tree A, P t
a: A
aux:= forall l: list (tree A), Forall P l
Forall P []
A: Type
P: tree A -> Prop
h:= forall (a : A) (l: list (tree A)), Forall P l -> P (node a l)
ind:= forall t: tree A, P t
a: A
aux:= forall l: list (tree A), Forall P l
x: tree A
l: list (tree A)
Forall P (x :: l)
  -A: Type
P: tree A -> Prop
h:= forall (a : A) (l: list (tree A)), Forall P l -> P (node a l)
ind:= forall t: tree A, P t
a: A
aux:= forall l: list (tree A), Forall P l
Forall P [] constructor.
  -A: Type
P: tree A -> Prop
h:= forall (a : A) (l: list (tree A)), Forall P l -> P (node a l)
ind:= forall t: tree A, P t
a: A
aux:= forall l: list (tree A), Forall P l
x: tree A
l: list (tree A)
Forall P (x :: l) constructor.A: Type
P: tree A -> Prop
h:= forall (a : A) (l: list (tree A)), Forall P l -> P (node a l)
ind:= forall t: tree A, P t
a: A
aux:= forall l: list (tree A), Forall P l
x: tree A
l: list (tree A)
P x
A: Type
P: tree A -> Prop
h:= forall (a : A) (l: list (tree A)), Forall P l -> P (node a l)
ind:= forall t: tree A, P t
a: A
aux:= forall l: list (tree A), Forall P l
x: tree A
l: list (tree A)
Forall P l
    +A: Type
P: tree A -> Prop
h:= forall (a : A) (l: list (tree A)), Forall P l -> P (node a l)
ind:= forall t: tree A, P t
a: A
aux:= forall l: list (tree A), Forall P l
x: tree A
l: list (tree A)
P x apply ind.
    +A: Type
P: tree A -> Prop
h:= forall (a : A) (l: list (tree A)), Forall P l -> P (node a l)
ind:= forall t: tree A, P t
a: A
aux:= forall l: list (tree A), Forall P l
x: tree A
l: list (tree A)
Forall P l apply aux.
Qed.good_tree_ind is defined

We can now use this induction principle by hand to prove tree_map_id again. We make use of the pattern tactic, pattern t attempts to rehape the goal so it has the form P t for some P.

Lemma tree_map_id_again :
  forall A (t : tree A),
    tree_map (fun x => x) t = t.forall (A : Type) (t : tree A), tree_map (fun x : A => x) t = t
Proof.forall (A : Type) (t : tree A), tree_map (fun x : A => x) t = t
  intros A t.A: Type
t: tree A
tree_map (fun x : A => x) t = t
  pattern t.A: Type
t: tree A
(fun t0 : tree A => tree_map (fun x : A => x) t0 = t0) t
  apply good_tree_ind.A: Type
t: tree A
forall (a : A) (l : list (tree A)), Forall (fun t0 : tree A => tree_map (fun x : A => x) t0 = t0) l -> tree_map (fun x : A => x) (node a l) = node a l
  clear t.A: Type
forall (a : A) (l : list (tree A)), Forall (fun t : tree A => tree_map (fun x : A => x) t = t) l -> tree_map (fun x : A => x) (node a l) = node a l intros a l h.A: Type
a: A
l: list (tree A)
h:= Forall (fun t : tree A => tree_map (fun x: A => x) t = t) l
tree_map (fun x : A => x) (node a l) = node a l cbn.A: Type
a: A
l: list (tree A)
h:= Forall (fun t : tree A => tree_map (fun x: A => x) t = t) l
node a (map (tree_map (fun x : A => x)) l) = node a l f_equal.A: Type
a: A
l: list (tree A)
h:= Forall (fun t : tree A => tree_map (fun x: A => x) t = t) l
map (tree_map (fun x : A => x)) l = l
  induction h as [| tr l e h ih].A: Type
a: A
map (tree_map (fun x : A => x)) [] = []
A: Type
a: A
tr: tree A
l: list (tree A)
e:= tree_map (fun x: A => x) tr = tr
h:= Forall (fun t : tree A => tree_map (fun x: A => x) t = t) l
ih:= map (tree_map (fun x: A => x)) l = l
map (tree_map (fun x : A => x)) (tr :: l) = tr :: l
  -A: Type
a: A
map (tree_map (fun x : A => x)) [] = [] reflexivity.
  -A: Type
a: A
tr: tree A
l: list (tree A)
e:= tree_map (fun x: A => x) tr = tr
h:= Forall (fun t : tree A => tree_map (fun x: A => x) t = t) l
ih:= map (tree_map (fun x: A => x)) l = l
map (tree_map (fun x : A => x)) (tr :: l) = tr :: l cbn.A: Type
a: A
tr: tree A
l: list (tree A)
e:= tree_map (fun x: A => x) tr = tr
h:= Forall (fun t : tree A => tree_map (fun x: A => x) t = t) l
ih:= map (tree_map (fun x: A => x)) l = l
tree_map (fun x : A => x) tr :: map (tree_map (fun x : A => x)) l = tr :: l f_equal.A: Type
a: A
tr: tree A
l: list (tree A)
e:= tree_map (fun x: A => x) tr = tr
h:= Forall (fun t : tree A => tree_map (fun x: A => x) t = t) l
ih:= map (tree_map (fun x: A => x)) l = l
tree_map (fun x : A => x) tr = tr
A: Type
a: A
tr: tree A
l: list (tree A)
e:= tree_map (fun x: A => x) tr = tr
h:= Forall (fun t : tree A => tree_map (fun x: A => x) t = t) l
ih:= map (tree_map (fun x: A => x)) l = l
map (tree_map (fun x : A => x)) l = l
    +A: Type
a: A
tr: tree A
l: list (tree A)
e:= tree_map (fun x: A => x) tr = tr
h:= Forall (fun t : tree A => tree_map (fun x: A => x) t = t) l
ih:= map (tree_map (fun x: A => x)) l = l
tree_map (fun x : A => x) tr = tr apply e.
    +A: Type
a: A
tr: tree A
l: list (tree A)
e:= tree_map (fun x: A => x) tr = tr
h:= Forall (fun t : tree A => tree_map (fun x: A => x) t = t) l
ih:= map (tree_map (fun x: A => x)) l = l
map (tree_map (fun x : A => x)) l = l apply ih.
Qed.tree_map_id_again is defined

In fact, we can still use the induction tactic to do it. And it's much nicer. This is done with the special using keyword as below.

Lemma tree_map_id_again' :
  forall A (t : tree A),
    tree_map (fun x => x) t = t.forall (A : Type) (t : tree A), tree_map (fun x : A => x) t = t
Proof.forall (A : Type) (t : tree A), tree_map (fun x : A => x) t = t
  intros A t.A: Type
t: tree A
tree_map (fun x : A => x) t = t
  induction t as [a l ihl] using good_tree_ind.A: Type
a: A
l: list (tree A)
ihl:= Forall (fun t : tree A => tree_map (fun x: A => x) t = t) l
tree_map (fun x : A => x) (node a l) = node a l
  cbn.A: Type
a: A
l: list (tree A)
ihl:= Forall (fun t : tree A => tree_map (fun x: A => x) t = t) l
node a (map (tree_map (fun x : A => x)) l) = node a l f_equal.A: Type
a: A
l: list (tree A)
ihl:= Forall (fun t : tree A => tree_map (fun x: A => x) t = t) l
map (tree_map (fun x : A => x)) l = l induction ihl.A: Type
a: A
map (tree_map (fun x : A => x)) [] = []
A: Type
a: A
x: tree A
l: list (tree A)
H:= tree_map (fun x: A => x) x = x
ihl:= Forall (fun t : tree A => tree_map (fun x: A => x) t = t) l
IHihl:= map (tree_map (fun x: A => x)) l = l
map (tree_map (fun x0 : A => x0)) (x :: l) = x :: l
  -A: Type
a: A
map (tree_map (fun x : A => x)) [] = [] reflexivity.
  -A: Type
a: A
x: tree A
l: list (tree A)
H:= tree_map (fun x: A => x) x = x
ihl:= Forall (fun t : tree A => tree_map (fun x: A => x) t = t) l
IHihl:= map (tree_map (fun x: A => x)) l = l
map (tree_map (fun x0 : A => x0)) (x :: l) = x :: l cbn.A: Type
a: A
x: tree A
l: list (tree A)
H:= tree_map (fun x: A => x) x = x
ihl:= Forall (fun t : tree A => tree_map (fun x: A => x) t = t) l
IHihl:= map (tree_map (fun x: A => x)) l = l
tree_map (fun x0 : A => x0) x :: map (tree_map (fun x0 : A => x0)) l = x :: l f_equal.A: Type
a: A
x: tree A
l: list (tree A)
H:= tree_map (fun x: A => x) x = x
ihl:= Forall (fun t : tree A => tree_map (fun x: A => x) t = t) l
IHihl:= map (tree_map (fun x: A => x)) l = l
tree_map (fun x0 : A => x0) x = x
A: Type
a: A
x: tree A
l: list (tree A)
H:= tree_map (fun x: A => x) x = x
ihl:= Forall (fun t : tree A => tree_map (fun x: A => x) t = t) l
IHihl:= map (tree_map (fun x: A => x)) l = l
map (tree_map (fun x0 : A => x0)) l = l all: assumption.
Qed.tree_map_id_again' is defined

Size recursion

We have already seen size induction earlier. We can use the same idea to prove a size recursion principle:

Lemma size_recursion (X : Type) (size : X -> nat) (P : X -> Type) :
  (forall x, (forall y, size y < size x -> P y) -> P x) ->
  forall x, P x.X: Type
size: X -> nat
P: X -> Type
(forall x : X, (forall y : X, size y < size x -> P y) -> P x) -> forall x : X, P x
Proof.X: Type
size: X -> nat
P: X -> Type
(forall x : X, (forall y : X, size y < size x -> P y) -> P x) -> forall x : X, P x
  intros D x.X: Type
size: X -> nat
P: X -> Type
D:= forall x : X, (forall y: X, size y < size x -> P y) -> P x
x: X
P x apply D.X: Type
size: X -> nat
P: X -> Type
D:= forall x : X, (forall y: X, size y < size x -> P y) -> P x
x: X
forall y : X, size y < size x -> P y
  cut (forall n y, size y < n -> P y).X: Type
size: X -> nat
P: X -> Type
D:= forall x : X, (forall y: X, size y < size x -> P y) -> P x
x: X
(forall (n : nat) (y : X), size y < n -> P y) -> forall y : X, size y < size x -> P y
X: Type
size: X -> nat
P: X -> Type
D:= forall x : X, (forall y: X, size y < size x -> P y) -> P x
x: X
forall (n : nat) (y : X), size y < n -> P y
  {X: Type
size: X -> nat
P: X -> Type
D:= forall x : X, (forall y: X, size y < size x -> P y) -> P x
x: X
(forall (n : nat) (y : X), size y < n -> P y) -> forall y : X, size y < size x -> P y eauto. }X: Type
size: X -> nat
P: X -> Type
D:= forall x : X, (forall y: X, size y < size x -> P y) -> P x
x: X
forall (n : nat) (y : X), size y < n -> P y
  clear x.X: Type
size: X -> nat
P: X -> Type
D:= forall x : X, (forall y: X, size y < size x -> P y) -> P x
forall (n : nat) (y : X), size y < n -> P y intros n y E.X: Type
size: X -> nat
P: X -> Type
D:= forall x : X, (forall y: X, size y < size x -> P y) -> P x
n: nat
y: X
E: size y < n
P y
  induction n as [| n ih] in y, E |- *.X: Type
size: X -> nat
P: X -> Type
D:= forall x : X, (forall y: X, size y < size x -> P y) -> P x
y: X
E: size y < 0
P y
X: Type
size: X -> nat
P: X -> Type
D:= forall x : X, (forall y: X, size y < size x -> P y) -> P x
n: nat
y: X
E: size y < S n
ih:= forall y: X, size y < n -> P y
P y
  -X: Type
size: X -> nat
P: X -> Type
D:= forall x : X, (forall y: X, size y < size x -> P y) -> P x
y: X
E: size y < 0
P y lia.
  -X: Type
size: X -> nat
P: X -> Type
D:= forall x : X, (forall y: X, size y < size x -> P y) -> P x
n: nat
y: X
E: size y < S n
ih:= forall y: X, size y < n -> P y
P y apply D.X: Type
size: X -> nat
P: X -> Type
D:= forall x : X, (forall y: X, size y < size x -> P y) -> P x
n: nat
y: X
E: size y < S n
ih:= forall y: X, size y < n -> P y
forall y0 : X, size y0 < size y -> P y0 intros x F.X: Type
size: X -> nat
P: X -> Type
D:= forall x : X, (forall y: X, size y < size x -> P y) -> P x
n: nat
y: X
E: size y < S n
ih:= forall y: X, size y < n -> P y
x: X
F: size x < size y
P x apply ih.X: Type
size: X -> nat
P: X -> Type
D:= forall x : X, (forall y: X, size y < size x -> P y) -> P x
n: nat
y: X
E: size y < S n
ih:= forall y: X, size y < n -> P y
x: X
F: size x < size y
size x < n lia.
Defined.size_recursion is defined

Well-founded induction

The last topic is about doing induction / recursion along any well-founded order. We define well-foundedness of an order on a point as the so-called accessibility predicate.

Section Well_founded.

We work with a type and a relation on it. Note. We do not require this relation to be an equivalence relation or anything actually. This isn't necessary.

  Context {A : Type}.A is declared
  Context (R : A -> A -> Prop).R is declared

A point x is accessible when all its predecessors in the relation are accessibe as well.

  Inductive Acc (x : A) : Prop :=
    Acc_intro : (forall y, R y x -> Acc y) -> Acc x.Acc is defined
Acc_rect is defined
Acc_ind is defined
Acc_rec is defined
Acc_sind is defined

  Fact Acc_iff x :
    Acc x <-> forall y, R y x -> Acc y.A: Type
R: A -> A -> Prop
x: A
Acc x <-> (forall y : A, R y x -> Acc y)
  Proof.A: Type
R: A -> A -> Prop
x: A
Acc x <-> (forall y : A, R y x -> Acc y)
    split.A: Type
R: A -> A -> Prop
x: A
Acc x -> forall y : A, R y x -> Acc y
A: Type
R: A -> A -> Prop
x: A
(forall y : A, R y x -> Acc y) -> Acc x
    -A: Type
R: A -> A -> Prop
x: A
Acc x -> forall y : A, R y x -> Acc y intros [h].A: Type
R: A -> A -> Prop
x: A
h:= forall y: A, R y x -> Acc y
forall y : A, R y x -> Acc y exact h.
    -A: Type
R: A -> A -> Prop
x: A
(forall y : A, R y x -> Acc y) -> Acc x intros.A: Type
R: A -> A -> Prop
x: A
H:= forall y: A, R y x -> Acc y
Acc x constructor.A: Type
R: A -> A -> Prop
x: A
H:= forall y: A, R y x -> Acc y
forall y : A, R y x -> Acc y assumption.
  Qed.Acc_iff is defined

End Well_founded.

Now behold the return of the subsingleton criterion! Acc indeed verifies it: it has exactly one constructor Acc_intro which itself has two arguments, x : A and h : forall y, R y x -> Acc y. The first one is a parameter so it doesn't count, and the second one is a proof (because, remember, ∀ quantifiers ending in Prop land in Prop as well).

This means that we get an induction principle with a motive in Type:

Check Acc_rect.Acc_rect
     : forall (R : ?A -> ?A -> Prop) (P : ?A -> Type), (forall x : ?A, (forall y : ?A, R y x -> Acc R y) -> (forall y : ?A, R y x -> P y) -> P x) -> forall x : ?A, Acc R x -> P x
where
?A : [ |- Type]

It says that when proving P x for accessible x, one can assume P y for any R-smaller y.

We can prove that accessible points are not contained in loops:

Fact exercise_loop (X : Type) (R : X -> X -> Prop) x :
  Acc R x ->
  ~ exists y, R x y /\ R y x.X: Type
R: X -> X -> Prop
x: X
Acc R x -> ~ (exists y : X, R x y /\ R y x)
Proof.X: Type
R: X -> X -> Prop
x: X
Acc R x -> ~ (exists y : X, R x y /\ R y x)
  intros H.X: Type
R: X -> X -> Prop
x: X
H: Acc R x
~ (exists y : X, R x y /\ R y x)
  induction H as [x H ih].X: Type
R: X -> X -> Prop
x: X
H:= forall y: X, R y x -> Acc R y
ih:= forall y : X, R y x -> ~ (exists y0: X, R y y0 /\ R y0 y)
~ (exists y : X, R x y /\ R y x)
  firstorder.
Qed.exercise_loop is defined

And that accessible points are not the start of an infinite descending path.

Fact exercise_chain (X : Type) (R : X -> X -> Prop) x :
  Acc R x ->
  ~ exists (path : nat -> X),
    path 0 = x /\ forall n, R (path (S n)) (path n).X: Type
R: X -> X -> Prop
x: X
Acc R x -> ~ (exists path : nat -> X, path 0 = x /\ (forall n : nat, R (path (S n)) (path n)))
Proof.X: Type
R: X -> X -> Prop
x: X
Acc R x -> ~ (exists path : nat -> X, path 0 = x /\ (forall n : nat, R (path (S n)) (path n)))
  intros H.X: Type
R: X -> X -> Prop
x: X
H: Acc R x
~ (exists path : nat -> X, path 0 = x /\ (forall n : nat, R (path (S n)) (path n)))
  induction H as [x H ih].X: Type
R: X -> X -> Prop
x: X
H:= forall y: X, R y x -> Acc R y
ih:= forall y : X, R y x -> ~ (exists path : nat -> X, path 0 = y /\ (forall n: nat, R (path (S n)) (path n)))
~ (exists path : nat -> X, path 0 = x /\ (forall n : nat, R (path (S n)) (path n)))
  intros (path & H1 & H2).X: Type
R: X -> X -> Prop
x: X
H:= forall y: X, R y x -> Acc R y
ih:= forall y : X, R y x -> ~ (exists path : nat -> X, path 0 = y /\ (forall n: nat, R (path (S n)) (path n)))
path: nat -> X
H1: path 0 = x
H2:= forall n: nat, R (path (S n)) (path n)
False subst.X: Type
R: X -> X -> Prop
path: nat -> X
ih:= forall y : X, R y (path 0) -> ~ (exists path : nat -> X, path 0 = y /\ (forall n: nat, R (path (S n)) (path n)))
H:= forall y: X, R y (path 0) -> Acc R y
H2:= forall n: nat, R (path (S n)) (path n)
False
  eapply ih.X: Type
R: X -> X -> Prop
path: nat -> X
ih:= forall y : X, R y (path 0) -> ~ (exists path : nat -> X, path 0 = y /\ (forall n: nat, R (path (S n)) (path n)))
H:= forall y: X, R y (path 0) -> Acc R y
H2:= forall n: nat, R (path (S n)) (path n)
R ?y (path 0)
X: Type
R: X -> X -> Prop
path: nat -> X
ih:= forall y : X, R y (path 0) -> ~ (exists path : nat -> X, path 0 = y /\ (forall n: nat, R (path (S n)) (path n)))
H:= forall y: X, R y (path 0) -> Acc R y
H2:= forall n: nat, R (path (S n)) (path n)
exists path0 : nat -> X, path0 0 = ?y /\ (forall n : nat, R (path0 (S n)) (path0 n))
  -X: Type
R: X -> X -> Prop
path: nat -> X
ih:= forall y : X, R y (path 0) -> ~ (exists path : nat -> X, path 0 = y /\ (forall n: nat, R (path (S n)) (path n)))
H:= forall y: X, R y (path 0) -> Acc R y
H2:= forall n: nat, R (path (S n)) (path n)
R ?y (path 0) eapply H2.
  -X: Type
R: X -> X -> Prop
path: nat -> X
ih:= forall y : X, R y (path 0) -> ~ (exists path : nat -> X, path 0 = y /\ (forall n: nat, R (path (S n)) (path n)))
H:= forall y: X, R y (path 0) -> Acc R y
H2:= forall n: nat, R (path (S n)) (path n)
exists path0 : nat -> X, path0 0 = path 1 /\ (forall n : nat, R (path0 (S n)) (path0 n)) exists (fun n => path (S n)).X: Type
R: X -> X -> Prop
path: nat -> X
ih:= forall y : X, R y (path 0) -> ~ (exists path : nat -> X, path 0 = y /\ (forall n: nat, R (path (S n)) (path n)))
H:= forall y: X, R y (path 0) -> Acc R y
H2:= forall n: nat, R (path (S n)) (path n)
path 1 = path 1 /\ (forall n : nat, R (path (S (S n))) (path (S n)))
    firstorder.
Qed.exercise_chain is defined

To conclude this lecture, we give a proof that one can use recursion on proofs to write a function that extracts the witness from a proof of exists n, f n = true.

This proof can be given using different ways. We show the easiest approach here, and leave a variant using Acc as exercise.

From Stdlib Require Import Lia.

We start by giving a predicate least P n k that says that k is the least natural (above n) that verifies predicate P.

Definition least P n k :=
  n <= k /\
  P k /\
  forall i, n <= i -> P i -> k <= i.least is defined

Section WO.

  Context (f : nat -> bool).f is declared

The key is in the definition of a guardedness predicate which is in Prop` (so we can eliminate exist into it) and which verifies the subsingleton criterion (so we can eliminate it into Type).

  Inductive G (n : nat) : Prop :=
  | GI : (f n = false -> G (S n)) -> G n.G is defined
G_rect is defined
G_ind is defined
G_rec is defined
G_sind is defined

  Lemma G_sig n :
    G n ->
    { k | least (fun k => f k = true) n k }.f: nat -> bool
n: nat
G n -> {k : nat | least (fun k0 : nat => f k0 = true) n k}
  Proof.f: nat -> bool
n: nat
G n -> {k : nat | least (fun k0 : nat => f k0 = true) n k}
    induction 1 as [n _ ih].f: nat -> bool
n: nat
ih:= f n = false -> {k : nat | least (fun k0: nat => f k0 = true) (S n) k}
{k : nat | least (fun k0 : nat => f k0 = true) n k}
    destruct (f n) eqn:e.f: nat -> bool
n: nat
e: f n = true
ih:= true = false -> {k : nat | least (fun k0: nat => f k0 = true) (S n) k}
{k : nat | least (fun k0 : nat => f k0 = true) n k}
f: nat -> bool
n: nat
e: f n = false
ih:= false = false -> {k : nat | least (fun k0: nat => f k0 = true) (S n) k}
{k : nat | least (fun k0 : nat => f k0 = true) n k}
    -f: nat -> bool
n: nat
e: f n = true
ih:= true = false -> {k : nat | least (fun k0: nat => f k0 = true) (S n) k}
{k : nat | least (fun k0 : nat => f k0 = true) n k} exists n.f: nat -> bool
n: nat
e: f n = true
ih:= true = false -> {k : nat | least (fun k0: nat => f k0 = true) (S n) k}
least (fun k : nat => f k = true) n n unfold least.f: nat -> bool
n: nat
e: f n = true
ih:= true = false -> {k : nat | least (fun k0: nat => f k0 = true) (S n) k}
n <= n /\ f n = true /\ (forall i : nat, n <= i -> f i = true -> n <= i) eauto.
    -f: nat -> bool
n: nat
e: f n = false
ih:= false = false -> {k : nat | least (fun k0: nat => f k0 = true) (S n) k}
{k : nat | least (fun k0 : nat => f k0 = true) n k} destruct (ih eq_refl) as (k & hle & hk & hleast).f: nat -> bool
n: nat
e: f n = false
ih:= false = false -> {k : nat | least (fun k0: nat => f k0 = true) (S n) k}
k: nat
hle: S n <= k
hk: f k = true
hleast:= forall i: nat, S n <= i -> f i = true -> k <= i
{k0 : nat | least (fun k1 : nat => f k1 = true) n k0}
      exists k.f: nat -> bool
n: nat
e: f n = false
ih:= false = false -> {k : nat | least (fun k0: nat => f k0 = true) (S n) k}
k: nat
hle: S n <= k
hk: f k = true
hleast:= forall i: nat, S n <= i -> f i = true -> k <= i
least (fun k0 : nat => f k0 = true) n k split.f: nat -> bool
n: nat
e: f n = false
ih:= false = false -> {k : nat | least (fun k0: nat => f k0 = true) (S n) k}
k: nat
hle: S n <= k
hk: f k = true
hleast:= forall i: nat, S n <= i -> f i = true -> k <= i
n <= k
f: nat -> bool
n: nat
e: f n = false
ih:= false = false -> {k : nat | least (fun k0: nat => f k0 = true) (S n) k}
k: nat
hle: S n <= k
hk: f k = true
hleast:= forall i: nat, S n <= i -> f i = true -> k <= i
f k = true /\ (forall i : nat, n <= i -> f i = true -> k <= i) 2: split.f: nat -> bool
n: nat
e: f n = false
ih:= false = false -> {k : nat | least (fun k0: nat => f k0 = true) (S n) k}
k: nat
hle: S n <= k
hk: f k = true
hleast:= forall i: nat, S n <= i -> f i = true -> k <= i
n <= k
f: nat -> bool
n: nat
e: f n = false
ih:= false = false -> {k : nat | least (fun k0: nat => f k0 = true) (S n) k}
k: nat
hle: S n <= k
hk: f k = true
hleast:= forall i: nat, S n <= i -> f i = true -> k <= i
f k = true
f: nat -> bool
n: nat
e: f n = false
ih:= false = false -> {k : nat | least (fun k0: nat => f k0 = true) (S n) k}
k: nat
hle: S n <= k
hk: f k = true
hleast:= forall i: nat, S n <= i -> f i = true -> k <= i
forall i : nat, n <= i -> f i = true -> k <= i
      +f: nat -> bool
n: nat
e: f n = false
ih:= false = false -> {k : nat | least (fun k0: nat => f k0 = true) (S n) k}
k: nat
hle: S n <= k
hk: f k = true
hleast:= forall i: nat, S n <= i -> f i = true -> k <= i
n <= k lia.
      +f: nat -> bool
n: nat
e: f n = false
ih:= false = false -> {k : nat | least (fun k0: nat => f k0 = true) (S n) k}
k: nat
hle: S n <= k
hk: f k = true
hleast:= forall i: nat, S n <= i -> f i = true -> k <= i
f k = true assumption.
      +f: nat -> bool
n: nat
e: f n = false
ih:= false = false -> {k : nat | least (fun k0: nat => f k0 = true) (S n) k}
k: nat
hle: S n <= k
hk: f k = true
hleast:= forall i: nat, S n <= i -> f i = true -> k <= i
forall i : nat, n <= i -> f i = true -> k <= i intros i hi.f: nat -> bool
n: nat
e: f n = false
ih:= false = false -> {k : nat | least (fun k0: nat => f k0 = true) (S n) k}
k: nat
hle: S n <= k
hk: f k = true
hleast:= forall i: nat, S n <= i -> f i = true -> k <= i
i: nat
hi: n <= i
f i = true -> k <= i inversion hi.f: nat -> bool
n: nat
e: f n = false
ih:= false = false -> {k : nat | least (fun k0: nat => f k0 = true) (S n) k}
k: nat
hle: S n <= k
hk: f k = true
hleast:= forall i: nat, S n <= i -> f i = true -> k <= i
i: nat
hi: n <= i
H: n = i
f i = true -> k <= i
f: nat -> bool
n: nat
e: f n = false
ih:= false = false -> {k : nat | least (fun k0: nat => f k0 = true) (S n) k}
k: nat
hle: S n <= k
hk: f k = true
hleast:= forall i: nat, S n <= i -> f i = true -> k <= i
i: nat
hi: n <= i
m: nat
H: n <= m
H0: S m = i
f (S m) = true -> k <= S m
        *f: nat -> bool
n: nat
e: f n = false
ih:= false = false -> {k : nat | least (fun k0: nat => f k0 = true) (S n) k}
k: nat
hle: S n <= k
hk: f k = true
hleast:= forall i: nat, S n <= i -> f i = true -> k <= i
i: nat
hi: n <= i
H: n = i
f i = true -> k <= i congruence.
        *f: nat -> bool
n: nat
e: f n = false
ih:= false = false -> {k : nat | least (fun k0: nat => f k0 = true) (S n) k}
k: nat
hle: S n <= k
hk: f k = true
hleast:= forall i: nat, S n <= i -> f i = true -> k <= i
i: nat
hi: n <= i
m: nat
H: n <= m
H0: S m = i
f (S m) = true -> k <= S m eapply hleast.f: nat -> bool
n: nat
e: f n = false
ih:= false = false -> {k : nat | least (fun k0: nat => f k0 = true) (S n) k}
k: nat
hle: S n <= k
hk: f k = true
hleast:= forall i: nat, S n <= i -> f i = true -> k <= i
i: nat
hi: n <= i
m: nat
H: n <= m
H0: S m = i
S n <= S m lia.
  Defined.G_sig is defined

  Lemma G_zero n :
    G n -> G 0.f: nat -> bool
n: nat
G n -> G 0
  Proof.f: nat -> bool
n: nat
G n -> G 0
    induction n as [|n ih].f: nat -> bool
G 0 -> G 0
f: nat -> bool
n: nat
ih: G n -> G 0
G (S n) -> G 0
    -f: nat -> bool
G 0 -> G 0 auto.
    -f: nat -> bool
n: nat
ih: G n -> G 0
G (S n) -> G 0 intros h.f: nat -> bool
n: nat
ih: G n -> G 0
h: G (S n)
G 0 apply ih.f: nat -> bool
n: nat
ih: G n -> G 0
h: G (S n)
G n
      constructor.f: nat -> bool
n: nat
ih: G n -> G 0
h: G (S n)
f n = false -> G (S n) auto.
  Defined.G_zero is defined

  Theorem linear_search :
    (exists n, f n = true) ->
    { n | least (fun n => f n = true) 0 n }.f: nat -> bool
(exists n : nat, f n = true) -> {n : nat | least (fun n0 : nat => f n0 = true) 0 n}
  Proof.f: nat -> bool
(exists n : nat, f n = true) -> {n : nat | least (fun n0 : nat => f n0 = true) 0 n}
    intros h.f: nat -> bool
h:= exists n: nat, f n = true
{n : nat | least (fun n0 : nat => f n0 = true) 0 n}
    apply (G_sig 0).f: nat -> bool
h:= exists n: nat, f n = true
G 0
    destruct h as [n h].f: nat -> bool
n: nat
h: f n = true
G 0
    apply (G_zero n).f: nat -> bool
n: nat
h: f n = true
G n
    constructor.f: nat -> bool
n: nat
h: f n = true
f n = false -> G (S n) rewrite h.f: nat -> bool
n: nat
h: f n = true
true = false -> G (S n) discriminate.
  Defined.linear_search is defined

End WO.

About linear_search.linear_search : forall f : nat -> bool, (exists n : nat, f n = true) -> {n : nat | least (fun n0 : nat => f n0 = true) 0 n}linear_search is not universe polymorphicArguments linear_search f%function_scope _linear_search is transparentExpands to: Constant lesson5.linear_searchDeclared in toplevel input, characters 7730-7743

Gallery of inductive types and corresponding inductive principles

We do not believe giving you the recipe in general is going to be useful, instead we think showing you representative examples together is going to be more helpful. So here we go.

Lists

Lists are an inductive type (Type) have one uniform parameter A : Type, and two constructors nil and cons.

Inductive list (A : Type) : Type :=
| nil
| cons (a : A) (l : list A).list is defined
list_rect is defined
list_ind is defined
list_rec is defined
list_sind is defined

As it's a type, it can be eliminated to produce both Type and Prop, hence we have the two following induction principles.

The motive is thus of the form P : list A -> Type or P : list A -> Prop. Note that A is a uniform parameter so it is quantified before the motive, which is why it can mention it. The conclusion will then be forall (l : list A), P l.

The induction principles has two branches, one for nil and one for cons. Because nil : list A the corresponding branch is P nil. Because cons : A -> list A -> list A the corresponding branch is forall (a : A) (l : list A), P l -> P (cons a l). To get it, you start from the type of the constructor, and for each recursive invocation of list A you additionally get some induction hypothesis P l. The return type list A is then replaced by P (cons a l), i.e. the motive applied to the constructor itself.

Check list_ind.list_ind
     : forall (A : Type) (P : list A -> Prop), P (nil A) -> (forall (a : A) (l : list A), P l -> P (cons A a l)) -> forall l : list A, P l
Check list_rect.list_rect
     : forall (A : Type) (P : list A -> Type), P (nil A) -> (forall (a : A) (l : list A), P l -> P (cons A a l)) -> forall l : list A, P l

Evenness

We have also seen the even predicate which is a proposition (Prop). It takes no parameter, has one index n : nat and two constructors.

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

Since it has two constructors, it doesn't satisfy the subsingleton criterion and thus it produces only even_ind but no even_rect.

Since the sort is Prop, the motive will not depend on the proof of even n, only on n, so it will be P : nat -> Prop.

Otherwise the recipe is the same, you just don't need to apply P to the constructor, only to the value of the index, so in one branch P 0 and in the other P (S (S n)). The conclusion will be forall n, even n -> P n. Even if P doesn't talk about the proof of even n, it is still required.

Check even_ind.even_ind
     : forall P : nat -> Prop, P 0 -> (forall n : nat, even n -> P n -> P (S (S n))) -> forall n : nat, even n -> P n

Accessibility

Acc has three parameters: two uniform parameters A and R and one non-uniform parameter x (it stays x in the conclusion, but in the argument to Acc_intro it is instiated by y). It has no index.

Because it has one constructor with only one non-parameter argument which happens to be a proof (forall y, R y x -> Acc A R y has type Prop), it satisfies the subsingleton criterion.

Inductive Acc' A (R : A -> A -> Prop) (x : A) :=
| Acc_intro' : (forall y, R y x -> Acc' A R y) -> Acc' A R x.Acc' is defined
Acc'_rect is defined
Acc'_ind is defined
Acc'_rec is defined
Acc'_sind is defined

Check Acc'_ind.Acc'_ind
     : forall (A : Type) (R : A -> A -> Prop) (P : forall x : A, Acc' A R x -> Prop), (forall (x : A) (a : forall y : A, R y x -> Acc' A R y), (forall (y : A) (r : R y x), P y (a y r)) -> P x (Acc_intro' A R x a)) -> forall (x : A) (a : Acc' A R x), P x a
Check Acc'_rect.Acc'_rect
     : forall (A : Type) (R : A -> A -> Prop) (P : forall x : A, Acc' A R x -> Type), (forall (x : A) (a : forall y : A, R y x -> Acc' A R y), (forall (y : A) (r : R y x), P y (a y r)) -> P x (Acc_intro' A R x a)) -> forall (x : A) (a : Acc' A R x), P x a