Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] A fast "eq" predicate for Gallina?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] A fast "eq" predicate for Gallina?


Chronological Thread 
    < Chronological >      < Thread >
  • From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
  • To: Xavier Leroy <Xavier.Leroy AT inria.fr>
  • Cc: coq-club AT inria.fr, Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
  • Subject: Re: [Coq-Club] A fast "eq" predicate for Gallina?
  • Date: Thu, 21 Jan 2021 10:45:27 -0500
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk1-f177.google.com
  • Ironport-phdr: 9a23:jSq2zhELmVIUCz/BjLo2pZ1GYnF86YWxBRYc798ds5kLTJ76ps24bnLW6fgltlLVR4KTs6sC17OH9fm8EjNdqdbZ6TZeKcMKD0dEwewt3CUYSPafDkP6KPO4JwcbJ+9lEGFfwnegLEJOE9z/bVCB6le77DoVBwmtfVEtfre9FYHdldm42P6v8JPPfQpImCC9YbRvJxmqsAndrMYbjZZmJ6or1xfErXREduZWyGh1IV6fgwvw6t2/8ZJ+8Slcoe4t+9JFXa7nY6k2ULtUASg8PWso/sPrrx7DTQWO5nsYTGoblwdDDhbG4h/nQJr/qzP2ueVh1iaUO832Vq00Vi+576h3Uh/oiTwIOCA//WrKl8F/lqNboBampxxi347ZZZyeOfRicq/Be94RWHFMVdhNWSNfHoy8bpMPD+sfMuZes4n9vEYFoR+nCQWxGO/j1jpEi3nr1qM4zushCxnL0gIgEdwQrXrar9f6NKkVX++60KbGwi7Ob+9U1Drn9ITFaAwtre+KULltccTR004vFwbdg1meq4zlODWV1uUOs2eF6+pvS/yghnUoqwF0uDevx8MshpPViYISz1DI+zhyzYE3Jd2/Tk57YN2kH4VUty6EKYR7WcwiQ2RytyY7zr0Ko4K0fC8PyJk+wRPUdvOIfZSS7B35SOaRPSl3hGhjeL+nmxq//lWsxvDiW8S001tHrSVIn8fCuH0C2RLe5MaKRuVz80qhxDuCygDd5+9ZLU0qm6TWNZ0szLA0m5QTsUrOHSn7k1j1gq+Obkgo5PSk5uD9brjlppKQLZF4hh/gPqg0h8CyA+Y1PhAQU2Wa5eiwybju8VD9TbpWi/A7najUvIzGKckeu6K0ABNZ34Mh5hqjATepy9EVkHcaIFJLdhKKiobpNE/UL/zmCPqyjU6jnCltyvvbJLPuGI/NIWLGkLr5fbZy9UpcyA0rwNBa/Z1UC7UBLOvqWk/yqdDUFxE5PxG2zuvlEtl92YQeWWWAAq+dLqzeq0OH5uUqI+WUZY8VvijyK+Q96vLwkXM0nUURcKqp0JcNdny0AOpqL1+EbXfugNoNCWIKsRA/TOzuhl2CSzlTZ3OqUqI+4TE7DoOmDYTdSYCpnrOOwjy2HpJTZm9cC1CMFW3keJmDW/cJcC6SONNukiQYVbi9TI8szR6vtAvkxLp9KerV+jYVtJPi1Nhw/OLTjws9+SZ1D8SbyWGNTnt7knkGRz8sxKp/u1Byyk+f0ahkhPxVDcBc5/RQUgsjKZHcy/F6BMvpVwLaftaJTU6mTc+8DTEwSNIx2d4ObFxnF9WslBDJxzCqDKMNl7yXGJw09brR32DvKMlg0XbG07UhgkInQ8tOMG2pnbR/+BLJC47IlUWZjaeqer4G0C7D7mfQhVaJ6XFRTg99S+3hUGoYdwOCnd3n507YCZujE7M2GgpH08+LbKVQPI7Hl1JDEb3hP9LfYG+1lmqYChOBx7fKZ43vMS1J3iLbCUsJlw0e1XmDPAk6QCympjSNX3RVCVvzbha0oqFFo3ShQxpxllnSNhEz5/+O4hcQwMekZbYLxLtd4XUurjx1GBC22NeEU4PR9TokR71VZJYG2HkC0GvYswJnOZn5dvJtg1cfd0J8uEa8jkwqWLUFqtAjqTYR9CQ3Ka+c1wkfJTaR3JS1I76Ob2ero0/pZKnR1VXTlt2R//VX5Q==
On Thu, 21 Jan 2021 11:14:40 +0100
Xavier Leroy <Xavier.Leroy AT inria.fr> wrote:

> On Wed, Jan 20, 2021 at 10:18 PM jonikelee AT gmail.com
> <jonikelee AT gmail.com> wrote:
>
> > It occurs to me that I don't really need "eq x y = true -> x = y",
> > but instead can get by with "eq x y = false -> x <> y"
>
>
> This is just as inconsistent. If x and y are (structurally) equal but
> physically unequal, you get false = false -> ~True.

right. But fortunately the almost-UID scheme holds up better than my
ego at the moment. It doesn't require any impossible eq function - just
an equality function that checks the UID first and gives up on
checking the rest of the structures if the UIDs are not equal.

Archive powered by MHonArc 2.6.19+.

Top of Page