6
$\begingroup$

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.

$\endgroup$
1

4 Answers 4

7
$\begingroup$

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.

$\endgroup$
7
  • 2
    $\begingroup$ You seem to be implying that any predicate defined with Fixpoint is decidable. Is that really your intention? $\endgroup$ May 1, 2023 at 0:08
  • $\begingroup$ Sorry that is not what I intended to say. Fixpoint must define some finite computation. In that sense they define something that can be computed. But the logical predicate resulting of this computation may be undecidable. I am not a specialist but I tend to recommend using inductive predicates in this case because the « computable » part is not very useful. $\endgroup$ May 1, 2023 at 20:12
  • 1
    $\begingroup$ In that case, perhaps the last sentence of your answer can be deleted, as it is misleading as written. (And saying that "fixpoint must define some finite computation" isn't quite accurate, either. Fixpoints don't define "computations", they define elements of types, just like all other definitions in Coq. In the particular case when a fixpoint defines a function, that function is total and it therefore normalizes (computes) in finite number of steps – and that's what you likely meant, yes?) $\endgroup$ May 1, 2023 at 20:45
  • $\begingroup$ I am not sure of what would be a fixpoint not defining a function. Would the following be correct?: Moreover inductive relations allow to define much more relations than fixpoint because the use of recursion is not expected to define always terminating computations. ” $\endgroup$ May 2, 2023 at 15:04
  • $\begingroup$ Since you insist: fixed points are more general than inductive types because inductive types are a special case of fixed points. $\endgroup$ May 2, 2023 at 17:38
4
$\begingroup$

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.

$\endgroup$
2
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ The example OP provided (In) is 'non-deterministic' and yet can be defined using Fixpoint so the distinction is not as strict as you make it to be. $\endgroup$
    – gallais
    May 1, 2023 at 22:23
-2
$\begingroup$

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

$\endgroup$
1
  • 3
    $\begingroup$ This question asks about the intersection of the two cases where you are defining a function from an inductive type to a universe (usually Prop) that has both a natural Inductive type constructor definition and a natural Fixpoint definition. (If you replace Prop with Bool, then Fixpoint would be the way to go of course.) $\endgroup$
    – Jason Rute
    Apr 30, 2023 at 10:56

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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