Obtenir un fort principe d'induction en Coq

Question

On suppose les éléments suivants:

Inductive bin : Set := Z | O. 

Fixpoint fib (n : nat) : list bin := 
    match n with 
    | 0 => [Z] 
    | S k => match k with 
       | 0 => [O] 
       | S k' => fib k' ++ fib k 
      end 
    end. 

Je voudrais montrer:

Theorem fib_first : forall n, 
    Nat.Even n -> n > 3 -> exists w, fib n = Z :: w. 

Cependant, en effectuant induction sur n, je reçois un inductive vraiment inutile hypothèse fixant n, indiquant que IH : Nat.Even n -> n > 3 -> exists w : list bin, fib n = Z :: w. Ce que j'aurais idéalement est ce qui suit: IH : forall n : nat, Nat.Even n -> n > 3 -> exists w : list bin, fib n = Z :: w Naturellement, je ne peux pas assumer la proposition originale, mais il me semble que j'ai besoin de prouver quelque chose de plus fort peut-être?

Mon idée du raisonnement inductif serait rendu possible par l'expansion F n = F n-2 . F n-1, nous savons F n-2 est encore ssi F n est même, et puisque aucun des F n-2 ou F n-1 est vide, on peut montrer la sous-chaîne est plus courte, donc suffisante pour la Hypothèse inductive - comment l'exprimer en Coq?

Answer 1

L'astuce consiste à se dérouler la définition de Nat.Even et faire induction sur n/2 au lieu de n:

Theorem fib_first : forall n, 
    Nat.Even n -> exists w, fib n = Z :: w. 
Proof. 
intros n [m ->]. 
induction m as [|m IH]. 
- now exists nil. 
- rewrite <- mult_n_Sm, plus_comm. 
    generalize (2 * m) IH. clear m IH. simpl. 
    intros n [w ->]. 
    simpl. eauto. 
Qed. 

Notez que votre n > 3 hypothèse n'est pas réellement nécessaire.