CODEWITHSUNDEEP
coqtheorem-provingcoqide
Baber
Baber

Reputation: 321

Can we define recursive definitions in Coq?

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?

Upvotes: 1

Views: 702

Answers (1)

Théo Winterhalter
Théo Winterhalter

Reputation: 5108

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.

Upvotes: 3

Related Questions