coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Pierre Casteran <pierre.casteran AT labri.fr>
- To: coq-club AT pauillac.inria.fr
- Subject: [Coq-Club] Principle of definition
- Date: Thu, 7 Jul 2005 09:53:18 +0200
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hi, all.
I'm working in some classical framework, and am looking for a correct
way to make definitions.
For instance, let D be some Set, ordered by some relation <=.
I define the following specification :
Definition zero_spec (z:D) := forall d, z <= d.
I can prove (using classical arguments) :
Lemma zero_exists : exists z, zero_spec z.
and
Lemma zero_unicity : forall z z', zero_spec z -> zero_spec z' -> z = z'.
If I want to consider a constant zero, it can do it using some declarations:
Parameter zero : D.
Axiom zero_ok : zero_spec zero.
Theorem zero_eq : forall z, zero_spec z -> z=zero.
<trivial proof>.
Is there a better way to proceed ? Because of classical logic,
I didn't use the sig type for zero_exists (which would have allowed me to
extract a witness).
Pierre
--
Pierre Casteran
http://www.labri.fr/Perso/~casteran/
(+33) 540006931
----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.
- [Coq-Club] Principle of definition, Pierre Casteran
- Re: [Coq-Club] Principle of definition,
Pierre Casteran
- Re: [Coq-Club] Principle of definition, Hugo Herbelin
- Re: [Coq-Club] Principle of definition,
Pierre Casteran
Archive powered by MhonArc 2.6.16.