The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi Fabian,

  I don't think there's any ready to use tactic for your example, but you might want to have a look at the https://github.com/CertiKOS/coqrel library for logical relations [1], which might help in this case. We're currently thinking about mixing this library with the generalized rewriting/setoid_rewrite tactic to allow for this kind of dependent/heterogeneous rewriting [2], but we're not there yet.

[1] A Coq Library for Binary Logical Relations - Jerémie Koenig, Yale University 

http://www.chargueraud.org/events/coqpl2016/CoqPL_2016_paper_7.pdf 

[2] https://github.com/mattam82/RewriteStrat

Best,

-- Matthieu

On Fri, Oct 21, 2016 at 11:27 AM Fabian Kunze <fkunze AT fakusb.de> wrote:

Hi,

My intention was to rewrite 'with reduce_trans', so i would hope to be left with t ~>(j) u and the side condition i+j=i+j (by instantiation of the k in reduce_trans, since by rewriting in the goal, we would force the goal to instantiate the conclusion of reduce_trans).

Best,

Fabian

John Wiegley <johnw AT newartisans.com> schrieb am Do., 20. Okt. 2016 um 19:32 Uhr:

>>>>> "FK" == Fabian Kunze <fkunze AT fakusb.de> writes:

FK> I can not register 'Transitive reduce' as 'reduce' is not transitive. I
FK> can also not register a proper "Proper"-Instance, as the argument 't' in
FK> 'reduce_trans' is in different positions of 'reduce'.

forall (R1 : s ~>(i) t), t ~>(j) u -> s ~>(i+j) u.

Wouldn't a rewrite using R1 here result in the goal: t ~>(i+i+j) u?

--
John Wiegley                  GPG fingerprint = 4710 CF98 AF9B 327B B80F
http://newartisans.com                          60E1 46C4 BD1A 7AC1 4BA2