Que fait un mot-clé amusant dans Coq?

Question

J'ai du mal à comprendre la signification du mot-clé 'fun' dans Coq.

Il existe plusieurs types tous et la fonction forallb:

Inductive all (X : Type) (P : X -> Prop) : list X -> Prop := 
    | all_nil : all X P [] 
    | all_cons : forall (x:X) (l: list X) , P x -> all X P l -> all X P (x::l). 

Fixpoint forallb {X : Type} (test : X -> bool) (l : list X) : bool := 
match l with 
| [] => true 
| x :: l' => andb (test x) (forallb test l') 
end. 

et le théorème:

Theorem all_spec: forall (X:Type) (test : X -> bool) (l: list X), 
    forallb test l = true <-> all X (fun x => test x = true) l. 

Je comprends la partie gauche, mais confus sur ce plaisir fait sur le côté droit du < -> .

Answer 1

est-il pas simplement comme un lambda, à savoir, n'est pas ici fun x => ... simplement comme \x -> ... dans Haskell?

Il y a une autre particularité intéressante de ce fun ... dans votre code. Le type du résultat de cette fonction dans votre code doit être proposition (Prop), et non booléen. L'expression test x = true doit être de ce type, donc nous concluons que = dans coq dénote des propositions sur l'égalité, pas l'opération booléenne binaire (qui est connue sous le nom == dans Haskell, nous ne voyons pas cela de votre exemple, mais peut-être la notation de coq est similaire). Alors

, bien que l'idée de ce fun ... est juste un lambda, il est un peu inhabituel du point de vue de Haskell, car ici, il introduit une fonction d'exploitation sur le type de niveau (le type de résultat est Prop), non niveau de valeur (seul ce dernier doit être possible - ou au moins l'usage habituel - pour \ x-> ... dans Haskell). coq's Prop est sur le même niveau que * dans Haskell, n'est ce pas?

et all X P dans ce code est comme un constructeur de type (bien, une famille paramétrée de constructeurs de type) dans Haskell, mais une dépendante, de type [X] -> * (en notation Haskell). all_nil et all_cons sont comme les constructeurs de données pour ce nouveau type.