Re: [Isarmathlib-devel] Coq

[Slawomir Kolodynski]

> Do you consider a project similar to IsarMathLib but with Coq?

I considered COQ in 2005 when I was starting the IsarMathLib project. I didn't 
like it at that time because of foundations (not set theory) and lack of 
readable proofs (I wouldn't even call those "proofs", they are verifications 
scripts). This may have changed  since then. I heard it is possible to do ZFC 
in COQ and there is a declarative proof language for COQ.
My feeling is that COQ is a good choice if you want to verify some software 
related to mathematics you formalize.


> Coq is more structured and elegant

Maybe it is true from the writer's perspective, I don't have experience with 
that. 


slawekk

 


----- Original Message -----
From: Victor Porton <address@hidden>
To: address@hidden
Cc: 
Sent: Monday, July 25, 2011 5:18 AM
Subject: [Isarmathlib-devel] Coq

Do you consider a project similar to IsarMathLib but with Coq?

What are relative advantages of Isabelle and Coq? (For me it seems that Coq is 
more structured and elegant.)

I started reading about Coq but laid it aside as there are not even cardinal 
arithmetic (based on ZFC) for Coq.

I do not want to code cardinal arithmetic myself. But if somebody will do, I 
may consider to learn Coq and code my theory (and maybe even the theory of 
posets and lattices which my theory is based on) in it. (Or I may don't.)

-- 
Victor Porton - http://portonvictor.org

_______________________________________________
Isarmathlib-devel mailing list
address@hidden
https://lists.nongnu.org/mailman/listinfo/isarmathlib-devel