coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: "John Wiegley" <johnw AT newartisans.com>
To: Fabian Kunze <fkunze AT fakusb.de>
Cc: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Setoid Rewrite with non-transitive (step-indexed) Relations
Date: Thu, 20 Oct 2016 10:32:42 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jwiegley AT gmail.com; spf=Pass smtp.mailfrom=jwiegley AT gmail.com; spf=None smtp.helo=postmaster AT mail-pf0-f182.google.com
Ironport-phdr: 9a23:K4kmChBWwtcYGynb0ikKUyQJP3N1i/DPJgcQr6AfoPdwSP76psbcNUDSrc9gkEXOFd2CrakV0ayL4+u5ADZIoc7Y9itdINoUD15NoP5VtjJjKfbNMVf8Iv/uYn5yN+V5f3ghwUuGN1NIEt31fVzYry76xzcTHhLiKVg9fbytScb6xv663OGq+pDVfx4AxH/kOeszf12KqlD/v8MXiI0qCbs32BaB9nVLZuJEyEtmLFGOhBy66srmr7B59CEF8dAm98gIbqT3cKA1XPYQWDYhM2YqzMvmqhDZUQqU730HFG4Rl0wbUED+8BjmU8Kp4WPBve1n1XzfZJWuQA==
Organization: New Artisans LLC

>>>>> "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