The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

On Dec 29, 2015, at 19:05 , Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

I typically combine the dependent arguments with their indices, and pick an appropriate equality for the combination.

Thanks! I have another related question about Proper, this time with Type classes. In this case

I am working with functions, which are declared to be instances of a type class ‘O’. In example

below this class have just one field, f_proper, but may have more fields. I understand the source

of the problem: I try to rewrite o2, but there is dependent argument O_o2 which needs to be replaced

as well. What would be a good way to deal with this?

Here is a complete example:

Require Import MathClasses.interfaces.canonical_names.

Require Import MathClasses.theory.setoids.

Require Import MathClasses.implementations.peano_naturals.

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

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

Definition o1 := plus 1.

Definition o2 := plus 2.

Definition o2' := compose (plus 1) (plus 1).

Instance O_o1: O o1. Admitted.

Instance O_o2: O o2. Admitted.

Instance O_o2': O o2'. Admitted.

Lemma oo: o2 = o2'. Proof. reflexivity. Qed.

Definition X

           (f: nat -> nat)

           (g: nat -> nat)

           `{!O f}

           `{!O g} := compose f g.

Lemma foo:

  X o1 o2 = X o1 o2'.

Proof.

  (* The following fails with: 

      Error: build_signature: no constraint can apply on a dependent argument

   *)

  setoid_rewrite oo.

Qed.

Sincerely,
Vadim Zaliva

--

CMU ECE PhD candidate

Mobile: +1(510)220-1060

Skype: vzaliva