The Coq mailing list

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

Hi Serge,

 A nice way to solve your problem should be the following one:

 1) Specify min (for instance by a predicate) :

 Inductive is_min (m z z':Z) : Prop :=
  is_min_intro : m <= z -> m <= z' ->
     (forall x, x <= z -> x <= z' -> x <= m) ->
  is_min m z z'.

 2) Then prove some properties (like unicity of m wrt z and z',
 and symmetry wrt z and z', etc .)

 3) Consider some function Min such that
   forall z z', is_min (Min z z') z z'.

  It should be easy to get the proprty wou want (commutativity of Min)

 4) Using ZArith, prove (forall z z', is_min (Zmin z z') z z').
 Etc ...

 5) All steps 1-3 are independent of Z.
   You can easily generalize your proof by :
   a)  Considering a signature associed with total orders with a comparison
    function (see for instance DEC_ORDER in
http://www.labri.fr/Perso/~casteran/CoqArt/modules/SRC/dict.v
)
   b) Considering an extended signature with is_min and Min, and
   the abstract properties seen above.

   c) Copy the preceeding proofs in a functor from the initial signature
     to the extended one

   d) Then build an implementation of DEC_ORDER upon Z.



I think it should be a nice example for a tutorial on
using the module system.

Have a nice week-end,
Pierre


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

> I am trying to prove the the following trivial goal. I don't reach it,
> can you show me how to make?
>
> Goal forall n m:Z, Zmin n m = Zmin m n.
>
> Sincerely,
> --
> 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.