coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Fabian Kunze <fkunze AT fakusb.de>
To: Fabian Kunze <fkunze AT fakusb.de>, coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Setoid Rewrite with non-transitive (step-indexed) Relations
Date: Fri, 21 Oct 2016 08:26:01 +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:MkXZTBNnCy/X2eTLS6Ml6mtUPXoX/o7sNwtQ0KIMzox0KP36rarrMEGX3/hxlliBBdydsKMezbSO+Pi6ESxYuNDa7yBEKMQNHzY+yuwo3CUYSPafDkP6KPO4JwcbJ+9lEGFfwnegLEJOE9z/bVCB6le77DoVBwmtfVEtfre9ScbuiJGZ3uqz8pubQBhOljf1Nb1xMROkoC3fv8oLmoEkJqtnjlPCpWINcOBLzys8LlWK2h34+82Y/Zh58i0Wteh3pOBaVqCvUa0yTLVeRBc7NXI4rJnltgTFXwan6HIfT34c1BZFVVuWpCrmV4v853Op/tF23zOXaJX7

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

[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