Stream: Coq devs & plugin devs

Topic: Guard Checker

Jason Gross (Oct 21 2022 at 13:09):

Why does Fixpoint with Unset Guard Checking still require an inductive type and a decreasing argument? That is, why can't I write Unset Guard Checking. Fixpoint Fix {A} (f : (unit -> A) -> A) := f (fun 'tt => Fix f).? (Is there a strong limitation here, or should I just open a feature request?)

Gaëtan Gilbert (Oct 21 2022 at 13:48):

if there is no decreasing argument how does it reduce?

Jason Gross (Oct 21 2022 at 14:27):

It should always reduce when not under binders

Jason Gross (Oct 21 2022 at 14:28):

(My actual desired example here is a fixpoint combinator in the TemplateMonad of TemplateCoq)

Théo Winterhalter (Oct 21 2022 at 14:36):

The syntactical guard is that the recursive argument must be a constructor for the fixpoint to unfold.

Guillaume Melquiond (Oct 21 2022 at 14:37):

"not under binders" is meaningless in the context of Coq. First, terms need to be normalizable. Second, there is always a binder lying around, as there is hardly any theorem that does not start with a forall quantifier.

Guillaume Melquiond (Oct 21 2022 at 14:40):

I mean, if you do not reduce under binders, you could not even typecheck (fun f => eq_refl) : forall f, Fix f = f (fun 'tt => Fix f) in the first place.

Pierre-Marie Pédrot (Oct 21 2022 at 21:49):

IIRC generalizing this to non-inductive types was attempted but then it messes with other invariants of the reduction.

Pierre-Marie Pédrot (Oct 21 2022 at 21:50):

You don't lose anything by adding a dummy unit argument to your fixpoint, in any case.

Pierre-Marie Pédrot (Oct 21 2022 at 21:52):

i.e. just write

Unset Guard Checking.
Fixpoint Fix0 {A} (f : (unit -> A) -> A) (u : unit) {struct u} := f (fun 'tt => Fix0 f tt).
Definition Fix {A} f := @Fix0 A f tt.

Pierre-Marie Pédrot (Oct 21 2022 at 21:52):

It's not worth making the other parts more complex when there is such a trivial workaround.

Last updated: Feb 02 2023 at 13:03 UTC