The Coq mailing list

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

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