Récursion structurelle sur un paramètre dépendant

Question

J'essaie d'écrire le tamis de Eratosthènes dans Coq. J'ai une fonction crossout : forall {n:nat}, vector bool n -> nat -> vector bool n. Lorsque le tamis trouve un nombre premier, il utilise crossout pour marquer tous les nombres qui ne sont pas premiers, puis récursifs sur le vecteur résultant. Le tamis ne peut évidemment pas être structurellement récursif sur le vecteur lui-même, mais il est structurellement récursif sur la longueur du vecteur. Ce que je veux faire quelque chose comme ceci:

Fixpoint sieve {n:nat} (v:vector bool n) (acc:nat) {struct n} : list nat := 
    match v with 
    | [] => Datatypes.nil 
    | false :: v' => sieve v' (S acc) 
    | true :: v' => Datatypes.cons acc (sieve (crossout v' acc) (S acc)) 
    end. 

Mais si je l'écris comme ça, Coq se plaint que la longueur de v' n'est pas un sous-terme de n. Je sais que c'est le cas, mais peu importe comment je structure la fonction, je n'arrive pas à convaincre Coq que c'est le cas. Est-ce que quelqu'un sait comment je peux?

Answer 1

Ceci est l'un des pièges les plus courants avec les types dépendants dans Coq. Ce qui se passe intuitivement, c'est que dès que le motif correspond à v, Coq "oublie" que la longueur de ce vecteur est réellement n, et perd la connexion entre la longueur de v' et le prédécesseur de n. La solution ici consiste à appliquer ce que Adam Chlipala appelle le modèle de convoi , et faire correspondre le motif renvoyer une fonction. Bien qu'il soit possible de le faire par le modèle correspondant à v, je pense qu'il est plus facile de le faire par le modèle correspondant à n:

Require Import Vector. 

Axiom crossout : forall {n}, t bool n -> nat -> t bool n. 

Fixpoint sieve {n:nat} : t bool n -> nat -> list nat := 
    match n with 
    | 0 => fun _ _ => Datatypes.nil 
    | S n' => fun v acc => 
       if hd v then 
        Datatypes.cons acc (sieve (crossout (tl v) acc) (S acc)) 
       else 
        sieve (tl v) (S acc) 
    end. 

Remarquez comment l'en-tête de sieve a changé un peu: maintenant le type de retour est en fait une fonction pour aider l'inférence de type de Coq.

Pour plus d'informations, consultez le livre d'Adam: http://adam.chlipala.net/cpdt/html/MoreDep.html.