How to use Coq's own induction principle?

Question

I read that the induction principle for a type is simply a proposition theorem for P Therefore, I built the 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 principle of induction itself:

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

But now I am having problems using the theorem. I cannot use it the same way as induction tactics.

For example, I tried:

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

But in the last line, I got:

 Error: Cannot recognize an induction scheme. 

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

thanks

Answer 1

What you did was basically right. The problem is that Coq has some problems recognizing that what you write is an induction principle due to intermediate definitions. This, for example, works great:

 Theorem list_ind_rcons: forall {X:Type} (P:list X -> Prop), P nil -> (forall xl, P l -> P (rcons lx)) -> forall l, P l. Proof. Admitted. Theorem rev_app_dist: forall {X} (l1 l2:list X), rev (l1 ++ l2) = rev l2 ++ rev l1. Proof. intros X l1 l2. induction l2 using @list_ind_rcons. 

I don’t know whether Coq should be considered impossible to automatically deploy intermediate definitions as an error or not, but at least there is a workaround.

Answer 2

If you want to keep intermediate definitions, then you can use the Section mechanism, for example:

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

Coq replaces the definitions and list_ind_rcons has the required type and induction ... using ... works:

 Theorem rev_app_dist: forall {X} (l1 l2:list X), rev (l1 ++ l2) = rev l2 ++ rev l1. Proof. intros X l1 l2. induction l2 using list_ind_rcons. Abort. 

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

 Coq < 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