Defining 2 inductive propositions relying on each other in Coq

Question

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

Answer 1

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 :=
  | evenO : even 0
  | evenS n : odd n -> even (S n)
with odd : nat -> Prop :=
  | oddS n : even n -> odd (S n).

Since you do not describe how you define your notion of formula or of occurrence of an atom, I'm not sure how exactly to make this idea fit your needs. I'll let you try and adapt it yourself.

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.