coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] setoid rewriting, partial application and relfexivity

From: "John Wiegley" <johnw AT newartisans.com>
To: Vadim Zaliva <vzaliva AT cmu.edu>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] setoid rewriting, partial application and relfexivity
Date: Thu, 16 Feb 2017 23:05:16 -0800
Authentication-results: mail3-smtp-sop.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:INUkbxPskknDe95lM04l6mtUPXoX/o7sNwtQ0KIMzox0Ivn7rarrMEGX3/hxlliBBdydsKMZzbKL+Pm4ByQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9GiTe5Yb5+Ngm6oAXeusULnYdvK7s6xwfUrHdPZ+lY335jK0iJnxb76Mew/Zpj/DpVtvk86cNOUrj0crohQ7BAAzsoL2465MvwtRneVgSP/WcTUn8XkhVTHQfI6gzxU4rrvSv7sup93zSaPdHzQLspVzmu87tnRRn1gyocKTU37H/YhdBxjKJDoRKuuRp/w5LPYIqIMPZyZ77Rcc8GSWZEWMtaSi5PDZ6mb4YXD+QPI/tWoIvzqVsJrhW+CwejC+zzxTJTmn/6wbc33/g9HQzcwAAtGc8FvnTOrNXyMacfSe65wq3PzTXDafNdxDfy6InWfRAupfGDQ7JxfcTMwkQoFQPFiVWQqYrrPj6O0OQCrWaa4PB6VeKzim4nsBt+oj60xss2lobJgYcVx0nC+C5kzog1Iti4R1R6Yd6iCJZQsT+VNoVsTcM4X2FouT06xacAuZ6gZiQF1JMnxxvZZveacIaI+gruWPiNLTp8nn5oe7Kyiwyv/UWk1OHwTNS43VVUoiZdkNTBt2oB2wLd58WIUPdw/0Os1SyS2w3c7uxJJ10/m7DBJJ472LEwk4IesUTdES/yn0X7lKqWeV8l+uis8ujnervmqoOFO496lw3zMboiltawAeQ/NQgOUGyb9vqm2LL/+k35Ra1GjvwwkqbHrJDXPdoXqrK9DgNP0Ysu6wyzAyqi3dgGh3ULMVFIdAyfg4jsIV7OIfT4Dfmlg1SrlTdm3/LGP7PgAprTIXjDlKnufLZm5k5TzQo819Ff55ZOBr4dJ/LzX1f9tMbEAR8hLwy03+HnBc1h2YMZQGKDG7OWMKfPsVCT/e8vOOmNZIoNuDnnMfQl5vjujWU4mVAHZ6Wp04EXOziEGaFYKkmYZDLei9MAD25C6hQsRejrllSqWjtOIXu+QvRvyCs8DdfsL4DDQMiSgbGO2CqqVNUCZGdGDE+kF3r3fp+YWuwFbjnUKchkxG9XHYO9QpMsgEn9/DTxzKBqe6+NonUV
Organization: New Artisans LLC

>>>>> "VZ" == Vadim Zaliva
>>>>> <vzaliva AT cmu.edu>
>>>>> writes:

VZ> Of course, R must be reflexive. But adding:

VZ> Instance R_reflexive: Reflexive R. Admitted.

VZ> Does not help either.

Turns out you need Transitive also.

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

[Coq-Club] setoid rewriting, partial application and relfexivity, Vadim Zaliva, 02/17/2017
- Re: [Coq-Club] setoid rewriting, partial application and relfexivity, Vadim Zaliva, 02/17/2017
  - Re: [Coq-Club] setoid rewriting, partial application and relfexivity, John Wiegley, 02/17/2017
    - Re: [Coq-Club] setoid rewriting, partial application and relfexivity, Vadim Zaliva, 02/18/2017
      - [Coq-Club] Question about maximum operation for universe levels in Coq, Erik Palmgren, 02/21/2017
        
        Re: [Coq-Club] Question about maximum operation for universe levels in Coq, Bas Spitters, 02/22/2017