Skip to Content.
Sympa Menu

coq-club - [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

[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: [Coq-Club] how to prove and evaluate new function definition with this axioms
  • Date: Sun, 7 Feb 2016 06:46:53 +0000
  • Accept-language: en-US, zh-HK
  • Authentication-results: mail2-smtp-roc.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-OMC2S13.hotmail.com
  • Ironport-phdr: 9a23:lHxloxZdniSybU9ZG4NxOKH/LSx+4OfEezUN459isYplN5qZpcq6bnLW6fgltlLVR4KTs6sC0LqJ9fq8EjZdvN6oizMrTt9lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUiv2OQc9HOnpAIma153xjLDtvcePKF8V2XKUWvBbElaflU3prM4YgI9veO4a6yDihT92QdlQ3n5iPlmJnhzxtY+a9Z9n9DlM6bp6r5YTGfayQ6NtB7dfFXEtN30/zMztrxjKCwWVrDNIWWIP1xFMHgLt7RfgX563vDGs5cRn3yzPGMTwQaF8fD2486ZtT1e8lCocMzM37EnXjdB1haNf5hmmokoskMbvfIiJOa8mLevmdtQASD8ZUw==

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