Zulip Chat Archive

Stream: new members

Topic: Interfacing with Coq and PVS


view this post on Zulip Haskell (Dec 29 2020 at 21:07):

Hi, I've been told that the Lean API might help me interface with other theorem provers, is this true? If so, any pointers would be appreciated. I'm having a hard time googling this.

I looked at this https://leanprover-community.github.io/mathlib_docs/
...but that'll probably come in later, if at all.

view this post on Zulip Bryan Gin-ge Chen (Dec 29 2020 at 21:08):

Can you say a bit more about what you're trying to do?

view this post on Zulip Haskell (Dec 29 2020 at 21:13):

The hope is for students to prove various parts in Coq, PVS or z3 and have it come together. Lean was suggested to me as being able to possibly integrate such.

I did find this (PDF link): https://leanprover.github.io/talks/from_z3_to_lean.pdf but that's also a little light on details for me.

view this post on Zulip Bryan Gin-ge Chen (Dec 29 2020 at 21:24):

I started writing a response about various ways to communicate with Lean 3, but I realized that @Jason Rute wrote a much more detailed one in this thread. As far as I know not too much has changed since then, but we do now have some documentation on the server protocol which might be useful.

view this post on Zulip Haskell (Dec 29 2020 at 21:30):

Thanks Bryan! I looked through your links; they might help for wrappers. But I think this means there aren't standard "transpilers" to lean from coq proof objects or pvs prf files that I could use?

I'm asking because if it's more than a couple of days of work, it might be better to table this idea.

view this post on Zulip Mario Carneiro (Dec 29 2020 at 21:32):

no, the translation story between those provers is currently pretty bad

view this post on Zulip Haskell (Dec 29 2020 at 21:33):

Thanks Mario and Bryan, that saves me a lot of digging!

view this post on Zulip Bryan Gin-ge Chen (Dec 29 2020 at 21:33):

That's right, there isn't anything like that at all as far as I know.

Note that even if there were such a thing, there are still a lot of obstacles in the way of any kind of useful translation. See this thread for some discussion.

view this post on Zulip Mario Carneiro (Dec 29 2020 at 21:33):

It's probably at the "bachelor's thesis" level of difficulty, not impossible but at least a few weeks of work

view this post on Zulip Mario Carneiro (Dec 29 2020 at 21:34):

especially if you want complete faithfulness


Last updated: May 08 2021 at 20:11 UTC