The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

When facing this sort of problems, unless you have a single instance and a quick-and-dirty method will suffice. It is often worth it using a combinator which encapsulates the logics (here applying = true to the body of a boolean relation) and on which you can prove properties.

Below a more verbose proof than the above responses, with reusable components:

Require Import Coq.Classes.RelationClasses.
Require Import Coq.Classes.Morphisms.
Require Import Coq.Arith.Arith.

(* Generic lemma, probably has a place in the standard library *)
Instance equivalence_extensional A
  : Proper (@relation_equivalence A ==> Basics.impl) Equivalence.
Proof.
  intros r s eq__rs [r__r s__r t__r]. cbn in eq__rs.
  split.
  all: hnf in *; intros **.
  all: rewrite <- eq__rs in *; eauto.
Qed.

Definition BRel {A} (r:A->A->bool) : A -> A -> Prop :=
  fun x y => r x y = true.

Lemma brel_nat_eqb_eq : relation_equivalence (BRel Nat.eqb) eq.
Proof.
  exact Nat.eqb_eq.
Qed.

Instance nat_eqb_equivalence : Equivalence (BRel Nat.eqb).
Proof.
  rewrite brel_nat_eqb_eq.
  typeclasses eauto.
Qed.

​

On 2 June 2016 at 19:16, Tej Chajed <tchajed AT mit.edu> wrote:

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