Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Needed assistance in Coq proof for kleene algebra axioms

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Needed assistance in Coq proof for kleene algebra axioms


chronological Thread 
  • From: David Pereira <dpereira AT liacc.up.pt>
  • To: prateek agarwal <prat0318 AT gmail.com>
  • Cc: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] Needed assistance in Coq proof for kleene algebra axioms
  • Date: Tue, 31 Mar 2009 17:10:07 +0100
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Dear Prateek,

The code described in the paper you are using, "KAT and PHL in Coq", puslished in ComSIS Volume 5, Number 2, December 2008, is part of a bigger project, and it will be publicly available when that project is completed.

Best regards,
   David Pereira


On 2009/03/31, at 09:52, prateek agarwal wrote:

Hi,
       If anyone has the coq proofs for the axioms of Kleene algebra
and Kleene algebra Tests, I shall be grateful if you could please
provide them to me. Or, I am having a short coq code written for their
proofs, but an error in compilation occurs in lines where ~ and #
symbols are used. I am a newbie in COQ, can anyone please sort out the
error.

<snippet from ka.v>...
Record boolean_theory : Prop := mk_bool {
ba_ax_1 : forall x, x * ~x = 0 ;
...
Error : The term "0" has the type "nat" while it is expected to have type "Set".

--
Prateek Agarwal
Senior Undergraduate Student
Dept. of Computer Science And Engg.
Indian Institute of Technology, Kharagpur

"Half the people you know are below average."
<ka.v>





Archive powered by MhonArc 2.6.16.

Top of Page