OK, who's going to set up the big one and ask: "What is the difference between Coq and Lean?"

Is there really anything preventing a Coq user from using only "recursor functions that are inherently terminating"? I thought this was one of the points of Equations.

Well, no, but it is not something the type system can enforce for you.

@Meven Lennon-Bertrand but you could check it using MetaCoq or a plugin, right? Just get the terms out and flag up if there is a `fix`

, etc.

I don't think equations compiles to recursors

what would be the point?

Well, it’s a bit more complex than this, because recursors are still implemented using `fix`

. But yeah you could implement your own guard condition (encoding the fact that the only fix allowed are exactly recursors) as a plugin/using MetaCoq and run that on your code

@Gaëtan Gilbert I can see the point of relying on a stricter guard condition than the one of Coq which is… muddy, to say the least

And "only use recursors" is the most strict guard I can think of :)

First we'd need the right recursors for all types.

I think @Yannick Forster worked on this, not sure exactly how far he got but pretty far from what I gathered

It would be possible to implement a guard condition in MetaCoq which checks that fix is only used internally to constants like `nat_rect`

and so on. I worked a little with @Lennard Gäher on re-implementing Coq's current guard condition. That could serve as a potential stepping stone for a guard checker allowing just recursors

I may be misunderstanding or missing something but what's the difference between limiting to recursors and "compil[ing] everything down to eliminators for inductive types, equality and accessibility"? [quote from Equations README]

It depends a bit on what you call a recursor. Equations does not insert `Acc_rect`

, but instead constructs term ultimately relying on `Coq.Init.Wf.Fix`

. Which is, at least syntactically, not a recursor

But conceptually, Equations compiles everything down to one single Fixpoint if `by wf`

is used. So yes, we can use it to argue that one doesn't have to trust Coq's guard checker if using Equations

Last updated: Jan 27 2023 at 01:03 UTC