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: Oct 13 2024 at 01:02 UTC