The Coq mailing list

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

Dear Abishek,

 

perfect, thanks! So I just have to prove this for all structures I am interested in to solves my issues.

 

Best regards,

 

Michael

 

From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of Abhishek Anand
Sent: Thursday, June 2, 2016 7:29 PM
To: coq-club <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?

 

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/

 

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