Come utilizzare un principio di induzione personalizzato in Coq?

Question

Ho letto che il principio di induzione per un tipo è solo un teorema su una proposizione P. Quindi ho costruito un principio di induzione per List basato sul costruttore di elenchi destro (o inverso).

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

Il principio di induzione è di per sé:

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. 

Ma ora, sto avendo problemi con il teorema. Non so come invocarlo per ottenere lo stesso risultato della tattica induction.

Per esempio, ho provato:

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. 

Ma nell'ultima riga, ho ottenuto:

Error: Cannot recognize an induction scheme. 

Quali sono i passi corretti per definire e applicare un principio di induzione personalizzato come list_ind_rcons?

Grazie

Answer 1

Quello che hai fatto era per lo più corretto. Il problema è che Coq ha qualche problema nel riconoscere che quello che hai scritto è un principio di induzione, a causa delle definizioni intermedie. Questo, per esempio, funziona bene:

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

Non so se Coq non essere in grado di dispiegare automaticamente le definizioni intermedie devono essere considerati un bug o no, ma almeno c'è una soluzione.

Answer 2

Se si vorrebbe preservare le definizioni intermedi, allora si potrebbe utilizzare il meccanismo Section, così:

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 sostituisce le definizioni list_ind_rcons ha il tipo necessario e induction ... using ... lavori:

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. 

A proposito, questo principio di induzione è presente nella libreria standard (modulo List):

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