What does fun keyword do in Coq?

Question

I am struggling to understand the meaning of keyword 'fun' in Coq.

There are types all and function 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.

And theorem:

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

I understand the left part but confused on what fun is doing on the right side of the <->.

Answer 1

Isn't it simply like a lambda, i.e., isn't here fun x => ... simply like \x -> ... in Haskell?

There is another interesting peculiarity of that fun ... in your code. The type of the result of that function in your code must be proposition (Prop), not boolean. The expression test x = true must be of that type, so we conclude that = in coq denotes propositions about equality, not the boolean binary operation (which is known as == in Haskell; we don't see this from your example, but perhaps coq's notation is similar).

So, although the idea of this fun ... is just a lambda, it is a bit unusual from Haskell's point of view, because here it introduces a function operating on type-level (the result type is Prop), not value-level (only the latter must be possible--or at least the usual usage--for \ x-> ... in Haskell). coq's Prop is on the same level as * in Haskell, isn't it?

And all X P in this code is like a type constructor (well, a parameterized family of type constructors) in Haskell, but a dependent one, of type [X] -> * (in Haskell's notation). all_nil and all_cons are like data constructors for this new type.