The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Selon Serge Leblanc 
<serge.leblanc AT wanadoo.fr>:

> I thank you for your very instructive answers which I study with
> attention.
> Is it possible to add in the Coq standard library the lemma Zmin_comm?

Hello Serge,

  I think that it should be better to develop (in the module framework)
a theory of ordered sets (with a compare function) and prove not only
the commutativity of min but also associativity, the same for max, ...

  If one develops proofs for all the interesting properties of Zmin
 the same work will have to be done for min (on nat, on lexicographic
  products, ...)

Cheers,

Pierre

>
> Mi dankas vin por viaj edukadaj solvoj kiuj mi atente studas.
> Ĉu oni eble aldonas la Zmin_comm theoremon en norma Coq theoremaro ?
>
> Amike,
> In a friendly way,
> --
> Serge Leblanc 
> <serge.leblanc AT wanadoo.fr>
>  GnuPG id: 1024D/73791C2B 2002-09-30
> Primary key fingerprint: 8E0C 0D6D E026 A278 9278  BF4F 1A93 D552 7379 1C2B
>


-- 
Pierre Casteran

http://www.labri.fr/Perso/~casteran/

(+33) 540006931

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.