coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Gaetan Gilbert <gaetan.gilbert AT ens-lyon.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] For arbitrary crelations, is symmetry involutive?
Date: Sun, 16 Apr 2017 11:03:43 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gaetan.gilbert AT ens-lyon.fr; spf=Neutral smtp.mailfrom=gaetan.gilbert AT ens-lyon.fr; spf=None smtp.helo=postmaster AT labbe.ens-lyon.fr
Ironport-phdr: 9a23:zacf2R9/21AqvP9uRHKM819IXTAuvvDOBiVQ1KB41u8cTK2v8tzYMVDF4r011RmSDNmds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2e2//5Lebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRgL2hicJNzA382/ZhcJ/g61ZvB2vqAdyw5LXbYyPKPZyYq3QcNMcSGFcXshRTStBAoakYoUOFeUOI/pYoJP7p1ATrBW+BA2sC/jxxT9Smn/9wKo30+s7Hg7YwAwvBdQOvG7brNX0MKcdSv66zLPUzTjYcfxW3yz95JHMchEhpvGMW6h8ccTLyUQ2EQ7Ok1aeqZT9Mj+I2ekBr3KX4uhiWO61lmIqqgN8riKxyssylIXFnoMYxk7e+Slk3Io5O8e0RFN0bNOnCpdcqiKXOoVwT8g/WW9nojw6xacDuZOjfCgF1pAnxxnHZvyDaYeH+QnsW/iLLThmgnJlY6uzhxKy8EinzO3wTMe00ExSoipElNnDqGwN2gTO5sWIVvdx5EWs1DSV2wzO6+xJI1o4mbTFJ5I/2rIwk4AcsUXHHi/4gkX2i6qWe10r+uey9evnfq/pppmGO497iwH+Nr8hldKlAeQkKQUBQW6b+f+l2L3n/Uz5R7NKguc4kqnDqJzaP9gUpralAw9J1YYu8wqwDzC/0NgBgXYHKE9FdwmcgojyO1DOJej4Au2lj1Stljdr3fHGMaf7DpXDNHiQ2IvmKL168gtXzBc55dFZ/ZNdTL8bc9zpXUqkm9XVEhY/eyO1x+zqEsk1gowXVH6GBOmWMafYvEWUzu8pOKyIdYgT/jjnfat2r8XyhGM0zAdONZKi2oEaPSi1

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

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

Gaëtan Gilbert

On 16/04/2017 10:28, John Wiegley wrote:

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.

[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