coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] Elegant way to show Equivalence (fun m n => Nat.eqb m n = true) from standard library lemmas?

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <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?
Date: Thu, 2 Jun 2016 17:31:28 +0000
Accept-language: de-DE, en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga04.intel.com
Ironport-phdr: 9a23:9IQmhxSQznp6qXDBZT/9Stq0Htpsv+yvbD5Q0YIujvd0So/mwa64YxeN2/xhgRfzUJnB7Loc0qyN4/GmBD1LuM7Q+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpq8yVPlQD3WLsKZpJbzyI7izp/vEMhoVjLqtjgjDomVBvP9ps+GVzOFiIlAz97MrjtLRq8iBXpu5zv5UYCfayLOwESukSBzM/dmsx+cfDtB/ZTALJ6GFWGjEdlQMNCAzY5jn7WI3wu230rLwu9jOdOJi8drc5Vii46L8vADrpgycOOjpzuDXSi8dwha9f5gmmqhNj2YnMSICTKPd6OKjaeIVJFiJ6Qs9NWnkZUcuHZIwVAr9ZMA==

Dear Jonathan, Tej,

yes, by breaking up the Equivalence into its components, it is fairly easy.

I was more looking for a method which avoids the constructor tactic and shows
this in a more direct way. Some of the structures I am looking into a fairly
complicated, and this breaking up method doesn't work that easily then.

Say I have some type class structure T for a relation R, I know that relation
R and S are equivalent (forall x y, R x y <-> S x y) and I want to derive
structure T for S. Is there a generic way to do this for any structure T?

Thanks & best regards,

Michael
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

Re: [Coq-Club] Elegant way to show Equivalence (fun m n => Nat.eqb m n = true) from standard library lemmas?, (continued)
- Re: [Coq-Club] Elegant way to show Equivalence (fun m n => Nat.eqb m n = true) from standard library lemmas?, Jonathan Leivent, 06/02/2016
  - RE: [Coq-Club] Elegant way to show Equivalence (fun m n => Nat.eqb m n = true) from standard library lemmas?, Soegtrop, Michael, 06/02/2016
    - Re: [Coq-Club] Elegant way to show Equivalence (fun m n => Nat.eqb m n = true) from standard library lemmas?, Emilio Jesús Gallego Arias, 06/02/2016
      - RE: [Coq-Club] Elegant way to show Equivalence (fun m n => Nat.eqb m n = true) from standard library lemmas?, Soegtrop, Michael, 06/03/2016