The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

On Nov 18, 2014, at 16:16 , Vadim Zaliva <vzaliva AT cmu.edu> wrote:

Hmm, that would be a bit tricky - as far as I know, Proper isn't really defined for functions taking dependent types.  I was able to get around it with my definition by using the fact that my @vector_cons A n was a simply typed function for each A, n.  Maybe you could define your own version of Vcons with arguments reordered, then provide trivial rewriting lemmas to convert Vcons to myVcons, and then you could use some Proper result on myVcons to do setoid rewriting.

I will try to do that. Although if that succeeds it would add an extra rewriting step to my proof where I want to use

this kind of rewriting. I guess if I really want to I can automate this via custom rewriting tactic...

I tried that and it looks like it does not solve the initial problem:

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.

Instance vcons_proper `{Equiv A} {n} (t: vector A n):

  Proper ((=) ==> (vec_equiv (A:=A) (n:=S n)))

  (VConsR t).

Now I use it like that:

Proof.

  ...

  rewrite ConsR_VConsR.

Which gets me to the following state:

1 subgoals, subgoal 1 (ID 1456)

  

  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:

Toplevel input, characters 0-84:

Error:

Tactic failure:setoid rewrite failed: Unable to satisfy the rewriting constraints.

Unable to satisfy the following constraints:

EVARS:

 ?1497==[B H H0 A f H1 n a b IHn Heq |- ProperProxy ?1495 (map2 f b a)]

          (internal placeholder)

 ?1496==[B H H0 A f H1 n a b IHn Heq (do_subrelation:=do_subrelation)

          |- Proper (?1491 ==> ?1495 ==> flip impl) equiv]

          (internal placeholder)

 ?1495==[B H H0 A f H1 n a b IHn Heq |- relation (vector B (S n))]

          (internal placeholder)

 ?1492==[B H H0 A f H1 n a b IHn Heq (do_subrelation:=do_subrelation)

          |- Proper (equiv ==> ?1491) (VConsR (map2 f (Vtail a) (Vtail b)))]

          (internal placeholder)

 ?1491==[B H H0 A f H1 n a b IHn Heq |- relation (vector B (S n))]

          (internal placeholder)

UNIVERSES:

 Top.17049 <= MathClasses.interfaces.canonical_names.8

 Top.17048 <= MathClasses.interfaces.canonical_names.8

 Top.17047 <= Coq.Classes.SetoidTactics.11

 Top.17046 <= MathClasses.interfaces.canonical_names.611

 Top.17043 <= MathClasses.interfaces.canonical_names.608

 Top.10792 <= Top.9679

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

 Top.10748 <= Spiral.387

 Top.10747 <= Spiral.386

 Top.10746 <= Spiral.385

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

 Top.10297 <= Top.10296

 Top.10292 <= Coq.Program.Equality.1

 Top.10291 <= Coq.Program.Equality.1

 Top.10272 <= Top.10271

 Top.10267 <= Coq.Program.Equality.1

 Top.10266 <= Coq.Program.Equality.1

 

Which is similar to the error I was getting earlier. Perhaps missing Proper was not the problem?

Sincerely,
Vadim