The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

Matthieu,

After switching to 8.5 I decided to see if I can take advantage of your 
bug fix to avoid Vector.cons argument reordering workaround I’ve used
before. To recap, I was using the following definitions to replace
Vector.cons with Vcons_reord which allowed me to rewrite its arguments:

Section VCons_p.
  Definition Vcons_reord {A} {n} (t: vector A n) (h:A): vector A (S n) := 
Vcons h t.

  Lemma Vcons_to_Vcons_reord: forall A n (t: vector A n) (h:A), Vcons h t  ≡ 
Vcons_reord t h.
  Admitted.

  Global Instance Vcons_reord_proper `{Equiv A} n:
    Proper (@vec_equiv A _ n ==> (=) ==> @vec_equiv A _ (S n))
           (@Vcons_reord A n).
  Admitted.
End VCons_p.

Now I get rid of this and defined Instance of vcons_proper as shown below and 
tried to rewrite
Vcons directly. It works if I rewrite the first argument (of type A), but 
does not allow me to rewrite
second one (of type (vector A n)). Here is example using your definitions 
below:

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

Any ideas why this is not working? Exact error message:

Tactic failure: setoid rewrite failed: Unable to satisfy the following 
constraints:
UNDEFINED EVARS:
 ?X83==[A H Setoid0 f h n a b Z |- relation (vector A (S n))]
         (internal placeholder) {r}
 ?X84==[A H Setoid0 f h n a b Z (do_subrelation:=do_subrelation)
         |- Proper
              (equiv ==>
               ?X83@{A:=A; A:=H; A:=Setoid0; A:=f; A:=h; A:=n; A:=a; A:=b;
                     A:=Z}) (Vector.cons A h n)] (internal placeholder) {p}
 ?X86==[A H Setoid0 f h n a b Z |- relation (vector A (S n))]
         (internal placeholder) {r0}
 ?X87==[A H Setoid0 f h n a b Z (do_subrelation:=do_subrelation)
         |- Proper
              (?X83@{A:=A; A:=H; A:=Setoid0; A:=f; A:=h; A:=n; A:=a; A:=b;
                     A:=Z} ==>
               ?X86@{A:=A; A:=H; A:=Setoid0; A:=f; A:=h; A:=n; A:=a; A:=b;
                     A:=Z} ==> Basics.flip Basics.impl) equiv]
         (internal placeholder) {p0}
 ?X88==[A H Setoid0 f h n a b Z
         |- ProperProxy
              ?X86@{A:=A; A:=H; A:=Setoid0; A:=f; A:=h; A:=n; A:=a; A:=b;
                    A:=Z} (Vcons h b)] (internal placeholder) {p1}.

Sincerely,
Vadim


> On Nov 23, 2014, at 6:09 , Matthieu Sozeau 
> <matthieu.sozeau AT inria.fr>
>  wrote:
> 
> 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
>> 
> 

Sincerely,
Vadim Zaliva

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