The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

To make your rewrite succeed, you need to show that Equivalence respects pointwise iff between relations, which is essentially what the error message suggests.

I merely proved the missing constraint in the error message (after generalizing nat to A), and your rewrite then succeeds:

Global Instance pr {A} : Proper

        (pointwise_relation A (pointwise_relation A iff) ==> Basics.flip Basics.impl)

        Equivalence.

Proof.

  intros ? ? ? ?.

  unfold pointwise_relation in H.

  constructor; intros ?; intros; rewrite H in *; eauto with relations.

  eapply transitivity; eauto.

Qed.

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

Proof.

  setoid_rewrite Nat.eqb_eq.

 

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Thu, Jun 2, 2016 at 1:17 PM, Soegtrop, Michael <michael.soegtrop AT intel.com> wrote:

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