Comment définir une fonction par induction sur deux arguments en Coq?

14

Comment puis-je convaincre Coq que la fonction récursive donnée ci-dessous se termine? La fonction prend deux arguments inductifs. Intuitivement, la récursivité se termine car l'un ou l'autre argument est décomposé.

Plus précisément, la fonction prend deux arbres en entrée.

Inductive Tree :=
| Tip: Tree
| Bin: Tree -> Tree -> Tree.

Sur Trees, j'aime faire le style d'induction suivant.

Inductive TreePair :=
| TipTip : TreePair
| TipBin : Tree -> Tree -> TreePair
| BinTip : Tree -> Tree -> TreePair
| BinBin : TreePair -> TreePair -> TreePair.

Fixpoint pair (l r: Tree): TreePair :=
  match l with
    | Tip =>
      match r with
        | Tip => TipTip
        | Bin rl rr => TipBin rl rr
      end
    | Bin ll lr =>
      match r with
        | Tip => BinTip ll lr
        | Bin rl rr => BinBin (pair l rl) (pair lr r)
      end
  end.

La définition de TreePair est acceptée, mais la définition de la paire de fonctions génère le message d'erreur:

Error: Cannot guess decreasing argument of fix.

Je suis donc intéressé à savoir comment convaincre Coq de la résiliation.

yhirai
la source
1
Avez-vous essayé de passer l et r ensemble comme produit plutôt que d'utiliser le curry? Cela devrait l'aider.
Per Vognsen
1
Certaines personnes pensent que cette question concerne la programmation et est hors de portée de ce site Web. Bien que je ne sois pas sûr si je suis d'accord, vous voudrez peut-être connaître le problème potentiel. Si quelqu'un a quelque chose à dire sur la pertinence, veuillez écrire sur la méta-discussion à laquelle j'ai lié.
Tsuyoshi Ito
3
Cette question concerne vraiment la spécification de limites décroissantes monotones sur les structures de données afin de s'assurer que l'opération pairest bien définie. Coq n'est que le véhicule.
Dave Clarke

Réponses:

12

Les définitions de points fixes de Coq nécessitent que les appels inductifs reçoivent un argument structurellement plus petit. Au fond, une construction fixpoint prend un seul argument: il n'y a pas de concept intégré d'une définition récursive sur deux arguments. Heureusement, la définition de Coq de structurellement plus petit inclut des types d'ordre supérieur, ce qui est extrêmement puissant.

Votre définition de point fixe à deux arguments suit un modèle simple: soit le premier argument devient plus petit, soit le premier argument reste identique et le deuxième argument devient plus petit. Ce modèle assez courant peut être géré par un simple correctif.

Fixpoint pair l := fix pair1 (r : Tree) :=
  match l with
    | Tip => match r with
              | Tip => TipTip
              | Bin rl rr => TipBin rl rr
            end
    | Bin ll lr => match r with
                    | Tip => BinTip ll lr
                    | Bin rl rr => BinBin (pair1 rl) (pair lr r)
                   end
  end.

Pour les cas plus complexes, ou si vos goûts fonctionnent de cette façon, vous pouvez utiliser la récursivité plus proche de la façon dont elle est enseignée dans les cours de mathématiques, en construisant le point de repère à partir d'un calcul d'étape et d'un argument de bien-fondé distinct , en utilisant souvent une mesure entière . Vous pouvez également faire ressembler votre définition à un programme classique dans une langue non totale avec une terminaison distincte en utilisant le Programvernaculaire .

Gilles 'SO- arrête d'être méchant'
la source
Maintenant je sais que c'est ce que j'ai demandé!
yhirai
cela fera-t-il une différence si je pousse fix pair1 rdans la deuxième branche du niveau supérieur match(et bien sûr, adapte la première branche pour renvoyer un type de fonction en conséquence)?
jour
@plmday: travail bidirectionnel. Ils sont équivalents sur le plan de l'extension pour une définition raisonnable de l'extensionnalité, et plus important encore, ils sont tous deux bien typés (la réécriture extensionnelle ne modifie aucune des propriétés de covariance (positivité) pertinentes).
Gilles 'SO- arrête d'être méchant'