Je suis un débutant dans l'utilisation de Coq. Je veux demander si je veux définir un ensemble comme , comment pourrais-je faire cela? J'écris quelque chose comme:Dans Coq, comment définir un ensemble comme A = {x | f (x) = 0}?
Definition f0 := nat->nat.
Definition A : Set :=
forall x, f0 x -> 0.
Ils ne fonctionnent pas comme prévu.
Merci beaucoup.
Plus ou moins comme vous avez écrit. Tout d'abord, vous devez avoir une fonction f0 : nat -> nat à laquelle vous souhaitez appliquer cette définition. Ce que vous avez fait ici
Definition f0 := nat -> nat.
était de nommer le type nat -> nat des fonctions de Naturals à Naturals f0. Vous avez probablement eu à l'esprit quelque chose comme ceci:
Variable f0 : nat -> nat.
Ceci déclare une f0 variable qui appartient au type nat -> nat. Maintenant, nous pouvons adapter votre description originale au code Coq:
Definition A : Set := {x : nat | f0 x = 0}.
Il y a deux choses à savoir ici. Tout d'abord, vous voudrez peut-être appliquer cette définition ultérieurement à une fonction particulièref0 : nat -> nat, telle que la fonction précédente pred : nat -> nat. Dans ce cas, vous devez placer votre code dans une section:
Section Test.
Variable f0 : nat -> nat.
Definition A : Set := {x : nat | f0 x = 0}.
End Test.
En dehors de la section, A est en fait une fonction (nat -> nat) -> Set, qui prend une fonction f0 : nat -> nat du type {x : nat | f0 x = 0}. Vous pouvez utiliser A comme vous utiliseriez n'importe quelle autre fonction, par ex.
Check (A pred).
(* A pred : set *)
La deuxième chose que vous devez garder à l'esprit est que Set en Coq est pas la même chose comme un ensemble en mathématiques conventionnelles. En math, un élément de l'ensemble {x | f(x) = 0} est aussi un élément de l'ensemble des nombres naturels. Mais pas dans Coq. Dans Coq, vous devez appliquer une fonction de projection explicite proj1_sig pour convertir un élément de {x : nat | f0 x = 0} en nat.
Merci beaucoup, c'est tellement parfait! :) –