Can we define recursive definitions in Coq?

Question

I know Coq allows to define mutually recursive inductive types. But is there a way to write the recursive definitions in Coq?

For example, I want to write a definition as:

Definition myDefinition A := forall B C, (myDefinition B) \/ (A = C).

Important part in above definition is myDefinition B, which is recursively calling the same definition on another argument. Is it possible to do this in Coq?

Do you intend A to be a piece of data (like a number or a string), if that is the case, then recursion is strictly restricted by the inductive structure of the datatype. — Yves

Théo Winterhalter Théo Winterhalter · Accepted Answer · 2020-11-04T08:42:53

You can use Fixpoint instead of Definition. I encourage you to look at the documentation if you want to know more about them.

Fixpoint myDefinition A := 
  forall B C, (myDefinition B) \/ (A = C).

Note that something like the above wouldn't be accepted as terminating by Coq and hence as a valid definition. Once again, the documentation should explain what you can and can't do with examples.

Edit

If you definition is supposed to be a type, then you can also define it as an inductive type.

Inductive myDefinition (A : Prop) : Prop :=
| myDef : forall B C, (myDefinition B) \/ (A = C) -> myDefinition A.

Here we say that to build a proof of myDefinition A it is sufficient to prove forall B C, (myDefinition B) \/ (A = C). Which is what you wanted. You will probably have a hard time proving it however, but perhaps your concrete case is different.

Can we define recursive definitions in Coq?

1 Answers