Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Principle of definition

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Principle of definition


chronological Thread 
  • 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.




Archive powered by MhonArc 2.6.16.

Top of Page