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: Sun, 16 Apr 2017 02:24:30 -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-f44.google.com
Ironport-phdr: 9a23:cErJ5RQ/fJ2GJuvk8gcvXLyv2dpsv+yvbD5Q0YIujvd0So/mwa6yYBeN2/xhgRfzUJnB7Loc0qyN4vymATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSijewZbx/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4rx1QxH0ligIKz858HnWisNuiqJbvAmhrAF7z4LNfY2ZKOZycqbbcNgHR2ROQ9xRWjRBDI2icoUADeQPPeFboYnzqVQBogexCwa3CePz0z9FnGP60bEg3ukjFwzNwQwuH8gJsHTRtNj5OqMcUee1zKnO0D7Mb/JW1iny6IjMbB8gof+AVq93fMrTzkkvFwXFj1uLpIzjITyU2P4Cs3KH7+phTuKgkWgnqxprrjezwccsj5DEi4QIwV7K8iV5xZw6Jdy+SENjZ96rDpVRuDuAN4tqQ8MiWHtnuCAhyrEcpZG7ey0KxZI6zBDcc/yKa4qF7x35WOqMPzt1hGhpdbGxihqo/kWtxfXwW8u13VpQsCZInNbBumoM2hHX8MSLV/Rw80On1D2SzQ7c8PtELloxlafDK54u3Lowlp0LvETGBCD2mUH2gLaOdkUr5uSk8urnb7rpq5OGOI90jQb+MqsqmsOhG+g3Lg8OX22D9eS90r3s41H5Ta1Ig/A5iKXVrY7WKMQBqqO6DQJZyIku5hmnAzejytsYnH0HLFxfeBKAiojkI1POIf75DfihjFSslClkxvDdM73uB5XCNHnDkLP7cblh7E5czRI/zcpD6JJMFrEBPPXzV1ftu9zfFx81KhC7w+L6CNpmzY4eQmKOAqqBMKzIq1OI5+QvI/ONZIAPojr9JeIltLbSiioWkFIBdK/h8poTYn2iArwyLEyUfXPqxNgAFW0HpBYWQerxzVmTVjgVaWzkDIwm4TRuQqChDYGLeYGgj7iMzW3zSp9RZmZZIlaBDn7ya4SfUvEXLimVJ5kywXQ/SbG9Rtp5hlmVvwjgxu8id7KM9w==
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].

Thank you, Gaëtan.

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