[opentheory-users] Is OpenTheory usable with Coq?

[Ramana Kumar]

On 29 December 2015 at 08:41, Yannick <yannick_duchene at yahoo.fr> wrote:

> Hi people out there, I'm new here.
>
> May be my mind is buggy, I was sure to recall there was an OpenTheory
> reader/writer for Coq. Now looking at
> http://www.gilith.com/research/opentheory/ , I can't see it.
>

You might be thinking of Holide. There is a link at
http://dedukti.gforge.inria.fr/, but it seems to be 404 at the moment. Ask
the authors?

Another possibility is https://www.lri.fr/~keller/Recherche/hollightcoq.html,
but I think it's only one-way (and not the direction you need).


>
> I know there is a reader for Isabell/HOL. Unfortunately, I'm rather
> looking for a proof environment with a writer, as I bother about saving
> proofs.
>

I am interested in producing a writer for Isabelle/HOL eventually (some
time over the next year hopefully). It could be good to combine efforts.


>
> If this is useful, I may draw the picture. I'm learning to effectively use
> ATS, a language with dependent types, linear types, inductive definitions
> and proofs. It's a very nice language, however and for good reasons, not
> suited to prove properties of as an example, inductive definitions (it
> mainly target programming issues, that is, ensuring pre/post conditions,
> resources tracking and the likes). I'm planning to export inductive
> definition using the abstract syntax tree output ATS provides, then prove
> properties of these inductive definitions, outside of ATS and save these
> proofs in a standard format (luckily, OpenTheory exists). I had some short
> past experience with Isabelle/HOL and Coq. I like Isabelle/HOL for being
> HOL, but don't really like the language and even less like the editor. So I
> tough about Coq and CoqIDE, which seems more usable to me, as much the
> language and the IDE, although I don't really know its logic, seemingly a
> superset of HOL. Unfortunately, it does not seems to support OpenTheory. So
> may be HOL Light, but I never used it, and am afraid of writing proofs in a
> TTy like interface.
>

Writing proofs in HOL4 or HOL Light is not as frightening as you might
think :)


>
> That's about the picture. If possible, I would prefer to use Coq, just
> only if it can writes OpenTheory files.
>

If you work in a restricted subset of Coq, it may be possible to create a
translation from Coq's proof terms to OpenTheory format. It might be worth
looking into that, if you're interested. Let me know.


>
> I welcome any comments and suggestions.
>
> Have a nice day as much as possible, and happy new year 2016.
>
>
> --
> Yannick Duchêne
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20151229/0aea2376/attachment.html>