coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

[Coq-Club] how to prove and evaluate new function definition with this axioms, Mandy Martino, 02/07/2016
- Re: [Coq-Club] how to prove and evaluate new function definition with this axioms, Mandy Martino, 02/07/2016
- Re: [Coq-Club] how to prove and evaluate new function definition with this axioms, Pierre Casteran, 02/07/2016
  - Re: [Coq-Club] how to prove and evaluate new function definition with this axioms, Mandy Martino, 02/09/2016
    - Re: [Coq-Club] how to prove and evaluate new function definition with this axioms, John Wiegley, 02/09/2016