preuve de Quicksort en utilisant Coq

Question

Je suis en train d'écrire une thèse sur la vérification de programme de l'algorithme quicksort en utilisant le système Coq. J'ai défini un quicksort en Coq mais mon superviseur et moi-même ne sommes pas très à l'aise d'écrire la preuve en utilisant des tactiques. Y at-il quelqu'un qui peut aider avec cette section de la preuve coq? Ce qui suit est ce que nous sommes venus avec à ce jour:

Inductive nat : Type := 
    | O : nat 
    | S : nat -> nat. 

Check (S (S (S (S O)))). 

Definition isZero (n:nat) : bool := 
    match n with 
    O => true 
    |S p => false 
    end. 

Inductive List: Set := 
| nil: List 
| cons: nat -> List -> List. 

Fixpoint Concat (L R: List) : List := 
match L with 
| nil => R 
| cons l ls => cons l (Concat ls R) 
end. 

Fixpoint Less (n m:nat) := 
    match m with 
    O => false 
    |S q => match n with 
      O => true 
     |S p => Less p q 
     end 
    end.  

Fixpoint Lesseq (n m:nat) := 
    match n with 
    O => true 
    |S p => match m with 
      O => false 
      |S q => Lesseq p q 
      end 
    end. 

Fixpoint Greatereq (n m:nat) := 
    match n with 
    O => true 
    |S p => match m with 
      O => true 
      |S q => Greatereq p q 
      end 
    end. 


Fixpoint Allless (l:List) (n:nat) : List := 
    match l with 
    nil => nil 
    |cons m ls => match Less n m with 
       false => Allless ls n 
       |true => cons m (Allless ls n) 
       end 
end.    

Fixpoint Allgeq (l:List) (n:nat) : List := 
    match l with 
    nil => nil 
    |cons m ls => match Greatereq n m with 
       false => Allgeq ls n 
       |true => cons m (Allgeq ls n) 
       end 
end. 

Fixpoint qaux (n:nat) (l:List) : List := 
    match n with 
    O => nil 
|S p => match l with 
     nil => nil 
     |cons m ls => let low := Allless ls m in 
        (let high := Allgeq ls m in 
        Concat (qaux p low) (cons m (qaux p high))) 
     end 
end. 

Fixpoint length (l:List) : nat := 
match l with 
    nil => O 
|cons m ls => S (length ls) 
end. 

Fixpoint Quicksort (l:List) : List := qaux (length l) l. 

Je sais que pour une preuve de travailler nous avons besoin d'un lemme ou un théorème mais je ne sais pas où commencer après. Merci pour l'aide :)

Answer 1

Il ya beaucoup de bons théorèmes que vous pouvez prouver au sujet de votre code.

• Définissez une fonction pos qui mappe un nombre et une liste à l'index du nombre dans la liste.

• Th 1: pour toutes les listes S, et a, b en S, (a < = b) < -> (pos un (type S)) < = (pos b (type S)). Ce serait un théorème de correction pour la fonction de tri.

• Th 2: (tri (tri S)) = sort S

• définir les fonctions min et max pour trouver le minimum et le maximum des éléments de la liste S.

• Th 3: pos de l'élément minimal de la liste triée est 0.

• Th 4: les pos de l'élément maximal de l'inverse de la liste triée est 0.

Résumé d'un prédicat hors de votre routine de tri, afin que vous puissiez le passer en argument.

• Th 5: Montrer que (tri < = S) = (inverse (type> = S))

etc. Vous pouvez continuer cette ad infinitum. C'est trop marrant. :-)

Answer 2

Voir votre problème comme un problème de "test symbolique". Écrivez une fonction qui vérifie que votre sortie est correcte, puis montrez que toutes les combinaisons de votre code initial et de votre fonction de test fonctionnent comme prévu.

Voici ma fonction de test préférée pour un algorithme de tri sur votre type de données.

Fixpoint sorted (l : List) : bool := 
    match l with cons a l' => 
    match l' with cons b l'' => 
     if Lesseq a b then sorted l' else false 
    | nil => true 
    end 
    | nil => true 
    end. 

alors vous pouvez commencer une preuve de la manière suivante:

Lemma Quicksort_sorted : forall l, sorted (Quicksort l) = true. 

Mais vous devrez prouver beaucoup lemmes intermédiaires avant d'arriver à prouver le principal. La preuve formelle est vraiment comme le test, sauf que vous assurez une couverture complète du test.