How to use a custom induction principle in Coq?

Question

I read that the induction principle for a type is just a theorem about a proposition P. So I constructed an induction principle for List based on the right (or reverse) list constructor.

Definition rcons {X : Type} (l : list X) (x : X) : list X :=
  l ++ x :: nil.

The induction principle itself is:

Definition true_for_nil {X : Type} (P : list X -> Prop) : Prop :=
  P nil.

Definition true_for_list {X : Type} (P : list X -> Prop) : Prop :=
  forall xs, P xs.

Definition preserved_by_rcons {X : Type} (P : list X -> Prop) : Prop :=
  forall xs' x, P xs' -> P (rcons xs' x).

Theorem list_ind_rcons :
  forall {X : Type} (P : list X -> Prop),
    true_for_nil P ->
    preserved_by_rcons P ->
    true_for_list P.
forall (X : Type) (P : list X -> Prop),
true_for_nil P ->
preserved_by_rcons P -> true_for_list P
Proof.
forall (X : Type) (P : list X -> Prop),
true_for_nil P ->
preserved_by_rcons P -> true_for_list P Admitted.

But now, I am having trouble using the theorem. I don't how to invoke it to achieve the same as the induction tactic.

For example, I tried:

Theorem rev_app_dist : forall {X} (l1 l2 : list X),
    rev (l1 ++ l2) = rev l2 ++ rev l1.
forall (X : Type) (l1 l2 : list X),
rev (l1 ++ l2) = rev l2 ++ rev l1
Proof.
forall (X : Type) (l1 l2 : list X),
rev (l1 ++ l2) = rev l2 ++ rev l1
  intros X l1 l2.
X: Type
l1, l2: list X
rev (l1 ++ l2) = rev l2 ++ rev l1
  induction l2 using list_ind_rcons.
Cannot recognize an induction scheme.
X: Type
l1, l2: list X
rev (l1 ++ l2) = rev l2 ++ rev l1

But in the last line, I got:

The command has indeed failed with message:
Cannot recognize an induction scheme.

What are the correct steps to define and apply a custom induction principle like list_ind_rcons?

Answer (Anton Trunov)

If one would like to preserve the intermediate definitions, then one could use the Section mechanism, like so:

Require Import Coq.Lists.List. Import ListNotations.

Definition rcons {X : Type} (l : list X) (x : X) : list X :=
  l ++ [x].

Section custom_induction_principle.
  Variable X : Type.
  Variable P : list X -> Prop.

  Hypothesis true_for_nil : P nil.
  Hypothesis true_for_list : forall xs, P xs.
  Hypothesis preserved_by_rcons : forall xs' x, P xs' -> P (rcons xs' x).

  Fixpoint list_ind_rcons (xs : list X) : P xs.
X: Type
P: list X -> Prop
true_for_nil: P []
true_for_list: forall xs : list X, P xs
preserved_by_rcons: forall (xs' : list X) (x : X),
P xs' -> P (rcons xs' x)
list_ind_rcons: forall xs : list X, P xs
xs: list X
P xs Admitted.
End custom_induction_principle.

Coq substitutes the definitions and list_ind_rcons has the needed type and induction ... using ... works:

Theorem rev_app_dist : forall {X} (l1 l2 : list X),
    rev (l1 ++ l2) = rev l2 ++ rev l1.
forall (X : Type) (l1 l2 : list X),
rev (l1 ++ l2) = rev l2 ++ rev l1
Proof.
forall (X : Type) (l1 l2 : list X),
rev (l1 ++ l2) = rev l2 ++ rev l1
  intros X l1 l2.
X: Type
l1, l2: list X
rev (l1 ++ l2) = rev l2 ++ rev l1
  induction l2 using list_ind_rcons.
X: Type
l1: list X
rev (l1 ++ []) = rev [] ++ rev l1
X: Type
l1, l2: list X
rev (l1 ++ l2) = rev l2 ++ rev l1
X: Type
l1, l2: list X
x: X
IHl2: rev (l1 ++ l2) = rev l2 ++ rev l1
rev (l1 ++ rcons l2 x) = rev (rcons l2 x) ++ rev l1
Abort.

By the way, this induction principle is present in the standard library (List module):

Check rev_ind.
rev_ind
     : forall (A : Type) (P : list A -> Prop),
       P [] ->
       (forall (x : A) (l : list A),
        P l -> P (l ++ [x])) -> forall l : list A, P l

Answer (Arthur Azevedo De Amorim)

What you did was mostly correct. The problem is that Coq has some trouble recognizing that what you wrote is an induction principle, because of the intermediate definitions. This, for instance, works just fine:

Theorem list_ind_rcons :
  forall {X : Type} (P : list X -> Prop),
    P nil ->
    (forall x l, P l -> P (rcons l x)) ->
    forall l, P l.
forall (X : Type) (P : list X -> Prop),
P nil ->
(forall (x : X) (l : list X), P l -> P (rcons l x)) ->
forall l : list X, P l
Proof.
forall (X : Type) (P : list X -> Prop),
P nil ->
(forall (x : X) (l : list X), P l -> P (rcons l x)) ->
forall l : list X, P l Admitted.

Theorem rev_app_dist : forall {X} (l1 l2 : list X),
    rev (l1 ++ l2) = rev l2 ++ rev l1.
forall (X : Type) (l1 l2 : list X),
rev (l1 ++ l2) = rev l2 ++ rev l1
Proof.
forall (X : Type) (l1 l2 : list X),
rev (l1 ++ l2) = rev l2 ++ rev l1
  intros X l1 l2.
X: Type
l1, l2: list X
rev (l1 ++ l2) = rev l2 ++ rev l1
  induction l2 using @list_ind_rcons.
X: Type
l1: list X
rev (l1 ++ nil) = rev nil ++ rev l1
X: Type
l1: list X
x: X
l2: list X
IHl2: rev (l1 ++ l2) = rev l2 ++ rev l1
rev (l1 ++ rcons l2 x) = rev (rcons l2 x) ++ rev l1

I don't know if Coq not being able to automatically unfold the intermediate definitions should be considered a bug or not, but at least there is a workaround.

A: In Coq, there is long standing disrespect for definitional equality in the implementation of tactics. Whilst this is questionable, ideologically, it is far too late to do anything about it in practice.