What is the difference between “definition” and “inductive” in Coq?

Question

In Coq, you can use two different kinds of keywords to do definitions--Inductive and Definition. I do not understand the difference between an inductive and a definition, or when it is appropriate to use one instead of the other.

Could someone with experience in Coq please shed some light on this, or provide a reference that is more succinct/informative on this point than the standard Coq tutorial?

Update:

Here are some additional, generally quite basic questions I have about Coq:

• How do you force a set to be finite? Is there a "finite set" data type?
• What exactly do ":" and ":=" mean?

Answer 1

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 MSets.MSetAVL.