Recherche récursive dans une liste dans Coq

Question

En essayant de rechercher un objet dans une liste, et peut-être retourner vrai si elle est trouvée; faux sinon.

Cependant, ce que j'ai essayé de trouver est incorrect. J'apprécierais vraiment quelques conseils. J'ai besoin de la fonction pour rechercher dans la liste des éléments en comparant la tête de la liste avec l'élément concerné, sinon une correspondance, puis récursivement mettre le reste de la liste à travers la fonction et répéter, en faisant correspondre la tête de la liste.

Fixpoint find (li:list Interface){struct li}: list Interface := 
match li with 
| nil => nil 
| y::rest => find rest 
end. 

Vos conseils et votre aide sont très appréciés.

Nous vous remercions à l'avance

Answer 1

Hmmm, je ne vais pas gâcher le plaisir en donnant le code de travail :). Tu manques évidemment quelque chose. Est-ce votre problème de coder en Coq ou est-ce plus général? Comment l'écririez-vous en pseudo-code? Ou dans une autre langue que vous connaissez?

Answer 2

Il existe une fonction très similaire dans la théorie List dans la bibliothèque standard. Cette fonction prend un prédicat en tant qu'argument, c'est-à-dire une fonction f du type d'élément à bool et renvoie Some x si un élément correspondant x est trouvé ou None si aucun n'est trouvé.

Variable A : Type. 
Fixpoint find (f:A->bool) (l:list A) : option A := 
    match l with 
    | nil => None 
    | x :: tl => if f x then Some x else find tl 
    end. 

Vous êtes à la recherche d'un élément qui est égal à un objet particulier a. Cela signifie que votre prédicat est eq_Interface a, où eq_Interface est l'égalité que vous voulez sur le Interface. C'est à vous de définir une fonction d'égalité sur votre type, car il peut y avoir plusieurs définitions d'égalité. Coq définit =, qui est Leibniz equality: deux valeurs sont égales ssi il n'y a aucun moyen de les distinguer. = est une proposition, pas un booléen, parce que cette propriété n'est pas décidable en général. Ce n'est pas toujours l'égalité désirable sur un type, parfois vous voulez une relation d'équivalence plus grossière, de sorte que deux objets peuvent être considérés égaux s'ils ont été construits de différentes manières mais ont néanmoins le même sens.

Si Interface est un type de données simple - intuitivement, une structure de données sans proposition intégrée - il y a une tactique intégrée pour construire une fonction d'égalité structurelle à partir de la définition de type. Rechercher decide equality dans le manuel de référence.

Definition Interface_dec : forall x y : Interface, {x=y} + {x <> y}. 
Proof. decide equality. Defined. 
Definition Interface_eq x y := if Interface_dec x y then true else false. 

non seulement vous indique si ses arguments sont égaux, mais est également livré avec une preuve que les arguments sont égaux ou qu'ils sont différents.

Une fois que vous avez cette fonction d'égalité, vous pouvez définir votre fonction find en termes de la fonction de la bibliothèque standard:

Definition Interface_is_in x := if List.find (Interface_eq x) then true else false.