coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- Re: [Coq-Club] For arbitrary crelations, is symmetry involutive?, Gaetan Gilbert, 04/16/2017
Archive powered by MHonArc 2.6.18.