The Coq mailing list

[Tej Chajed <tchajed AT mit.edu>]

You can also prove it directly fairly easily, still relying on Nat.eqb_eq. I think this is quite similar in spirit to Emilio's ssreflect proof.

Lemma eqb_equiv : Equivalence (fun m n => Nat.eqb m n = true).

Proof.

  constructor; repeat intro;

    rewrite Nat.eqb_eq in *;

    congruence.

Qed.

On Thu, Jun 2, 2016 at 1:03 PM, Emilio Jesús Gallego Arias <e+coq-club AT x80.org> wrote:

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