pliant retour après déploiement

Question

je fold_length défini comme ceci:

Inductive list (X: Type) : Type := 
    | nil : list X 
    | cons : X -> list X -> list X. 

Arguments nil {X}. 
Arguments cons {X} _ _. 

Notation "x :: y" := (cons x y) 
        (at level 60, right associativity). 
Notation "[ ]" := nil. 

Fixpoint fold {X Y:Type} (f: X -> Y -> Y) (l:list X) (b:Y) : Y := 
    match l with 
    | nil => b 
    | h :: t => f h (fold f t b) 
    end. 

Definition fold_length {X : Type} (l : list X) : nat := 
    fold (fun _ n => S n) l 0. 

Je dois prouver un théorème et c'est mon code à ce jour:

Theorem fold_length_correct : forall X (l : list X), 
    fold_length l = length l. 
Proof. 
    intros X l. 
    induction l as [| n l' IHl']. 
    - simpl. 
    unfold fold_length. 
    simpl. 
    reflexivity. 
    - simpl. 
    unfold fold_length. 
    simpl. 

En ce moment, mon but ressemble à ceci :

X : Type 
    n : X 
    l' : list X 
    IHl' : fold_length l' = length l' 
    ============================ 
    S (fold (fun (_ : X) (n0 : nat) => S n0) l' 0) = S (length l') 

maintenant, je veux convertir l'expression (fold (fun (_ : X) (n0 : nat) => S n0) l' 0) à fold_length l' en utilisant la définition de fold_length. Existe-t-il un moyen de faire cela dans Coq (Il semble y avoir quelque chose de tactique nommé fold dans Coq. Est-ce que cela peut arriver?)?

Aussi, est-il un moyen de prouver le théorème ci-dessus sans l'utilisation de unfold et fold tactique?

Answer 1

Pour répondre à votre première question, oui, la tactique fold peut être utilisée ici pour remplacer le côté gauche de l'égalité par S (fold_length l'). Habituellement, pour une fonction f, fold f n'est pas assez puissant pour détecter ce qu'il peut plier. Mais si vous spécifiez le terme entier, comme ici fold (fold_length l'), cela fonctionne. En ce qui concerne votre deuxième question, notez que des tactiques comme reflexivity ou assumption peuvent conclure si les termes impliqués sont égaux jusqu'à certaines simplifications. Ici, le cas de base de l'induction peut être juste reflexivity. Dans le second cas, en supposant que fold est List.fold_right, simpl peut étonnamment simplifier sans se déplier et vous ne devriez pas avoir besoin de unfold ou fold ici non plus.