The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

Require Export Relations Morphisms Setoid Equalities.
Require Import Arith.

Search Nat.eqb.

Lemma eqb_equiv : Equivalence (fun m n => Nat.eqb m n = true).
Proof.
  constructor; hnf; intros; rewrite Nat.eqb_eq in *; congruence.
Qed.

On 06/02/2016 12:40 PM, Soegtrop, Michael wrote:
> Dear Coq Users,
>
> sometimes I am struggling a bit with type classes. I wonder if there is an 
> elegant way to show:
>
> Lemma eqb_equiv : Equivalence (fun m n => Nat.eqb m n = true).
>
> This would follow easily from Nat.eq_equiv and Nat.eqb_eq, if I could rewrite 
> with Nat.eqb_eq under the lambda. I tried setoid_rewrite like this:
>
> 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.
>
> But I don't quite understand what to supply to get rid of the resulting error 
> message:
>
> Error: setoid rewrite failed: Unable to satisfy the following constraints:
> In environment:
> do_subrelation := Morphisms.do_subrelation : apply_subrelation
>
> ?p : "@Proper (forall _ : relation nat, Prop)
>          (@respectful (relation nat) Prop
>             (@pointwise_relation nat (forall _ : nat, Prop)
>                (@pointwise_relation nat Prop iff)) (@Basics.flip Prop Prop 
> Prop Basics.impl))
>          (@Equivalence nat)"
>
> The description in the manual is a bit too short for me to understand it.
>
> Or is there a more elegant way to prove this without a rewrite under the 
> binder?
>
> Or is there already an instance for this in the library?
>
> 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