The Coq mailing list

[Gregory Malecha <gmalecha AT gmail.com>]

Hello --

It does not look like you have any morphisms defined for 'X' and as it is it is probably difficult to define one. The issue, as the error message states, is that the type of [X] is dependent on the argument it is given. You can see this by printing implicit arguments.

Set Printing Implicit.

Here you will see that your problem is actually:

X o1 o2 O_o1 O_o2 = X o1 o2' O_o1 O_o2'.

In this problem, [setoid_rewrite] does not support rewriting like this. Supporting it would require finding a new instance to replace [O_o2] on the left-hand side of the equality and it would need to know that the value of [O_o2] can be replaced with another one. Writing these types of morphisms is a bit more complicated.

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

On Wed, Dec 30, 2015 at 5:13 PM, Vadim Zaliva <vzaliva AT cmu.edu> wrote:

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

--

gregory malecha