Inductive creates a new type and gives it a name. It is similar to
datatype in SML,
data in Haskell,
type (defining an ordinary variant or a record) in Ocaml.
In addition to defining the type,
Inductive also defines induction principles for that type. These induction principles aren't necessary from a theoretical point of view: all they do is to give a name to a particular well-typed term. They are provided because while you could write that term in your proof, it is mechanical and repetitive.
Definition gives a name to a term. It's broadly similar to
let in SML or Ocaml or Haskell (but it doesn't let you write recursive definitions as such). Since Coq is pure (no side effects), if you write two definitions with the same right-hand side, the resulting names are equal. You can use
Definition at any level of the sort hierarchy, including for types (in which case the definition is similar to
type aliases in SML, Ocaml or Haskell).
Fixpoint is similar to
Definition, but allows a recursive definition (like
let rec in ML). It's in fact syntactic sugar for
Definition plus the explicit fixpoint combinator
fix, but definitions made using
Fixpoint are easier to read and write.
The best way to understand these is to write a few proofs about some datatype. Try to rewrite some parts of the
List library, for example.
There are several ways to implement finite sets in Coq. To to set theory proofs, try
Sets.Finite_sets. If you want to have decent extracted code, use