Pourquoi est-il impossible d'effectuer une induction sur un terme utilisé en conclusion?

Question

Supposons le scénario particulier suivant.

Nous avons une définition de l'égalité:

Inductive eqwal {A : Type} (x : A) : A -> Prop := 
    eqw_refl : eqwal x x. 

Et nats Peano:

Inductive nawt : Prop := 
    | zewro : nawt 
    | sawc : nawt -> nawt. 

Nous définissons plus sur nats:

Fixpoint plaws (m n : nawt) : nawt := 
    match m with 
     | zewro => n 
     | sawc m' => sawc (plaws m' n) 
    end. 

Et maintenant, nous voulons prouver que zéro est neutre par rapport à sommateur:

Theorem neutral_r : forall n : nawt, eqwal (plaws n zewro) n. 

Malheureusement, la dernière ligne des proofscripts suivants dit "Erreur: n est utilisé en guise de conclusion.".

Proof. 
intros. 
induction n. - this is the culprit 

Il n'y a pas beaucoup d'erreur dans la documentation officielle et je suis un peu confus - pourquoi cette erreur se produit-elle?

Utilisation de la bibliothèque standard, je peux prouver le théorème facilement:

Theorem neutral_r : forall n : nat, 
    n + 0 = n. 
Proof. 
    induction n; try reflexivity. 
    cbn; rewrite IHn; reflexivity. 
Qed. 

Answer 1

Le problème est que vous avez défini nawt avec tri Prop au lieu de Type ou Set. Par défaut, les principes d'induction générés pour les propositions ne permettent pas de prouver quoi que ce soit à propos des preuves de ces propositions. Considérons le principe d'induction par défaut généré pour nawt:

Check nawt_ind. 
> nawt_ind : forall P : Prop, P -> (nawt -> P -> P) -> nawt -> P 

Parce que nawt_ind quantifie sur Prop, et non plus nat -> Prop, nous ne pouvons pas l'utiliser pour prouver votre objectif.

La solution consiste à définir quelques options qui modifient le comportement par défaut de Coq, comme dans le script suivant.

Inductive eqwal {A : Type} (x : A) : A -> Prop := 
    eqw_refl : eqwal x x. 

Unset Elimination Schemes. 

Inductive nawt : Prop := 
    | zewro : nawt 
    | sawc : nawt -> nawt. 

Scheme nawt_ind := Induction for nawt Sort Prop. 

Set Elimination Schemes. 

Fixpoint plaws (m n : nawt) : nawt := 
    match m with 
     | zewro => n 
     | sawc m' => sawc (plaws m' n) 
    end. 

Theorem eqwal_sym {A : Type} (x y : A) : eqwal x y -> eqwal y x. 
Proof. intros H. destruct H. constructor. Qed. 

Theorem neutral_r : forall n : nawt, eqwal (plaws n zewro) n. 
Proof. 
intros. induction n as [|n IH]; simpl. 
- constructor. 
- apply eqwal_sym in IH. destruct IH. constructor. 
Qed. 

L'option Elimination Schemes cause Coq pour générer automatiquement des principes d'induction pour les types et les propositions données. Dans ce script, je l'ai simplement désactivé et j'ai utilisé la commande Scheme pour générer le principe d'induction correct pour nawt. Pour que la tactique induction fonctionne, il est important de donner à ce principe le nom nawt_ind: c'est le nom par défaut qui est généré par Coq, et c'est celui que induction recherche lorsqu'il est appelé.

Cela dit, je déconseillerais généralement la définition d'un type de nombres naturels dans Prop au lieu de Type, car Coq impose des restrictions sur la façon dont vous pouvez utiliser des choses qui vivent dans Prop. Par exemple, il est impossible de montrer que zewro est différent de sawc zewro.