Mutual Global Fixpoints in SProp · Coq users

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?

Gaëtan Gilbert (Nov 13 2023 at 17:19):

D.G. Berry (Nov 13 2023 at 17:27):

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.

D.G. Berry (Nov 13 2023 at 17:31):

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.

D.G. Berry (Nov 13 2023 at 17:33):

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

Gaëtan Gilbert (Nov 13 2023 at 17:51):

D.G. Berry (Nov 13 2023 at 17:54):

Gaëtan Gilbert (Nov 13 2023 at 18:03):

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 *)

D.G. Berry (Nov 13 2023 at 18:05):

Gaëtan Gilbert (Nov 13 2023 at 18:15):

D.G. Berry (Nov 14 2023 at 10:50):

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?

D.G. Berry (Nov 14 2023 at 12:25):

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

Gaëtan Gilbert (Nov 14 2023 at 12:44):

Inductive thing : SProp :=.

Fixpoint foobar (x:thing) {struct x} : thing.
Proof.
  Guarded.
  exact x.
  Guarded.
Defined.

D.G. Berry (Nov 14 2023 at 13:07):

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

Gaëtan Gilbert (Nov 14 2023 at 13:10):

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

D.G. Berry (Nov 14 2023 at 13:19):

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.

Gaëtan Gilbert (Nov 14 2023 at 13:33):

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) *)

Stream: Coq users

Topic: Mutual Global Fixpoints in SProp

D.G. Berry (Nov 13 2023 at 17:15):