coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: "John Wiegley" <johnw AT newartisans.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] For arbitrary crelations, is symmetry involutive?
Date: Sun, 16 Apr 2017 01:28:17 -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-f173.google.com
Ironport-phdr: 9a23:Tc3+8R+ij24plf9uRHKM819IXTAuvvDOBiVQ1KB42+ocTK2v8tzYMVDF4r011RmSDNmds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2e2//5Lebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRh/2hikaOTA592LZhcJ/g61Hux+huwBzzpTIbI2JLvdyYqXQds4aS2pbWcZRUjRMDo24YYsID+oBO/tToIn8p1QQohu+ARejBePhxjRVgXL236o60+QnEQDIxwEgGcwBsXrOo9XvKKcSUPu1w7POzTXYdf9ZxTD96I3Rfx0nvPqCU7Vwcc/LxkkuEQPIllOQppLrPjyPzOQNr2mb7/F6WuKpkG4rsR1+oj+qxsoql4LHhZoVx0ja+SllxIs5P961RU5hbdK5FJZcqTuWO5Z0T84sW21luic3xqcYtZO1cyUG0pUqyhrFZ/CafIWF5hTuX/uLLzhinnJqYre/ig6y8Ue+zu38UdG50FNQoSpEltnAr2gN1xLP5sSeRPtx40Ws1DiV2wDc7eFEJk80la7FJJI73rEwkZ8TvVzCHi/whkr2kLebels49uWs8ejqYbXrqoWBO4JwlA3yKLkil86xDOggNwgBRWmb+eCy1L35+k35Ra1Hjv84k6nYrp/aKsAbqbC5AgJO3YYj7gywDzai0NgCgXYHK1dFdAqdj4f1I1HOPOz4DfCnjluwlzdr3unKMaHlApXQNXfOi6zhfLZ4605E0gU/19Ff55ROCrEAOv3/QEHxtMaLRiM+Zgez2qPsDMh3/oIYQ2OGRKGDY43ItlrdrMAoI+/EW44YtzLwOrJts/zpjXkmsVkQYqCzwZoMYXajWP9hJhPKMjLXnt4dHDJS7UIFR+vwhQjaXA==
Organization: New Artisans LLC

I'm having difficulty with how to approach the following, since I have no
theories about symmetry to work with in the standard library.

Lemma symmetry_involutive
`{R : crelation A} `{Symmetric _ R} {x y : A} (f : R x y) :
symmetry (symmetry f) = f.

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