Écrire des programmes bien établis en Coq en utilisant Fix ou Program Fixpoint

Question

En suivant l'exemple donné dans le chapitre GeneralRec du livre Chlipala, j'essaye d'écrire l'algorithme de fusion.

Voici mon code

Require Import Nat. 

Fixpoint insert (x:nat) (l: list nat) : list nat := 
    match l with 
    | nil => x::nil 
    | y::l' => if leb x y then 
       x::l 
      else 
       y::(insert x l') 
    end. 

Fixpoint merge (l1 l2 : list nat) : list nat := 
    match l1 with 
    | nil => l2 
    | x::l1' => insert x (merge l1' l2) 
    end. 

Fixpoint split (l : list nat) : list nat * list nat := 
    match l with 
    | nil => (nil,nil) 
    | x::nil => (x::nil,nil) 
    | x::y::l' => 
    let (ll,lr) := split l' in 
    (x::ll,y::lr) 
    end. 

Definition lengthOrder (l1 l2 : list nat) := 
    length l1 < length l2. 

Theorem lengthOrder_wf : well_founded lengthOrder. 
Admitted. 

Le problème est qu'il est impossible d'écrire la fonction mergesort avec la commande Fixpoint puisque la fonction ne diminue pas structurellement:

Fixpoint mergeSort (l: list nat) : list nat := 
    if leb (length l) 1 then l 
    else 
    let (ll,lr) := split l in 
    merge (mergeSort ll) (mergeSort lr). 

Au lieu de cela, un peut utiliser la commande Program Fixpoint ou Definition avec le terme Fix (comme dans le livre de Chlipala).

Cependant, si je vous écris ce

Definition mergeSort : list nat -> list nat. 
refine (Fix lengthOrder_wf (fun (l: list nat) => list nat) 
     (fun (l : list nat) => (fun mergeSort : (forall ls : list nat, lengthOrder ls l -> list nat)=> 
          if leb (length l) 1 then 
          let (ll,lr) := split l in 
          merge (mergeSort ll _) (mergeSort lr _) 
          else 
          l))). 

je reçois des objectifs impossibles:

2 subgoals, subgoal 1 (ID 65) 

    l : list nat 
    mergeSort : forall ls : list nat, lengthOrder ls l -> list nat 
    ll, lr : list nat 
    ============================ 
    lengthOrder ll l 

subgoal 2 (ID 66) is: 
lengthOrder lr l 

C'est pourquoi Chlipala suggère de modifier la définition de mergesort cette façon:

Definition mergeSort : list nat -> list nat. 
    refine (Fix lengthOrder_wf (fun _ => list nat) 
       (fun (ls : list nat) 
       (mergeSort : forall ls' : list nat, lengthOrder ls' ls -> list nat) => 
       if Compare_dec.le_lt_dec 2 (length ls) 
       then let lss := split ls in 
         merge (mergeSort (fst lss) _) (mergeSort (snd lss) _) 
       else ls)). 

qui génère les objectifs suivants:

2 subgoals, subgoal 1 (ID 68) 

    ls : list nat 
    mergeSort : forall ls' : list nat, lengthOrder ls' ls -> list nat 
    l : 2 <= length ls 
    lss := split ls : list nat * list nat 
    ============================ 
    lengthOrder (fst lss) ls 

subgoal 2 (ID 69) is: 
lengthOrder (snd lss) ls 

Cette nouvelle définition me semble magique. Donc je me demande:

• A partir de la première définition, est-il encore possible de prouver le bien-être de la fonction?
• Sinon, pourquoi la première définition ne peut pas fonctionner?
• Comment un utilisateur de base peut-il passer facilement de la première définition à la seconde?

Answer 1

Il est facile de voir que vous devez faire deux changements pour accéder à la solution de A. Chlipala.

1) Quand vous faites split dont vous avez besoin en quelque sorte de se rappeler que ll et lr est venu de Split, sinon ils seraient des listes arbitraires, qui ne peuvent peut-être plus courte que la liste initiale l.

La pièce de code suivante ne parvient pas à enregistrer ce genre d'information:

let (ll,lr) := split l in 
    merge (mergeSort ll _) (mergeSort lr _) 

et, par conséquent, doit être remplacé par

let lss := split ls in 
    merge (mergeSort (fst lss) _) (mergeSort (snd lss) _) 

qui maintient ce que nous avons besoin.

L'échec est dû à l'incapacité de se rappeler que Coq ll et lr viennent de split l et cela se produit parce que let (ll,lr) est juste match déguisé (voir le manuel, §2.2.3).

Rappelons que les objectifs du schéma de correspondance est de (vaguement parler)

• déballer les composants d'une certaine valeur d'un type de données inductif et les lient à quelques noms (nous aurons besoin dans le 2ème partie de ma réponse) et
• remplacer la définition d'origine par ses cas spéciaux dans les branches de correspondance de motif correspondantes.

Maintenant, observer que split lne le fait pas se produit partout dans le but ou le contexte avant de modèle match là-dessus. Nous l'introduisons arbitrairement dans la définition. C'est pourquoi le pattern-matching ne nous donne rien - nous ne pouvons pas remplacer split l par son "cas particulier" ((ll,lr)) dans l'objectif ou le contexte, car il n'y a pas de split l partout.

Il existe une autre façon de le faire en utilisant l'égalité logique (=):

(let (ll, lr) as s return (s = split l -> list nat) := split l in 
    fun split_eq => merge (mergeSort ll _) (mergeSort lr _)) eq_refl 

Ceci est analogue à l'utilisation de la tactique remember. Nous nous sommes débarrassés de fst et snd, mais c'est une énorme exagération et je ne le recommanderais pas.

---

2) Une autre chose que nous devons prouver est le fait que ll et lr sont plus courtes que l quand 2 <= length l.

Depuis un if -expression est un match déguisé aussi bien (cela fonctionne pour tout type de données inductif avec exactement deux constructeurs), nous avons besoin d'un mécanisme de se rappeler que leb 2 (length l) = true dans la branche then. Encore une fois, puisque nous n'avons pas leb partout, cette information est perdue.

Il y a au moins deux solutions possibles au problème:

• soit nous nous souvenons leb 2 (length l) comme une équation (comme nous l'avons fait dans la 1ère partie), ou
• nous pouvons utiliser une fonction de comparaison avec le type de résultat se comporte comme bool (donc il peut représenter deux alternatives), mais il devrait également se rappeler quelques informations supplémentaires dont nous avons besoin. Ensuite, nous pourrions faire correspondre le résultat de la comparaison et extraire l'information, qui, bien sûr, dans ce cas doit être une preuve de 2 <= length l.

Ce que nous avons besoin est un type qui est capable de transporter une preuve de dans le cas où leb m n retours true et une preuve de, disons, m > n autrement. Il y a un type dans la bibliothèque standard qui fait exactement cela! Il est appelé sumbool:

Inductive sumbool (A B : Prop) : Set := 
    left : A -> {A} + {B} | right : B -> {A} + {B} 

{A} + {B} est juste une notation (sucre syntaxique) pour sumbool A B. Tout comme bool, il a deux constructeurs, mais en plus il se souvient de l'une des deux propositions A et B. Son avantage sur bool apparaît lorsque vous effectuez une analyse de cas avec if: vous obtenez une preuve de A dans la branche then et une preuve de B dans la branche else. En d'autres termes, vous arrivez à utiliser le contexte que vous avez sauvegardé auparavant, alors que bool ne porte aucun contexte (seulement dans l'esprit du programmeur).

Et nous avons besoin exactement de ça! Eh bien, pas dans la branche else, mais nous aimerions obtenir 2 <= length l dans notre branche then. Alors, laissez-nous demander Coq si elle a déjà une fonction de comparaison avec le type de retour comme ça:

Search (_ -> _ -> {_ <= _} + {_}). 

(* 
output: 
le_lt_dec: forall n m : nat, {n <= m} + {m < n} 
le_le_S_dec: forall n m : nat, {n <= m} + {S m <= n} 
le_ge_dec: forall n m : nat, {n <= m} + {n >= m} 
le_gt_dec: forall n m : nat, {n <= m} + {n > m} 
le_dec: forall n m : nat, {n <= m} + {~ n <= m} 
*) 

Tout des cinq résultats feraient, parce que nous avons besoin d'une preuve que dans un seul cas. Par conséquent, nous pouvons remplacer if leb 2 (length l) then ... par if le_lt_dec 2 (length l) ... et obtenir 2 <= length dans le contexte de preuve, ce qui nous permettra de terminer la démonstration.