Apologies if this has been answered elsewhere: I cannot find anything after some searching. I cannot make a mutual global(?) fixpoint from SProp into SProp pass the typechecker, even though I can write the analogous term as a mutual local(?) fixpoint. Even running Guarded only after giving the declaration fails. Is there some way to force Coq into accepting it?

could be a bug, can you show an example?

```
Inductive IsNeutral {Gamma : Ctxt} : forall {T}, Tm Gamma T -> SProp :=
| IsNeutralVar {T} (i : Idx Gamma T) : IsNeutral (Var i)
| IsNeutralApp {T T'} {t0 : Tm Gamma (Arr T T')} {t1 : Tm Gamma T} : IsNeutral t0 -> IsNormal t1 -> IsNeutral (App t0 t1)
with IsNormal {Gamma : Ctxt} : forall {T}, Tm Gamma T -> SProp :=
| IsNormalNeutral {t : Tm Gamma Iota} : IsNeutral t -> IsNormal t
| IsNormalAbs {T T'} {t : Tm (Snoc Gamma T) T'} : IsNormal t -> IsNormal (Abs t).
Fixpoint IsNeutralDCR {Gamma Delta : Ctxt} {T : Ty} {t : Tm Delta T} (X1 : IsNeutral t) {struct X1} : (forall (rho : CtxtRnm Gamma Delta), IsNeutral (DoCtxtRnm t rho)) : SProp
with IsNormalDCR {Gamma Delta : Ctxt} {T : Ty} {t : Tm Delta T} (X1 : IsNormal t) {struct X1} : (forall (rho : CtxtRnm Gamma Delta), IsNormal (DoCtxtRnm t rho)) : SProp.
Fail Guarded.
```

This fails. I appreciate that this is not a standalone example, but when I tried to create something standalone it did not fail. Although it was not using indexed inductive families.

It fails with: "Recursive definition of IsNeutralDCR is ill-formed. Fixpoints on proof irrelevant inductive types should produce proof irrelevant values."

what Coq version?

v8.18.0

it's a bug, can reproduce with

```
Axiom Ctxt : Type.
Axiom Ty : Type.
Axiom Tm : forall c:Ctxt, Ty -> Type.
Axiom CtxtRnm : Ctxt -> Ctxt -> Type.
Axiom DoCtxtRnm : forall {c c' T}, Tm c T -> CtxtRnm c' c -> Tm c' T.
Inductive IsNeutral {Gamma : Ctxt} : forall {T}, Tm Gamma T -> SProp :=
with IsNormal {Gamma : Ctxt} : forall {T}, Tm Gamma T -> SProp :=
.
Fixpoint IsNeutralDCR {Gamma Delta : Ctxt} {T : Ty} {t : Tm Delta T} (X1 : IsNeutral t) {struct X1} : (forall (rho : CtxtRnm Gamma Delta), IsNeutral (DoCtxtRnm t rho)) : SProp
with IsNormalDCR {Gamma Delta : Ctxt} {T : Ty} {t : Tm Delta T} (X1 : IsNormal t) {struct X1} : (forall (rho : CtxtRnm Gamma Delta), IsNormal (DoCtxtRnm t rho)) : SProp.
Proof.
Fail Guarded. (* fails *)
all:destruct X1.
Defined. (* also fails *)
```

Thanks for doing the work to figure this out! It would be a problem with https://github.com/coq/coq/blob/b10573deb4f3e0aecf74692af95f84127576c8d9/kernel/inductive.ml#L1438 .

https://github.com/coq/coq/issues/18308

Is the only workaround to use local mutual fixpoints, and thereby duplicate the definition? Or is there some flag that can be (un)set to disable such checking?

FYI, I am hitting it again but this time not with a mutual inductive. So that cannot be a contributing factor.

yes it can be reproduced with as little as

```
Inductive thing : SProp :=.
Fixpoint foobar (x:thing) {struct x} : thing.
Proof.
Guarded.
exact x.
Guarded.
Defined.
```

But not all fixpoints in SProp exhibit this buggy behaviour? What are the conditions to trigger it?

it needs to be an interactive fixpoint, so eg `Fixpoint foo (x:thing) := x`

would work

Let me (re)clarify my earlier message. I was misremembering that non-mutuals have a convenient fix: to move to using the fix tactic; but that mutuals do not have this fix so conveniently. One can only extract out one of the mutuals from a local mutual fixpoint.

you can extract it if you're willing to use low level ltac2

```
Definition even :=
fix even n := match n with 0 => true | S n => negb (odd n) end
with odd n := match n with 0 => false | S n => negb (even n) end
for even.
Require Import Ltac2.Ltac2.
Definition odd :=
ltac2:(
let c := Std.eval_unfold [(reference:(even),Std.AllOccurrences)] constr:(even) in
match Constr.Unsafe.kind c with
| Constr.Unsafe.Fix structs which names bodies =>
let c := Constr.Unsafe.make (Constr.Unsafe.Fix structs 1 names bodies) in
exact $c
| _ => Control.throw Assertion_failure
end).
Print odd.
(* ... for odd *)
Check fun n => eq_refl : odd (S n) = negb (even n).
Eval simpl in fun n => even (S n).
(* fun n => negb (odd n) *)
```

Last updated: Oct 08 2024 at 15:02 UTC