Interfacing with Coq and PVS

Stream: new members

[Haskell]

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.

[Bryan Gin-ge Chen]

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

[Haskell]

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.

[Bryan Gin-ge Chen]

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.

[Haskell]

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.

[Mario Carneiro]

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

[Haskell]

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

[Bryan Gin-ge Chen]

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.

[Mario Carneiro]

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

[Mario Carneiro]

especially if you want complete faithfulness