The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

On Dec 30, 2015, at 23:06 , Gregory Malecha <gmalecha AT gmail.com> wrote:

Your best bet to get this to work is remove the two [O] instances in the definition of X.

I am trying to build some theory using type classes and could use little more advice. I wrote the following:

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}.

  (* 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.

  Qed.

  Section Test.

    (* sample operators *)

    Parameters o1 o2 o2': A->A.

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

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

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

    (* Sample meta-operator *)

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

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

    (* 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.

    (* TODO: this does not work *)

    Lemma bar:

      X o1 o2 = X o1 o2'.

    Proof.

      rewrite oo.

    Qed.

  End Test.

End Operators.

Basically type class ‘O’ denotes an “operator” which in my world is a function along with proper morphism wrt. `equiv` relation.

Class ‘MO2’ denotes binary meta-operator. 

Now I am facing two problems:

1. I need to have reflexivity on operators. My `Reflexive_ext_equiv_A` instance is too generic and could not be proven as stated. It needs to be narrowed to instances of ‘O’ only. How one can do that?

2. The second problem is that ‘rewrite’ still does not work. I can apply X_MO2 manually, but it would be nice to be able to use ‘setoid_rewrite’ tactics as shown in ‘bar’. Somehow type class resolver could not find Proper instances required. Perhaps it needs some Hints?

 

Any comments are greatly appreciated.

Sincerely,
Vadim Zaliva

--

CMU ECE PhD candidate

Mobile: +1(510)220-1060

Skype: vzaliva