0
$\begingroup$

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:
enter image description here

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

$\endgroup$
2
  • $\begingroup$ 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. $\endgroup$
    – D.W.
    Jul 8, 2023 at 6:35
  • $\begingroup$ Please credit the original source of all material originally written by others. See cs.stackexchange.com/help/referencing $\endgroup$
    – D.W.
    Jul 8, 2023 at 6:35

1 Answer 1

2
$\begingroup$

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.

$\endgroup$

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.