coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] For arbitrary crelations, is symmetry involutive?

From: "John Wiegley" <johnw AT newartisans.com>
To: Gaetan Gilbert <gaetan.gilbert AT ens-lyon.fr>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] For arbitrary crelations, is symmetry involutive?
Date: Sat, 29 Apr 2017 01:16:15 -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-pg0-f45.google.com
Ironport-phdr: 9a23:ezq+Xxf32CPGp5c0+jIDpCgBlGMj4u6mDksu8pMizoh2WeGdxcS+ZR7h7PlgxGXEQZ/co6odzbGH7+a4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9GiTe5br5+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v9LlgRgP2hygbNj456GDXhdJ2jKJHuxKquhhzz5fJbI2JKPZye6XQds4YS2VcRMZcTyxPDJ2hYYUBCOoPPuhYoIfyqFQSohWzHhWsBPr1xzNUmnP7x6833uI8Gg/GxgwgGNcOvWzaoNvxM6cSUea1x7TIwjXCcfxW1jP955bIcxwvvPqBWrBwcc3RyUkpGQLIlVOQppLrPjyPzOQNr2mb7/F6WuKpkG4rsR1+oj+qxso1jITCm4wbylfB9SpjwYY1I8W1SEhlbt+qCpRQrT2aN4ptQsw4RWFoozw2xaEBuZ6+eiUB1ZcpxwbHZvGFfIWE+A/vWPiRLDtih39odqizihmy/ES4yODxV9O43EhEoydKiNXBt3QA2wbO5sWITvZw+Fqq1yyV2ADJ8O5EJFg5larFJJ4lxb49jp8Tvl7CHi/ygUn2lKCWelk99uim5OnqYq/qppCbN49zhQH+NrohltajDuQ/NwgCR2mb+eKi273/5UD0QrpHgucrnqXHsJ3WP8cWq6CjDwJa0osv8xO/AC2n0NQck3kHNlVFeBefgojrNVDOIe73Dfi7g1uykDZm3P/GPrj7DZXMKnjPiqvufbF460JE0go80chf545ICrEGOP/8RkjxtMXBAhAlNwy03v3oBc5m1oIeXGKPGrWWPLnTsV+O/OIvIvODaJUbuDbneLAZ4KvBhHIlkFlVUqit15YNdDjsEf1rP0yfJ3Xtht0MC3siswwlCej7j1vEXyQFNFioWKdprBM8CITuMobOSYSgkfbJiCW8HptJTmZLFVmWDXbzfoOfHfwLbXTBcYdajjUYWO35GMca3ha0uVq/kuI/Iw==
Organization: New Artisans LLC

>>>>> "GG" == Gaetan Gilbert
>>>>> <gaetan.gilbert AT ens-lyon.fr>
>>>>> writes:

GG> [symmetry] is not involutive: take [R := fun _ _ => bool] and for the
GG> proof of symmetry [fun x y (H : R x y) => true : R y x].

GG> Then for some x and y, [false : R x y] and [symmetry (symmetry false) =
GG> true <> false].

Hi Gaëtan,

How about relations that are known to be equivalences?

Theorem symmetry_invol `{Setoid A} (x y : A) (R : x === y) :
symmetry (symmetry R) = R.

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

[Coq-Club] For arbitrary crelations, is symmetry involutive?, John Wiegley, 04/16/2017
- Re: [Coq-Club] For arbitrary crelations, is symmetry involutive?, Gaetan Gilbert, 04/16/2017
  - Re: [Coq-Club] For arbitrary crelations, is symmetry involutive?, John Wiegley, 04/16/2017
  - Re: [Coq-Club] For arbitrary crelations, is symmetry involutive?, John Wiegley, 04/30/2017
    - Re: [Coq-Club] For arbitrary crelations, is symmetry involutive?, Gaetan Gilbert, 04/30/2017