Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Setoid Rewrite with non-transitive (step-indexed) Relations

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Setoid Rewrite with non-transitive (step-indexed) Relations


Chronological Thread 
  • 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 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.




Archive powered by MHonArc 2.6.18.

Top of Page