Stream: Coq users

Topic: Mutual Global Fixpoints in SProp


view this post on Zulip D.G. Berry (Nov 13 2023 at 17:15):

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?

view this post on Zulip Gaëtan Gilbert (Nov 13 2023 at 17:19):

could be a bug, can you show an example?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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."

view this post on Zulip Gaëtan Gilbert (Nov 13 2023 at 17:51):

what Coq version?

view this post on Zulip D.G. Berry (Nov 13 2023 at 17:54):

v8.18.0

view this post on Zulip Gaëtan Gilbert (Nov 13 2023 at 18:03):

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

view this post on Zulip D.G. Berry (Nov 13 2023 at 18:05):

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 .

view this post on Zulip Gaëtan Gilbert (Nov 13 2023 at 18:15):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Nov 14 2023 at 12:44):

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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Nov 14 2023 at 13:33):

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: Jun 13 2024 at 21:01 UTC