The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

On May 7, 2015, at 16:13 , Jason Gross <jasongross9 AT gmail.com> wrote:

You get more useful output if you [Set Typeclasses Debug], and then do [try rewrite Z].  The issues are:

(?X84) you are missing a Vcons_proper instance; this works:

Global Instance Vcons_proper A `{H:Equiv A} n a:

  Proper (@equiv (vector A (n)) (@vecequiv A H (n)) ==> equiv) (@Vcons A a n).

Admitted.

Thanks for debug suggestion!

After 'Set Typeclasses Debug’ here is the output:

Debug: : no match for (Params H0 ?H1) , 0 possibilities

Debug: 1.1: (*external*) proper_subrelation on

(Proper (equiv ==> ?r) (Vector.cons A h n))

Debug: : no match for (Params H0 ?H1) , 0 possibilities

Debug: 1.1.1.1: (*external*) proper_reflexive on

(Proper ?R' (Vector.cons A h n))

Debug: 1.1.2.1: (*external*) unconvertible on

(Unconvertible (relation (vector A n -> vector A (S n)))

   (equiv ==> ?r)%signature eq)

Debug: 1.1.3: no match for (subrelation eq (equiv ==> ?r)%signature)

, 1 possibilities

Debug: Backtracking after (*external*) unconvertible

Debug: Backtracking after (*external*) proper_reflexive

Debug: Backtracking after (*external*) proper_subrelation

Debug: 1.2: (*external*) proper_normalization on

(Proper (equiv ==> ?r) (Vector.cons A h n))

Debug: 1.2.1.1: (*external*) normalizes on

(Normalizes (vector A n -> vector A (S n)) (equiv ==> ?r)%signature ?R1)

Debug: 1.2.1.1.1.1: (*external*) normalizes on

(Normalizes (vector A n) equiv (Basics.flip ?Goal3))

Debug: 1.2.1.1.2.1: (*external*) normalizes on

(Normalizes (vector A (S n)) ?r (Basics.flip ?Goal5))

Debug: 1.2.2.1: (*external*) class_apply @proper_flip_proper on

(Proper (Basics.flip (equiv --> Basics.flip ?r)%signature)

   (Vector.cons A h n))

Debug: 1.2.2.1.1.1: (*external*) proper_subrelation on

(Proper (equiv --> Basics.flip ?r) (Vector.cons A h n))

Debug: 1.2.2.1.1.1.1: no match for (Proper ?R' (Vector.cons A h n))

, 6 possibilities

Debug: Backtracking after (*external*) proper_subrelation

Debug: Backtracking after (*external*) class_apply @proper_flip_proper

Debug: 1.2.2.2: (*external*) proper_subrelation on

(Proper (Basics.flip (equiv --> Basics.flip ?r)%signature)

   (Vector.cons A h n))

Debug: 1.2.2.2.1: no match for (Proper ?R' (Vector.cons A h n))

, 6 possibilities

Debug: Backtracking after (*external*) proper_subrelation

Debug: Backtracking after (*external*) normalizes

Debug: Backtracking after (*external*) normalizes

Debug: Backtracking after (*external*) normalizes

Debug: Backtracking after (*external*) proper_normalization

Debug: 1.3: (*external*) proper_reflexive on

(Proper (equiv ==> ?r) (Vector.cons A h n))

Debug: 1.3.1.1: apply @Equivalence_Reflexive on

(Reflexive (equiv ==> ?r)%signature)

Debug: 1.3.1.1.1: no match for (Equivalence (equiv ==> ?r)%signature)

, 1 possibilities

Debug: Backtracking after apply @Equivalence_Reflexive

Debug: 1.3.1.2: apply @PreOrder_Reflexive on

(Reflexive (equiv ==> ?r)%signature)

Debug: 1.3.1.2.1: no match for (PreOrder (equiv ==> ?r)%signature)

, 1 possibilities

Debug: Backtracking after apply @PreOrder_Reflexive

Debug: Backtracking after (*external*) proper_reflexive

Toplevel input, characters 5-15:

>   rewrite Z.

>   ^^^^^^^^^^

I do have Proper instance for Vcons defined as follows:

Global Instance vcons_proper A `{Equiv A} :

 Proper (equiv ==> forall_relation (fun k => equiv ==> equiv))

        (@Vector.cons A).

Proof. Admitted.

But it does not seems to be applicable here. I am trying to understand why.

I also tried to use your definition of Vcons_proper and it gives me error:

Error: Illegal application (Non-functional construction): 

The _expression_ "Vcons A a" of type "vector Type (S ?n)"

cannot be applied to the term

 "n" : "nat"

I am using latest build from v8.5 branch.

Sincerely,
Vadim Zaliva

--

CMU ECE PhD candidate

Mobile: +1(510)220-1060

Skype: vzaliva