The Coq mailing list

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

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

In your case, I would redefine my `f` so that it has the following type:

f: {i | i<n} -> A -> A

Then I would declare the equality Instance for  {i | i<n}  to be the equality of the corresponding first projections.

Then I would prove an instance of the form

Proper (equal  ==> equal  ==> equal ) f.

Below is a complete example using MathClasses:

Require Import MathClasses.interfaces.canonical_names.

Require Import MathClasses.theory.setoids.

Require Import MathClasses.implementations.peano_naturals.

Section rewriteTest.

Variable A:Type.

Variable  n:nat.

Variable f: {i | (i<n)%nat} -> A -> A.

Global Instance Equiv1 : Equiv {i | (i<n)%nat} := sig_equiv _.

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

Global Instance ProperF :

Proper (equiv ==> equiv ==> equiv) f.

Admitted.

Lemma rewriteTest : forall i1 i2 p1 p2 a1 a2, 

i1=i2

-> a1=a2

-> f (i1 ↾ p1) a1 = f  (i2 ↾ p2) a2.

Proof using All.

  intros ? ? ? ? ? ? H1 H2.

  change ((i1 ↾ p1) = (i2 ↾ p2)) in H1.

  rewrite H2.

  rewrite H1.

  reflexivity.

Qed.

End rewriteTest.

-- Abhishek

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

On Tue, Dec 29, 2015 at 6:36 PM, Vadim Zaliva <vzaliva AT cmu.edu> wrote:

I have a family of functions defined like this:

f: forall i, i<n -> A -> A

where {A:Type} and {n:nat}. Now I need to specify that for all ‘i’
A->A are proper wrt. my custom equality (equal). In other words
for all ‘i’ following holds:

`{pF: !Proper ((equal) ==> (equal)) f}

What is the best way to specify this, so I can make use of it in
setoid rewriting?

Thanks!

Sincerely,
Vadim Zaliva

--
CMU ECE PhD candidate
Mobile: +1(510)220-1060
Skype: vzaliva