The Coq mailing list

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

Dear Arnaud,

 

ahh, that’s what I call haute couture! Many thanks!

 

Best regards,

 

Michael

 

From: arnaud.spiwack AT gmail.com [mailto:arnaud.spiwack AT gmail.com] On Behalf Of Arnaud Spiwack
Sent: Thursday, June 2, 2016 7:44 PM
To: Coq Club <coq-club AT inria.fr>
Cc: Soegtrop, Michael <michael.soegtrop AT intel.com>
Subject: Re: [Coq-Club] Elegant way to show Equivalence (fun m n => Nat.eqb m n = true) from standard library lemmas?

 

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

 

 

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