Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] setoid rewriting -- naive questions

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] setoid rewriting -- naive questions


Chronological Thread 
  • From: Vadim Zaliva <vzaliva AT cmu.edu>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] setoid rewriting -- naive questions
  • Date: Tue, 18 Nov 2014 16:51:17 -0800


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 



Archive powered by MHonArc 2.6.18.

Top of Page