# Induction error on mutually defined types in Coq

I want to define two types that depend on each other

Inductive formula_neutral (A : Set) := variable (P : A) | and (p q : formula_charged A).

Inductive formula_charged (A : Set) := positive (p : formula_neutral A) | negative (p : formula_neutral A).


I know that this is not possible in Coq, so I did the following (as I saw in some sample code):

Inductive formula_type := neutral | charged.

Inductive formula (A : Set) : formula_type -> Set :=
| variable (V : A) : formula A neutral
| and (p q : formula A charged) : formula A neutral
| positive (p : formula A neutral) : formula A charged
| negative (p : formula A neutral) : formula A charged.


This solution works, but when I have to prove goals like P p by induction on p (where P : formula A charged -> Prop), the command induction p fails with the message Abstracting over the term "p" leads to a term [...] which is ill-typed, I guess because it generates a subgoal where p = variable V which makes P p ill-typed, etc.

Alternative question: I want to define a logic where $$\neg \neg p \equiv p$$. I previously tried to model it with the semantics, but it gets very messy, so it tried to impose it syntactically as described above. Do you have any tips on how to do it?

You can define mutual inductive types in Coq. In your case, that would look like

Inductive formula_neutral (A : Set) : Set :=
| variable (P : A)
| and (p q : formula_charged A) with

formula_charged (A : Set) : Set :=
| positive (p : formula_neutral A)
| negative (p : formula_neutral A).


The recursion principle generated by default by Coq is not very good, you might want to look as Scheme to derive better ones.

As for your second question, intuitively your problem comes from the fact that you only provide the predicate for charged, but your induction also has to handle the neutral cases. Instead of trying to prove forall p : formula charged, P p, you should rather try to prove forall (x : formula_type) (p : formula x), P' x p, and there induction will succeed. The definition of P' can be something like fun x => match x with | neutral => Q | charged => P end, and then you'll recover what you wanted to do… except now you also have to provide the predicate Q to handle the neutral case.

As for your last question, it might deserve its own post, and currently is rather vague, so it is hard to answer. But I just want to point out that if all you wish to have is Coq + classical logic, you can simply work in with an axiom Axiom dneg_elim : forall P : Prop, ~ ~ P -> P, in vanilla Coq.

• As for your first tip: thanks, I didn't know that. It also makes a nicer definition and I can also declare positive as a coercion and hence have a nicer syntax :) I've never used the Scheme command and I'd never think that could be useful for my problem. Jul 12, 2023 at 18:15
• As for your second tip: I've thought of that, but makes things less natural. For example, one of the first things I have to define is a predicate models : structure -> formula charged -> Prop, which doesn't make much sense on formula neutral. Of course I can define a models_aux, but it makes things a bit cluncky for me. Jul 12, 2023 at 18:17
• As for you third answer: I know, but I want to define a logic langugage separate from the already existing Coq logic, using the latter as a meta logic. I could define an axiom forall S P, models S (~ ~ P) -> models S P (haven't tried yet). Jul 12, 2023 at 18:19