coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Fabian Kunze <fkunze AT fakusb.de>
- To: coq-club <coq-club AT inria.fr>
- Subject: [Coq-Club] Setoid Rewrite with non-transitive (step-indexed) Relations
- Date: Thu, 20 Oct 2016 08:24:05 +0000
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=fkunze AT fakusb.de; spf=None smtp.mailfrom=fkunze AT fakusb.de; spf=None smtp.helo=postmaster AT tucana.uberspace.de
- Ironport-phdr: 9a23:m1DSAhbFlHBuNSgicrN5OiP/LSx+4OfEezUN459isYplN5qZpsuybnLW6fgltlLVR4KTs6sC0LuM9f2wEjRaqdbZ6TZZL8wKD0dEwewt3CUeQ+e9QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYnbr+tQt2a3IyL0LW5/ISWaAFVjnLparRraR6ysA/5t88MgIIkJLxnmTXTpX4dVe1cxGpubXGOmQTxrpO+/4Nl4Sl4tfsi6tVKF6n3KfdrBYdEBSgrZjhmrPbgsgPOGFOC
Dear Coq-Club,
Is there a way to use setoid_rewrite or something equivalent for non-transitive relations?
I have some indexed relation that is transitive up to adding the index parameter:
"forall (s t u:X) (i j k:nat), i+j=k -> s ~>(i) t -> t ~>(j) u -> s ~>(k) u"
The complete minimal example is at the end of this mail.
I have some indexed relation that is transitive up to adding the index parameter:
"forall (s t u:X) (i j k:nat), i+j=k -> s ~>(i) t -> t ~>(j) u -> s ~>(k) u"
The complete minimal example is at the end of this mail.
I can not register 'Transitive reduce' as 'reduce' is not transitive. I can also not register a proper "Proper"-Instance, as the argument 't' in 'reduce_trans' is in different positions of 'reduce'.
I'm happy for any hints on how to use setoid_rewrite or another tactic/plugin to ease this kind of rewriting.
Best,
Fabian
--------------------------------------------------------------------
Require Import Setoids.Setoid.
Variable X : Type.
Variable reduce : nat -> X -> X -> Prop.
Notation "s '~>(' i ')' t" := (reduce i s t) (at level 50, format "s '~>(' i ')' t").
Axiom reduce_trans :
forall s t u i j k, i+j=k -> s ~>(i) t -> t ~>(j) u -> s ~>(k) u.
Lemma testRewrite s t u i j:
s ~>(i) t -> t ~>(j) u -> s ~>(i+j) u.
Proof.
intros R1 R2.
Fail setoid_rewrite R1. (* Obviously, this fails, as there is no registered instance for anything concerning reduce. But the error message might be helpful to others...*)
(*
s, t, u : X
i, j : nat
R1 : s ~>(i) t
R2 : t ~>(j) u
============================
s ~>(i + j) u
Obviously, this
Error: setoid rewrite failed: Unable to satisfy the following constraints:
UNDEFINED EVARS:
?X21==[s t u i j R1 R2 |- relation X] (internal placeholder) {?r}
?X22==[s t u i j R1 R2 (do_subrelation:=Morphisms.do_subrelation)
|- Morphisms.Proper
(reduce i ==>
?X21@{__:=s; __:=t; __:=u; __:=i; __:=j; __:=R1; __:=R2} ==>
Basics.flip Basics.impl) (reduce (i + j))] (internal placeholder) {?p}
?X23==[s t u i j R1 R2
|- Morphisms.ProperProxy ?X21@{__:=s; __:=t; __:=u; __:=i; __:=j; __:=R1; __:=R2} u]
(internal placeholder) {?p0}
*)
eapply reduce_trans;eauto.
Qed.
- [Coq-Club] Setoid Rewrite with non-transitive (step-indexed) Relations, Fabian Kunze, 10/20/2016
- Re: [Coq-Club] Setoid Rewrite with non-transitive (step-indexed) Relations, John Wiegley, 10/20/2016
- Re: [Coq-Club] Setoid Rewrite with non-transitive (step-indexed) Relations, Fabian Kunze, 10/21/2016
- [Coq-Club] Coercions with constructors of inductive types, richard dapoigny, 10/21/2016
- Re: [Coq-Club] Setoid Rewrite with non-transitive (step-indexed) Relations, Matthieu Sozeau, 10/23/2016
- Re: [Coq-Club] Setoid Rewrite with non-transitive (step-indexed) Relations, Fabian Kunze, 10/21/2016
- Re: [Coq-Club] Setoid Rewrite with non-transitive (step-indexed) Relations, John Wiegley, 10/20/2016
Archive powered by MHonArc 2.6.18.