Coq support?

[brando90]

Is it planned to have Coq supported too?

[tlringer]

I'm thinking about chipping away at a few of these in Coq later today, if anyone wants to do a push from the Coq community. Would be good to email coq-club.

[brando90]

I might be interested. What would be a list/plan of what would be needed to do this?

…

On Feb 6, 2022, at 12:25 PM, Talia Ringer ***@***.***> wrote: I'm thinking about chipping away at a few of these in Coq later today, if anyone wants to do a push from the Coq community. Would be good to email coq-club. — Reply to this email directly, view it on GitHub <#66 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAOE6LWNUP26BT5W6CNMEWTUZ24K7ANCNFSM5NTHE4GA>. Triage notifications on the go with GitHub Mobile for iOS <https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675> or Android <https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub>. You are receiving this because you authored the thread.

[spolu]

It would be awesome to have Coq support (even if only partial to start with).

In our experience it takes ~15-20mn to students to formalize a statement and ~5mn to review one. With a small group, covering the 488 statements shouldn't take that long!

[brando90]

Cool! Once I have more open cycles I will see how to organize formalizing it. Perhaps I can share it in the Coq discuss and have people help me do it! :)

…

On Feb 8, 2022, at 2:04 AM, Stanislas Polu ***@***.***> wrote: It would be awesome to have Coq support (even if only partial to start with). In our experience it takes ~15-20mn to students to formalize a statement. With a small group, covering the 488 statements shouldn't take that long! — Reply to this email directly, view it on GitHub <#66 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAOE6LUHNI4XRIHKUF7HWPLU2DFBTANCNFSM5NTHE4GA>. Triage notifications on the go with GitHub Mobile for iOS <https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675> or Android <https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub>. You are receiving this because you authored the thread.

[brando90]

Perhaps we can start discussing it. Say I translate the statmenets from Lean to Coq. Then I'd need to reprove them in Coq, right? Perhaps it's trivial since lean and coq are both depedently typed? Or how would I proceed? Perhaps I am assuming translating the statement itself is trivial when it's not...?

…

On Feb 8, 2022, at 9:23 AM, Brando Miranda ***@***.***> wrote: Cool! Once I have more open cycles I will see how to organize formalizing it. Perhaps I can share it in the Coq discuss and have people help me do it! :) > On Feb 8, 2022, at 2:04 AM, Stanislas Polu ***@***.*** ***@***.***>> wrote: > > > It would be awesome to have Coq support (even if only partial to start with). > > In our experience it takes ~15-20mn to students to formalize a statement. With a small group, covering the 488 statements shouldn't take that long! > > — > Reply to this email directly, view it on GitHub <#66 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAOE6LUHNI4XRIHKUF7HWPLU2DFBTANCNFSM5NTHE4GA>. > Triage notifications on the go with GitHub Mobile for iOS <https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675> or Android <https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub>. > You are receiving this because you authored the thread. >

[tlringer]

I was slow to get to this but still plan on it. Yes, I think translating the statement should be fairly simple since Lean and Coq are so similar, and the serious ways they differ are unlikely to show up much in these proofs. Proofs in Coq might be similar to Lean or might differ a bit, it depends on what the proof is about and what automation is present in each proof assistant.

If you submit a PR for any of them, feel free to list me and I'll take a look.

[brando90]

plan to post a discussion here perhaps later? https://coq.zulipchat.com/#narrow/stream/237655-Miscellaneous

[tlringer]

Sure, if you post there I'll join in. I'm also happy to email coq-club to try to organize more of an effort here.

[tlringer]

@spolu, not sure on the permissions, but is the best way to contribute to fork? Or can we have edit access for a Coq branch?

[tlringer]

Forked for now: https://github.com/tlringer/miniF2F/tree/coq

@brando90 happy to develop in my fork; added you. Happy to add any other Coq proof engineers who get started on this, too, once we spread the word.

[tlringer]

So, the theorems are easy to state, but many proofs will be a huge pain in the ass because of Coq's real number library, which is terrible. For example, I took a shot at the first one, and it's maybe the ugliest proof I've ever written: tlringer@3985d96

(@SkySkimmer helped me improve this a lot, since he seems to better understand how lra works: tlringer@4dced50)

[spolu]

@tlringer you can fork the repo and create a pull-request 👍

@brando90 most statements in minif2f don't have a proof. I think this is fine. Obviously there is a risk that the statement contains an error (though that risk still exists with a proof).

Anyway statements only are accepted, proofs are welcome.

[spolu]

Let us know how we can help!

[tlringer]

Good to know the theorems are enough. Sounds like any math library like this in Coq would use SSReflect, so I need to figure out whether that would change the theorem statements or just their proofs before continuing.

…

On Wed, Feb 9, 2022, 1:47 AM Stanislas Polu ***@***.***> wrote: Let us know how we can help! — Reply to this email directly, view it on GitHub <#66 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ACLFD77GBIGHQQZVXKPVB43U2ILYHANCNFSM5NTHE4GA> . Triage notifications on the go with GitHub Mobile for iOS <https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675> or Android <https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub>. You are receiving this because you were mentioned.Message ID: ***@***.***>

[tlringer]

Indeed, it will change the theorems too, so getting some SSReflect people on board is a good idea.

…

On Wed, Feb 9, 2022, 7:32 AM Talia Ringer ***@***.***> wrote: Good to know the theorems are enough. Sounds like any math library like this in Coq would use SSReflect, so I need to figure out whether that would change the theorem statements or just their proofs before continuing. On Wed, Feb 9, 2022, 1:47 AM Stanislas Polu ***@***.***> wrote: > Let us know how we can help! > > — > Reply to this email directly, view it on GitHub > <#66 (comment)>, > or unsubscribe > <https://github.com/notifications/unsubscribe-auth/ACLFD77GBIGHQQZVXKPVB43U2ILYHANCNFSM5NTHE4GA> > . > Triage notifications on the go with GitHub Mobile for iOS > <https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675> > or Android > <https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub>. > > You are receiving this because you were mentioned.Message ID: > ***@***.***> >