Inductive vs. recursive definitions

Question

In Coq there are two ways to define a new type on an inductive type: Using Inductive and using Fixpoint. What are pros and cons of these approaches? Some aspects in which they can be compared: Difficulty of interacting with them (proofs, constructions). How large are the generated internal terms? Effects on performance.

Example:

Inductive list (A : Type) : Type :=
| nil : list | cons : A -> list -> list.

Inductive In {A : Type} (a : A) : list A -> Prop :=
| In_cons_hd (l : list A) : In (cons a l)
| In_cons_tl (hd : A) (tl : list A) : In tl -> In (hd :: tl).

Fixpoint In' {A : Type} (a : A) (l : list A) : Prop :=
  match l with
  | nil => False
  | cons hd tl =>
    a = hd \/ In' a tl
  end.

Theorem In_equiv (A : Type) (a : A) (l : list A) :
  In a l <-> In' a l.

If Inductive is used, one has to use the destruct, induction, inversion and constructor tactics (or explicitly choose a constructor using apply). This makes it harder to write proof terms manually, I think.

If Fixpoint is used and (in the above example) the list starts with constructors, the computation will take care of these steps.

Sometimes the Fixpoint is not definable in Coq, because of issue #1433.

Edit: Using Fixpoint made more "primitive logical operations" (conj., disj., quantifiers) appear in my proofs, which firstorder could process and often solve quickly.

Edit 2, regarding Fixpoint being "strongly normalizing": I think this is not that much of a problem per se, if enough disjunctions are used. I see another difficulty with Fixpoint. The recursive property must be structurally (or well-founded) recursive in the data, for all possible input data. (Proven at the time of definition)

So for example a sequent calculus is "easily" definable using Fixpoint if it has the subformula property, or if we add a dummy natural number as "fuel", which must decrease when going up in the deduction tree. Calculi without subformula property probably can't be to translated directly from Inductive to Fixpoint.

Answer 1

Defining recursive properties by fixpoint is possible, but it is usually easier to reason on inductively defined ones. Mostly because they come with their own induction principles. If you use fixpoint then you are forced to use the inductive principles of the underlying data type (lists in your case). In your example it makes no difference but most of the time it does.

Moreover inductive relations allow to define much more relations than fixpoint because the use of recursion is not expected to define always terminating computations.

Answer 2

Let me just mention a third possibility which is sometimes called "small inversion". This is some kind of middle ground between the two possibilities you present, which gives you some of the advantages of the Fixpoint-style definition on top of an Inductive-style one. Here is an example:

Definition In'' {A : Type} (a : A) (l : list A) : Prop :=
  match l with
  | nil => False
  | cons hd tl =>
    a = hd \/ In a tl
  end.

Theorem In_equiv (A : Type) (a : A) (l : list A) :
  In a l <-> In'' a l.

The main difference is that In'' is not a fixpoint, because it does not call itself – only In. However, proving In_equiv is rather easy, and then applying it in an hypothesis/goal you can trigger just the amount of computation that the Fixpoint-based definition would give you. As the name "small inversion" suggest, this can be seen as an alternative, more controlled approach to inversion and the related tactics for indexed inductive types.

Answer 3

Inductive allows you to express non-deterministic, non-terminating computations, while Fixpoint computations can be automatically reduced ("normalized") by cbv/compute and cbn/simpl.

A Fixpoint term is strongly normalizing: for any fixpoint f, there's exactly one value which f v0 v1 ... reduces to, and you can get it with cbv or compute [3]. An Inductive term is not, which means there may be multiple ways to construct an instance f v0 v1 ..., or none at all, and you must find them manually with apply/constructor (to construct the instance), inversion (to reveal how the instance was constructed), and/or other tactics.

Repeating tactics on inductives [1] can also create loops and hang your Coq process [2]. For example, repeat apply cons if your goal is a list, or repeat inversion on a list hypothesis, will hang while generating the infinite term (cons ?a (cons ?b (cons ?c .... repeat cbv, repeat cbn, repeat compute, and repeat simpl will never hang; in fact, when you call any of these tactics once, calling them again is guaranteed to do nothing.

Generally, you want to define a Fixpoint when it's easy enough to do so, and Inductive otherwise. Sometimes your computation is too complex to define in Fixpoint even when it's deterministic and guaranteed to terminate (specifically, when it uses non-structural recursion). In this case, you can either use Program Fixpoint, Function, or Equations (from the coq-equations plugin), and then prove or just Admit the additional "obligations"; or you can use Inductive and you don't have to prove termination at all. Even when you can prove the obligations from Program Fixpoint/Function/Equations, those don't have as good UX as Fixpoint, and it may be easier to use Inductive when they are the only alternative.

There are also libraries like ssreflect which try to achieve the best of both worlds for usability: you define both the Inductive and Fixpoint definitions of a computation, and can switch ("reflect") between them. Similarly, there may be a case where you have an intuitive Inductive definition and an unintuitive Fixpoint definition, and you want to prove they are equivalent (e.g. you are extracting Fixpoint definition and want it to match the Inductive specification).

---

[1] e.g. when using Ltac to try and automate constructing or "reducing" the inductive type

[2] Tip: when using coq with emacs and proof-general, use Set Default Timeout to prevent the process from permanently hanging and requiring you to restart coqtop

[3] Sometimes you want extra control like what you get by manually constructing/destructing inductives: sometimes the normal form you get via cbv/compute is too far reduced, and you must "undo" some of the computation via change (which is also manual) or other rewriting. This is where cbn and simpl come in, they're explicitly designed to prevent "bad" reductions and usually you want to use them instead of cbv or compute. When you need even more control, you can provide arguments to cbn/simpl or use unfold.

Answer 4

As far as I can know, Inductive is used to define an inductive type, and Fixpoint a function on an inductive type.