Jason Gross (Oct 21 2022 at 13:09): 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.
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