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?)
if there is no decreasing argument how does it reduce?
It should always reduce when not under binders
(My actual desired example here is a fixpoint combinator in the TemplateMonad of TemplateCoq)
The syntactical guard is that the recursive argument must be a constructor for the fixpoint to unfold.
"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.
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.
IIRC generalizing this to non-inductive types was attempted but then it messes with other invariants of the reduction.
You don't lose anything by adding a dummy unit
argument to your fixpoint, in any case.
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.
It's not worth making the other parts more complex when there is such a trivial workaround.
Last updated: Dec 07 2023 at 14:02 UTC