The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Tue, Nov 18, 2014 at 4:51 PM, Vadim Zaliva <vzaliva AT cmu.edu> wrote:

  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

  ============================

   VConsR (map2 f (Vtail a) (Vtail b)) (f (Vhead a) (Vhead b)) = map2 f b a

At this point trying:

  replace (f (Vhead a) (Vhead b)) with (f (Vhead b) (Vhead a)) by commutativity. 

Gives:

... 

 

You appear to have two instances of Equiv B, which could be confusing things.  My guess would be that you have something like `{Equiv B} `{Commutative f} where the second should be `{!Commutative f} instead.  Also, I don't see any instances of Setoid B which could be useful in inferring Setoid (Vector.t B (S n)), which in turn would be useful for doing the rewriting.

That said, when I tried it with a similar situation with only one Equiv B, and Setoid B in the context (and a registered instance of forall (A:Type) `{Setoid A} (n:nat), Setoid (Vector.t A n)), it still didn't work for me.

1 subgoals

A : Type

B : Type

f : A -> A -> B

H : Equiv B

H0 : Setoid B

Commutative0 : Commutative f

h : A

n : nat

w : Vector.t A (S n)

h' : A

n0 : nat

t' : Vector.t A n0

v0 : Vector.t A n0

IHv0 : forall y : Vector.t A n0, (=) (map2 f v0 y) (map2 f y v0)

H1 : (=) (f h h') (f h' h)

H2 : forall (A0 : Type) (H2 : Equiv A0) (n1 : nat),

     Proper ((=) ==> vector_equiv A0 n1 ==> vector_equiv A0 (S n1))

       vcons_reord

H3 : forall (A0 : Type) (H3 : Equiv A0),

     Setoid A0 -> forall n1 : nat, Setoid (Vector.t A0 n1)

______________________________________(1/1)

(=) (vcons_reord (f h h') (map2 f v0 t'))

  (vcons_reord (f h' h) (map2 f t' v0))

rewrite H1.

==>

Error:

Tactic failure:Unable to satisfy the rewriting constraints.

Unable to satisfy the following constraints:

EVARS:

 ?394==[A B f H H0 Commutative0 h n w h' n0 t' v0 IHv0 H1

         |- ProperProxy ?392 (vcons_reord (f h' h) (map2 f t' v0))]

         (internal placeholder)

 ?393==[A B f H H0 Commutative0 h n w h' n0 t' v0 IHv0 H1

         (do_subrelation:=do_subrelation)

         |- Proper (?385 ==> ?392 ==> Basics.flip Basics.impl) (=)]

         (internal placeholder)

 ?392==[A B f H H0 Commutative0 h n w h' n0 t' v0 IHv0 H1

         |- relation (Vector.t B (S n0))] (internal placeholder)

 ?388==[A B f H H0 Commutative0 h n w h' n0 t' v0 IHv0 H1

         |- ProperProxy ?386 (map2 f v0 t')] (internal placeholder)

 ?387==[A B f H H0 Commutative0 h n w h' n0 t' v0 IHv0 H1

         (do_subrelation:=do_subrelation)

         |- Proper ((=) ==> ?386 ==> ?385) vcons_reord]

         (internal placeholder)

 ?386==[A B f H H0 Commutative0 h n w h' n0 t' v0 IHv0 H1

         |- relation (Vector.t B n0)] (internal placeholder)

 ?385==[A B f H H0 Commutative0 h n w h' n0 t' v0 IHv0 H1

         |- relation (Vector.t B (S n0))] (internal placeholder)

UNIVERSES:

 Top.9442 <= Top.7471

 Top.9441 <= Top.7470

 Top.9438 <= Top.6223

 Top.9423 <= Top.7236

 Top.9422 <= Coq.Init.Logic.47

 Top.9408 <= Top.7236

 Top.9407 <= Coq.Init.Logic.47

 Top.9002 <= Coq.Vectors.VectorDef.3

 

.

-- 

Daniel Schepler