The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Emilio,

thanks for your suggestion! I considered moving to ssreflect several times, 
maybe I should.

My larger goal is to create order structures (like TotalOrder) from user 
supplied types and boolean comparison operators in a reasonably efficient 
way. Using Nat.eqb was just an example. I am interested in elegant proof 
techniques for such kind of goals, but not so much in this specific goal.

Best regards,

Michael

-----Original Message-----
From: Emilio Jesús Gallego Arias 
[mailto:e+coq-club AT x80.org]
 
Sent: Thursday, June 2, 2016 7:04 PM
To: Soegtrop, Michael 
<michael.soegtrop AT intel.com>
Cc: 
coq-club AT inria.fr
Subject: Re: [Coq-Club] Elegant way to show Equivalence (fun m n => Nat.eqb m 
n = true) from standard library lemmas?

Dear Michael,

"Soegtrop, Michael" 
<michael.soegtrop AT intel.com>
 writes:

> Require Export Relations Morphisms Setoid Equalities.
> Require Import Arith.
> Lemma eqb_equiv : Equivalence (fun m n => Nat.eqb m n = true).
> Proof.
>   setoid_rewrite Nat.eqb_eq.

I am not sure what you intend to prove, but here's a different proof your 
result (using ssreflect's == equality instead of Nat.eqb).

From mathcomp
Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq.
Require Export Relations Morphisms Setoid Equalities.

Lemma eqb_equiv : Equivalence (fun m n : nat => m == n).
Proof.
constructor.
- exact: eqxx.
- by move=> x y; rewrite eq_sym.
- by move=> x y z /eqP->.
Qed.

Best,
Emilio
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928