4
$\begingroup$

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?
$\endgroup$
  • $\begingroup$ I'm not sure whether this question is on-topic here. We've had an inconclusive discussion on the topic. If we decide that the question is off-topic, we'll migrate it to Stack Overflow where it is on-topic. $\endgroup$ – Gilles May 16 '13 at 0:03
  • $\begingroup$ : and := have different meanings in different contexts. $\endgroup$ – Gilles May 16 '13 at 0:03
4
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ How does one use Sets.FiniteSets? $\endgroup$ – Philip White May 16 '13 at 3:34

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.