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 
  • From: Adam Chlipala <adamc AT csail.mit.edu>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] A fast "eq" predicate for Gallina?
  • Date: Wed, 20 Jan 2021 15:24:14 -0500
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=adamc AT csail.mit.edu; spf=Pass smtp.mailfrom=adamc AT csail.mit.edu; spf=None smtp.helo=postmaster AT outgoing-stata.csail.mit.edu
  • Ironport-phdr: 9a23:u8DD1B1DoZjnXvuvsmDT+DRfVm0co7zxezQtwd8ZseIQL/ad9pjvdHbS+e9qxAeQG9mCurQd0aGP6vmoGTRZp8rY7zZaKN0EfiRGoP1epxYnDs+BBB+zB9/RRAt+Iv5/UkR49WqwK0lfFZW2TVTTpnqv8WxaQU2nZkJ6KevvB4Hdkdm82fys9J3PeQVIgye2ba9vIBmsogjdq80bjZF/JqovxRfFv2ZEd/lLzm9sOV6fggzw68it8JNh6Shcp+4t+8tdWqjmYqo0SqBVAi47OG4v/s3rshfDTQqL5nQCV2gdjwRFDQvY4hzkR5n9qiT1uPZz1ymcJs32UKs7WS++4KdxSR/nkzkIOjgk+2zKkMNwjaZboBW8pxxjxoPffY+YOOZicq7bYNgXQ3dKUMRMWCxbGo6ycpUBD+QBM+hboYfyqVQBohmiCgejH+7v1jxFi2Xq0aEm3eksEwfL1xEgEdIUt3TUqc34ObsPXu+vyanD0CvOb/NS2Tf88IjHaBQhruuRVr93a8Xe1FMgFwbZgViLtYPlJCma1uUJs2SB6upgVP6vh3Q5pA5svzii38EhgZTGiYwJ0F7L7zl5wJorKt2iTk52ecKpHIdNuiyYNIZ4QsEvT39stSsm17EKpZ+2cicJxZg52xPRZfyJfouH7B/+UOucLzl1inxhdby/mxu/7EitxvD6W8Kp01hKtjJInsTSun0OzRDe5NSLRuFj8ku7xzqDyhzf5vlGLE06j6bXNYMtz7oqmpcSsUnPBDL6lFvqgKKQa04q4PKn6/79bbXjvpKcN5F7igX5Mqk2ncy/HPg4MgcJX2ia/+S826Tv/VblQLpQkv05iLPVv4zBJcsBp665BxVZ0oMi6xajFTupzskXnWQfIFJEfhKIkZTpNknTLPzmDvqzmVqhnCtxy/zYJLHtHIjBImTbnLfkZ7l96kpcyAQpzdBY4pJZEqsOL+/pVU/0qNPVFQM2MxeuzObmDNVxzIYeWWOTAqODLqzdrEKI6vo1I+aQfI8VpCr9K/896vHyin85gEYRcrWt3ZsKc3+1Be9mIkWcYXr0mNgNC2YKvgwkTOzrklKOSzBTZ2zhF547szo8EcetCZrJboGrmr2ImimhTbNMYWUTI1yFFD/Dd4GFQ/4IYWrGK8NolzcsXqOoSotn0BCy8gL21uw0faLv5iQEuMe7h5BO7OrJmERqrGEmP4Gmy2iIClpMsCYISjsxh/gtplFhxVCC16c9mOBRCdUV7OhAUwN8MJ/AieF2FoKqA16TTpKyUF+jB+6eL3QpVNtono0FeE98H5OnjwyF0ia3UedMxu67Qacs+6eZ5EDfYsN0ynLIzq4k1gR0SdBGNGngg69jsQXfGtyQng==

On 1/20/21 3:20 PM, Pierre-Marie Pédrot wrote:
As long as you only have an under-approximation in the sense that
forall x y, pointereq x y = true -> x = y

you should be safe, if you only care about soundness.
Except that the whole point of "pointereq" is that it doesn't respect definitional equality, so that a program could monitor all of its return values to detect counterexamples that imply contradictions, right?



Archive powered by MHonArc 2.6.19+.

Top of Page