coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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 usethis 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
Vadim
- [Coq-Club] setoid rewriting -- naive questions, Vadim Zaliva, 11/18/2014
- Re: [Coq-Club] setoid rewriting -- naive questions, Robbert Krebbers, 11/18/2014
- Re: [Coq-Club] setoid rewriting -- naive questions, Vadim Zaliva, 11/18/2014
- Re: [Coq-Club] setoid rewriting -- naive questions, Daniel Schepler, 11/18/2014
- Re: [Coq-Club] setoid rewriting -- naive questions, Vadim Zaliva, 11/19/2014
- Re: [Coq-Club] setoid rewriting -- naive questions, Daniel Schepler, 11/19/2014
- Re: [Coq-Club] setoid rewriting -- naive questions, Vadim Zaliva, 11/19/2014
- Re: [Coq-Club] setoid rewriting -- naive questions, Vadim Zaliva, 11/19/2014
- Re: [Coq-Club] setoid rewriting -- naive questions, Daniel Schepler, 11/19/2014
- Re: [Coq-Club] setoid rewriting -- naive questions, Vadim Zaliva, 11/19/2014
- Re: [Coq-Club] setoid rewriting -- naive questions, Jonathan, 11/19/2014
- Re: [Coq-Club] setoid rewriting -- naive questions, Daniel Schepler, 11/19/2014
- Re: [Coq-Club] setoid rewriting -- naive questions, Robbert Krebbers, 11/19/2014
- Re: [Coq-Club] setoid rewriting -- naive questions, Vadim Zaliva, 11/19/2014
- Re: [Coq-Club] setoid rewriting -- naive questions, Daniel Schepler, 11/19/2014
- Re: [Coq-Club] setoid rewriting -- naive questions, Vadim Zaliva, 11/21/2014
- Re: [Coq-Club] setoid rewriting -- naive questions, Daniel Schepler, 11/21/2014
- Re: [Coq-Club] setoid rewriting -- naive questions, Vadim Zaliva, 11/19/2014
- Re: [Coq-Club] setoid rewriting -- naive questions, Daniel Schepler, 11/19/2014
- Re: [Coq-Club] setoid rewriting -- naive questions, Vadim Zaliva, 11/19/2014
- Re: [Coq-Club] setoid rewriting -- naive questions, Daniel Schepler, 11/18/2014
- Re: [Coq-Club] setoid rewriting -- naive questions, Vadim Zaliva, 11/18/2014
- Re: [Coq-Club] setoid rewriting -- naive questions, Robbert Krebbers, 11/18/2014
Archive powered by MHonArc 2.6.18.