[opentheory-users] Is OpenTheory usable with Coq?

[Yannick]

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.

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.

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.

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

I welcome any comments and suggestions.

Have a nice day as much as possible, and happy new year 2016.


-- 
Yannick Duchêne
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20151229/88b693cc/attachment.html>