Stream: Coq users

Topic: Lean vs Coq SE question


view this post on Zulip Karl Palmskog (Feb 08 2022 at 19:24):

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

view this post on Zulip Karl Palmskog (Feb 09 2022 at 11:31):

https://proofassistants.stackexchange.com/questions/153/what-are-the-main-differences-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.

view this post on Zulip Meven Lennon-Bertrand (Feb 09 2022 at 13:15):

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

view this post on Zulip Karl Palmskog (Feb 09 2022 at 13:30):

@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.

view this post on Zulip Gaëtan Gilbert (Feb 09 2022 at 13:32):

I don't think equations compiles to recursors
what would be the point?

view this post on Zulip Meven Lennon-Bertrand (Feb 09 2022 at 13:33):

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

view this post on Zulip Meven Lennon-Bertrand (Feb 09 2022 at 13:34):

@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

view this post on Zulip Meven Lennon-Bertrand (Feb 09 2022 at 13:35):

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

view this post on Zulip Théo Winterhalter (Feb 09 2022 at 13:35):

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

view this post on Zulip Meven Lennon-Bertrand (Feb 09 2022 at 13:36):

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

view this post on Zulip Yannick Forster (Feb 09 2022 at 13:39):

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

view this post on Zulip Karl Palmskog (Feb 09 2022 at 13:43):

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]

view this post on Zulip Yannick Forster (Feb 09 2022 at 13:50):

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

view this post on Zulip Yannick Forster (Feb 09 2022 at 13:51):

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