Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] how to prove and evaluate new function definition with this axioms

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] how to prove and evaluate new function definition with this axioms


Chronological Thread 
  • From: Mandy Martino <tesleft AT hotmail.com>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] how to prove and evaluate new function definition with this axioms
  • Date: Sun, 7 Feb 2016 08:00:04 +0000
  • Accept-language: en-US, zh-HK
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=tesleft AT hotmail.com; spf=Pass smtp.mailfrom=tesleft AT hotmail.com; spf=None smtp.helo=postmaster AT COL004-OMC4S1.hotmail.com
  • Ironport-phdr: 9a23:w/8LeRJe24I4K6h03dmcpTZWNBhigK39O0sv0rFitYgULPzxwZ3uMQTl6Ol3ixeRBMOAu60C0bad6f+8EUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ35vxjbz5ocKPKyxzxxODIppKZC2sqgvQssREyaBDEY0WjiXzn31TZu5NznlpL1/A1zz158O34YIxu38I46FppIZ8VvCwdKMhCLdcET4OMmYv5cStuwOJBV+E4WJZWWELmDJJBRLE5Vf0RMGinDH9s79Y0S+WLIXTRKooWDKlp/N3RQTshSkbHz4+7GTei8g2h6Ve9kHy7ydjypLZNdnGfMF1ebnQKIsX

Hi ,


Is it possible to apply ring homomorphism on list to apply to axioms to auto generate recursive function or fixed point definition in coq?


Regards,

Martin 


From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Mandy Martino <tesleft AT hotmail.com>
Sent: Sunday, February 7, 2016 14:46
To: coq-club AT inria.fr
Subject: [Coq-Club] how to prove and evaluate new function definition with this axioms
 

Hi ,


Require Import Arith.
Parameter G : Type.
Axiom reflexive : forall x y z:G, x <= x.
Axiom symmetric : forall x y z:G, x = y <= y = x.
Axiom transitive : forall x y z:G, (z = y) * z <= (z = x) * x.

Regards,

Martin 

Archive powered by MHonArc 2.6.18.

Top of Page