The Coq mailing list

[Fabian Kunze <fkunze AT fakusb.de>]

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.