The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT inria.fr>]

Hello,

  generalized rewriting won’t let you rewrite the dependent 
index argument of vcons but it does support rewriting the other, 
non-dependent arguments in principle. After some investigation, 
I discovered a de Bruijn bug that prevented this rewriting in arguments 
prior to a dependent argument to succeed. It is now fixed in the trunk 
and the following works. Note the vcons_proper signature is using the 
[forall_relation] combinator which allows to state the signature for 
the (vector A k) argument of (Vcons A x k) and it’s codomain of type 
(vector A (S k)) for any k : nat.

Require Import Setoid.
Require Import Morphisms.
Require Vector.
Notation vector := Vector.t.
Notation Vcons n t := (@Vector.cons _ n _ t). 

Class Equiv A := equiv : A -> A -> Prop.
Class Setoid A `{Equiv A} := setoid_equiv:> Equivalence (equiv).

Instance vecequiv A `{Equiv A} n : Equiv (vector A n).
admit.
Defined.

Global Instance vcons_proper A `{Equiv A} :
 Proper (equiv ==> forall_relation (fun k => equiv ==> equiv))
        (@Vector.cons A).
Proof. Admitted.

Instance vecsetoid A `{Setoid A} n : Setoid (vector A n).
Proof. Admitted.

Goal forall A `{Equiv A} `{!Setoid A} (f : A -> A) (a b : A) (H : equiv a b) 
n (v : vector A n), 
       equiv (Vcons a v) (Vcons b v).
Proof.
  intros.
  rewrite H0.
  reflexivity.
Qed.

  About the vecequiv vs. equiv issue in vcons_proper’s declaration, it 
happens 
because Equivalence vecequiv (needed to find a reflexivity proof for the v 
argument)
cannot be inferred from the setoid_equiv + vecsetoid instances as @equiv ?A 
?e does
not unify with vecequiv. The following declarations make it work:

Instance equiv_setoid A {e : Equiv A} {s : @Setoid A e} : Equivalence e.
apply setoid_equiv.
Qed.
Typeclasses Transparent Equiv. (* This last bit is necessary to convert Equiv 
A and A -> A -> Prop *)

But I would advise to stay with the [equiv] formulation.

Hope this helps,
— Matthieu


On 21 nov. 2014, at 10:13, Vadim Zaliva 
<vzaliva AT cmu.edu>
 wrote:

> With huge help from Daniel we have been able to work out a solution.
> I will summarize my findings in case somebody interested. The main missing 
> part
> was proving Proper for Vcons. It requires two things:
> 
> 1. Reordering Vcons arguments. I did this like this:
> 
> Definition VConsR {A} {n} (t: vector A n) (h:A): vector A (S n) := Vcons h 
> t.
> 
> Lemma ConsR_VConsR: forall A n (t: t A n) (h:A), Vcons h t  ≡ VConsR t h.
> Proof.
>  intros. reflexivity.
> Qed.
> 
> 2. Proving 'Proper' instance:
> 
> Global Instance vconsR_proper `{Equiv A} n:
>  Proper (@vec_equiv A _ n ==> (=) ==> @vec_equiv A _ (S n))
>         (@VConsR A n).
> Proof.
>  split.
>  assumption.
>  unfold vec_equiv, Vforall2 in H0.  assumption.
> Qed.
> 
> Now to use commutativity in the original proof we can just do:
> 
>  rewrite ConsR_VConsR.
>  rewrite commutativity.
> 
> My only remaining regret is that I have two to 2 steps to apply 
> commutativity to Vcons.
> I guess this could be automated via custom tactics, but I have not even 
> started learning LTAC :)
> 
> Vadim
> 
>> On Nov 18, 2014, at 11:25 , Vadim Zaliva 
>> <vzaliva AT cmu.edu>
>>  wrote:
>> 
>> I am trying to prove following lemma:
>> 
>> Lemma map2_setoid_comm `{Equiv B} `{Commutative B A}:
>> forall n (a b: vector A n),
>>    (map2 f a b) = (map2 f b a).
>> 
>> I am using Equiv and Commutative type classes from CoRN. For convenience I 
>> am also using VecUtil from CoLoR which provide several handy definitions 
>> for fixed-size vectors.
>> 
>> Require Import abstract_algebra orders.minmax interfaces.orders.
>> Require Import MathClasses.theory.rings.
>> Require Import CoLoR.Util.Vector.VecUtil.
>> Import VectorNotations.
>> 
>> The equivalence used here (=) is 'equiv'. I was able to instantiate:
>> 
>> Definition vec_equiv `{Equiv A} {n}: relation (vector A n) := Vforall2 
>> (n:=n) equiv.
>> Instance vec_Equiv `{Equiv A} {n}: Equiv (vector A n) := vec_equiv.
>> 
>> which permitted me to use reflexivity tactics to prove IH. Now I am trying
>> to use 'commutativity' but no luck so far:
>> 
>> 1 subgoals, subgoal 1 (ID 1405)
>> 
>> B : Type
>> H : Equiv B
>> H0 : Equiv B
>> A : Type
>> f : A → A → B
>> H1 : Commutative f
>> n : nat
>> a : vector A (S n)
>> b : vector A (S n)
>> IHn : ∀ a0 b0 : vector A n, map2 f a0 b0 = map2 f b0 a0
>> ============================
>>  Vcons (f (Vhead a) (Vhead b)) (map2 f (Vtail a) (Vtail b)) = map2 f b a
>> 
>> As the next step I want rewrite LHS cons head by replacing  (f (Vhead a) 
>> (Vhead b)) with (f (Vhead b) (Vhead a)) by commutativity. I could not make 
>> it work with any of rewrite tactics.
>> 
>> I will appreciate if somebody would point me in the right direction. 
>> Thanks!
>> 
>> Sincerely,
>> Vadim
> 
> Sincerely,
> Vadim Zaliva
> 
> --
> CMU ECE PhD student
> Mobile: +1(510)220-1060
> Skype: vzaliva
>