Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • 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



Archive powered by MHonArc 2.6.18.

Top of Page