The Coq mailing list

[David Pichardie <david.pichardie AT irisa.fr>]

Hi,

To complete the other propositions, I recommend to use a generic proof method for min (and adaptable for max) :

Lemma case_Zmin : forall (P:Z->Type) x y,
(x<=y -> P x) -> (y<=x -> P y )-> P (Zmin x y).
Proof.
unfold Zmin, Zle; intros P x y.
generalize (Zcompare_antisym x y).
destruct (x ?= y); intros.
apply X; discriminate.
apply X; discriminate.
apply X0.
rewrite <- H; discriminate.
Qed.

Lemma Zmin_comm : forall n m, Zmin n m = Zmin m n.
Proof.
intros; repeat (apply case_Zmin; intros); omega.
Qed.

With such a proof principle the script " intros; repeat (apply case_Zmin; intros); omega." is often very powerful.

Here is an other example :

Lemma Zmin_glb : forall n m p, p <= n -> p <= m -> p <= Zmin n m.
Proof.
intros; repeat (apply case_Zmin; intros); omega.
Qed.

Hope this helps,

David.



Le 20 mai 05, à 19:13, Serge Leblanc a écrit :

> 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
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
David Pichardie
http://www.irisa.fr/lande/pichardie/index.en.html