Comment prouver une définition de preuve dans Coq

Question

Je travaille actuellement avec Coq et je rencontre un problème que je ne sais pas comment résoudre.

Supposons que nous travaillions avec un type donné, je prendrai nat pour l'exemple, et je veux utiliser une fonction f qui pourrait échouer. Pour compenser l'échec, nous définissons f comme étant de type nat -> option nat.

Maintenant, j'ai une hypothèse donnée H: nat -> bool en vertu de laquelle f ne manque pas, et je l'ai même prouvé le lemme

Lemma no_error_in_f : forall (n:nat), H n = true -> exists (u:nat), f n = Some u. 

Je veux définir une fonction g: nat->nat qui donne le résultat de f sur n si H n est satisfait, et donne simplement n sinon. Cette fonction devrait être bien définie, mais je ne sais pas comment la définir correctement. Si j'essaie quelque chose de naïf comme Definition g (n:nat) := if H n then f n else n., il y a un problème dans le système de frappe.

Est-ce que quelqu'un sait comment rassembler tous les éléments et dire au système que la définition est légale?

Answer 1

Je donne ici une solution qui fonctionne avec les mêmes hypothèses que celles données dans la question.

Axiom f : nat -> option nat. 
Axiom H : nat -> bool. 
Axiom no_error_in_f : forall n, 
    H n = true -> exists u, f n = Some u. 

Lemma no_error_in_f_bis : forall n, 
    H n = true -> f n <> None. 
Proof. 
    intros. apply no_error_in_f in H0. destruct H0. rewrite H0. discriminate. 
Qed. 

Definition g n := 
    match H n as b return H n = b -> _ with 
    | true => fun H => 
    match f n as f0 return f n = f0 -> _ with 
    | Some n0 => fun _ => n0 
    | None => fun H0 => match no_error_in_f_bis n H H0 with end 
    end eq_refl 
    | false => fun _ => n 
    end eq_refl. 

j'utiliser un autre lemme que no_error_in_f, qui est plus pratique pour prouver False. Notez que les deux idées de cette fonction (utiliser la construction return de match, détruire une preuve de False pour montrer qu'une branche n'est pas accessible) sont expliquées ici: http://adam.chlipala.net/cpdt/html/Subset.html.

Answer 2

Votre développement comporte deux problèmes. La première est que vous ne pouvez pas utiliser no_error_in_f pour définir g dans Coq sans supposer des axiomes supplémentaires, car Coq ne permet pas d'extraire des informations de calcul à partir d'une preuve (vérifiez here pour plus de détails). Un autre problème est que vous ne pouvez pas utiliser H dans une expression if, car elle renvoie un Prop au lieu d'un bool (vérifiez this answer pour plus de détails).

Answer 3

J'ai trouvé une façon de le faire, voici ma solution si quelqu'un est intéressé:

Definition g (n:nat) :nat := (match (H n) as a return a = H n -> nat with | true => (fun H_true => (match (f n) as b return b = f n -> nat with | Some u => (fun _ => u) | None => (fun H1 => False_rec _ (no_error_in_f H_true H1)) end) (eq_refl f n)) | false => n end) (eq_refl H n).

Pour ceux qui voudraient savoir ce que cela signifie, False_rec prendre comme second argument une preuve de False et certifie que l'appariement n'est pas possible. le terme

(match (f n) as b return b = f n -> nat with | Some u => (fun _ => u) | None => (fun H1 => False_rec _ (no_error_in_f H_true H1)) end) (eq_refl f n)) est de type f n = f n-> nat et quand je l'applique à l'épreuve eq_refl (f n) (ce qui est une preuve que f n = f n, donc est tapé f n = f n), j'obtenir un nat. Ceci est une astuce qui me permet d'obtenir H1 ce qui est une preuve que f n = None obtenu en utilisant le reflexevity de l'égalité et le pattern-matching, et que je vais utiliser dans ma preuve de False.

Il en va de même pour l'autre correspondance.