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: e+coq-club AT x80.org (Emilio Jesús Gallego Arias)
To: "Soegtrop\, Michael" <michael.soegtrop AT intel.com>
Cc: "coq-club\@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, 02 Jun 2016 19:03:51 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=e+coq-club AT x80.org; spf=Neutral smtp.mailfrom=e+coq-club AT x80.org; spf=None smtp.helo=postmaster AT jiboia.ensmp.fr
Ironport-phdr: 9a23:HPrkwx+ZKUoCk/9uRHKM819IXTAuvvDOBiVQ1KB80+4cTK2v8tzYMVDF4r011RmSDdSdtqMP0rKI+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuSt+U0pX8jrjss7ToICx2xxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cYk7sb+sVBSaT3ebgjBfwdVWx+cjN92Mq+/yLEQAST/HwEZiFetxtDAwHI6FuyCpLwuSvzu+47wy6XMtHsSqgcWDK+4qMtQxjt3nQpLTk8pWyUgctpyalfvRiJt0wnhYnOb8nVGf9/eqLaNfEXXvhaFulYUyhMDYT0RpEOBvFAbrUQlJX0u1Zb9Uj2PgKrHu66j2YQ3nI=
Organization: X80 Heavy Industries

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

[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?, Tej Chajed, 06/02/2016
    - Re: [Coq-Club] Elegant way to show Equivalence (fun m n => Nat.eqb m n = true) from standard library lemmas?, Arnaud Spiwack, 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?, 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?, Abhishek Anand, 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?, Soegtrop, Michael, 06/03/2016
        
        Re: [Coq-Club] Elegant way to show Equivalence (fun m n => Nat.eqb m n = true) from standard library lemmas?, Abhishek Anand, 06/03/2016
        
        [Coq-Club] Elegant way to show Equivalence (fun m n => Nat.eqb m n = true) from standard library lemmas?, Soegtrop, Michael, 06/03/2016
- 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