Correspondance de modèle en utilisant les informations des théorèmes

Question

J'ai la question suivante, regardez dans le code.

(* Suppose we have type A *) 
    Variable A: Type. 

    (* Also we have a function that returns the type (option A) *) 
    Definition f_opt x: option A := ... 

    (* Then, I can prove that this function always returns something: *) 
    Theorem always_some: forall x, exists y, f_opt x = Some y. 
    Admitted. 

    (* Or, equivalently: *) 
    Theorem always_not_none: forall x, f_opt x <> None. 
    Admitted. 

Maintenant, je voudrais obtenir une version de f_opt qui retourne toujours une valeur de type A. Quelque chose comme ceci:

Definition f x: A := 
    match f_opt x with 
     | Some y => y 
    end. 

Mais je reçois l'erreur suivante:

Non exhaustive pattern-matching: no clause found for pattern None .

Je comprends que je dois faire une sorte de travail avec des types, mais je ne comprends pas ce que je dois faire exactement.

Answer 1

En La théorie sous-jacente de Coq, chaque correspondance de modèle doit être exhaustive - c'est-à-dire qu'elle doit considérer explicitement tous les constructeurs du type inductif en question. C'est pourquoi vous obtenez le message d'erreur que vous avez vu.

Comment contourner cette restriction? Il y a quelques solutions. Voyons d'abord comment convaincre Coq que la branche None ne peut jamais se produire. Pour cela, nous utiliserons votre théorème always_not_none:

Definition f x : A := 
    match f_opt x as res return res <> None -> A with 
    | Some y => fun _ => y 
    | None => fun H => match H eq_refl with end 
    end (always_not_none x). 

Ce code peut paraître étrange à première vue, mais il effectue presque le match de modèle que vous voulez. Pour expliquer à Coq que le cas None ne se pose jamais, il combine always_not_none avec le fait que f_opt x = None sur cette branche pour dériver une contradiction. C'est le terme H eq_refl sur cette branche. Ensuite, le match sur cette contradiction suffit à convaincre Coq que la branche est fausse. Un peu plus formellement, parce que False, la proposition contradictoire, est définie sans aucun constructeur, quand nous faisons correspondre sur un terme de type False, il n'y a pas de branches à traiter, et l'expression entière peut retourner tout type que nous voulons - dans ce cas, A.

Ce qui est étrange à propos de ce code est le type annotations sur la correspondance, et qu'il renvoie une fonction à la place de quelque chose de type A directement. Cela est dû au fait que la correspondance de pattern depend fonctionne dans Coq: chaque fois que nous voulons utiliser les informations que nous obtenons d'une branche particulière d'une correspondance (ici, f_opt x est égal à None dans cette branche), nous devons explicitement faire le match retourner une fonction - ce que Adam Chlipala appelle le convoy pattern. Ceci est fait pour que Coq sache où vous prévoyez d'utiliser cette information supplémentaire et vérifie que c'est fait correctement. Ici, nous utilisons que f_opt x est None pour nourrir l'hypothèse nécessaire par always_not_none x pour dériver une contradiction.

Bien que cela résoudra votre problème, je vous déconseille généralement de le faire de cette façon. Par exemple, si vous savez que votre type A est habité par un élément a : A, alors vous pouvez simplement faire f retourner a sur cette branche.Cela a l'avantage d'éviter de mentionner des preuves dans vos fonctions, ce qui est souvent gênant lors de la simplification et de la réécriture des termes.

Answer 2

Vous aurez besoin de mettre votre preuve existentielle always_not_none dans Set ou Type de le faire:

Theorem always_some: forall x, { y: A & f_opt x = Some y}. 
... 
Qed. 

Ensuite, vous pouvez effectuer les opérations suivantes (ou utilisez refine ou Program):

Definition f (x: B) : A := 
    let s := always_some x in let (x0, _) := s in x0. 

Answer 3

en utilisant le module Program Coq, vous pouvez écrire un match de modèle exhaustif, mais annoter que certaines branches doivent être impossibles à atteindre et fournir plus tard la preuve que ce soit le cas:

Require Import Program. 
Program Definition f x : A := 
match f_opt x with 
| Some a => a 
| None => ! 
end. 
Next Obligation. 
destruct (always_some x). congruence. 
Qed. 

(Le module Program fait beaucoup de travail dans les coulisses que dans une définition explicite complète que vous auriez à écrire en utilisant le "modèle de convoi" Sachez, cependant, que parfois Program a tendance à générer beaucoup de dépendances sur JMeq et l'axiome JMeq_eq lorsqu'il dépend les types sont impliqués, même si cela n'est pas nécessaire.)