# Defining 2 inductive propositions relying on each other in Coq

I'm pretty beginner in Coq. I want to formalize negative and positive occurrence of an atom in a proposition inside coq the definition is as down below:

I want to define this property as an Inductive prop so I use it with more ease in proving theorems (such as interpolation) but the problem is positively occurrence and negatively occurrence are defined with each other and I don't know how to do that.
I also thought of a Fixpoint function which returns option bool which false is equivalent to negative occurrence and true is equivalent to positive occurrence and None to no occurrence but it seems like a messy way to do it

• Please don't use images for text/math content of your post. This makes your question impossible to search and inaccessible to the visually impaired; we don't like that. Please transcribe text and mathematics. You can use LaTeX.
– D.W.
Commented Jul 8, 2023 at 6:35
• Please credit the original source of all material originally written by others. See cs.stackexchange.com/help/referencing
– D.W.
Commented Jul 8, 2023 at 6:35

You can use mutually defined inductive types, using the with construct. Here is the standard simple example on how to do that:
Inductive even : nat -> Prop :=

Note that there are other ways to go about this than indexed inductive proposition. Your fixpoint idea seems like it can definitely work, and depending on the task might be better suited than the inductively defined solution. Also, instead of mutually defining the positive and negative occurrences, you can also define a single inductive proposition, say occurrence_variance : occurrence -> formula -> bool -> Prop, where occurrence_variance o f true means the occurrence o in f is a positive one, and occurrence_variance o f false in f is a negative one. This gives you the benefit of inductive definition for doing proofs by induction, but should cut down nicely on the duplication you'll get with the mutual approach.