The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Sorry, I forgot that I had to make another fix to your code.

When declaring the `Equivalence` instance, you have to mention which relation is being declared as an equivalence.

Otherwise, Coq makes a wrong choice -- it introduces an arbitrary new relation.

That fix was as follows:

  Context `{Ae: Equiv A} `{Equivalence A Ae}.

To be safe, I have included the entire source, checked with 8.5 beta3 on Linux.

Require Import MathClasses.interfaces.canonical_names.

Require Import MathClasses.theory.setoids.

Require Import MathClasses.implementations.peano_naturals.

Section Operators.

  Context `{Ae: Equiv A} `{Equivalence A Ae}.

  (* simple operators *)

  Class O (op: A -> A) :=

    op_proper :> Proper ((=) ==> (=)) (op).

  (* meta-operators *)

  Class MO2 (mop: (A->A) -> (A->A) -> A -> A) :=

    mop_proper :> Proper (((=) ==> (=)) ==> ((=) ==> (=)) ==> (=) ==> (=)) (mop).

  (* currued meta-operators are operators *)

  Instance MO_O `{Of: O f, Og: O g, MO2m: MO2 m}: O (m f g).

  Proof.

    apply MO2m; [apply Of | apply Og].

  Qed.

  (* TODO: Need this to use reflexivity on operators, but currently it is defined to widely, not just for operators but for any functions *)

  Instance Reflexive_ext_equiv_A: Reflexive (@ext_equiv A Ae A Ae).

  Proof.

    intros a x x' E.

    admit.

  Admitted.

  Section Test.

    (* sample operators *)

    Parameters o1 o2 o2': A->A.

    Instance O_o1: O o1. Proof. admit. Admitted.

    Instance O_o2: O o2. Proof. admit. Admitted.

    Instance O_o2': O o2'. Proof. admit. Admitted.

    (* Sample meta-operator *)

    Parameter X: (A->A) -> (A->A) -> A -> A.

    Instance X_MO2: MO2 X.  Proof.  admit. Admitted.

    (* two of operators are equal *)

    Axiom oo: o2 = o2'.

    (* this works *)

    Lemma foo:

      X o1 o2 = X o1 o2'.

    Proof.

      apply X_MO2; [reflexivity | apply oo].

    Qed.

    Lemma bar:

      X o1 o2 = X o1 o2'.

    Proof.

      rewrite oo. (* works *)

      reflexivity.

    Qed.

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Wed, Jan 6, 2016 at 12:28 AM, Vadim Zaliva <vzaliva AT cmu.edu> wrote:

On Jan 5, 2016, at 21:14 , Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

2) Fields of typeclasses are NOT automatically added to the database used for typeclass resolution. You need to mark that explicitly by replacing ":" with ":>".

For example, rewrite works in your `bar` after you change your `MO2` as follows:

Class MO2 (mop: (A->A) -> (A->A) -> A -> A) :=

    mop_proper :> Proper (((=) ==> (=)) ==> ((=) ==> (=)) ==> (=) ==> (=)) (mop).

Thanks! I just tried this and it did not work even though I can see mop_proper instance via 'Print Instances Proper’.

I am using Coq 8.4.

Sincerely,
Vadim Zaliva

--

CMU ECE PhD candidate

Mobile: +1(510)220-1060

Skype: vzaliva