coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Rewriting/Morphism/Partial Point-wise equality

From: Christopher Ernest Sally <christopherernestsally AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Rewriting/Morphism/Partial Point-wise equality
Date: Thu, 6 May 2021 08:34:02 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=christopherernestsally AT gmail.com; spf=Pass smtp.mailfrom=christopherernestsally AT gmail.com; spf=None smtp.helo=postmaster AT mail-io1-f54.google.com
Ironport-hdrordr: A9a23:FO+Fh6BTPnY3NWblHemh55DYdb4zR+YMi2TDtnoBLiC9F/bzqynApoV56faZslYssRIb+OxoWpPwI080nKQdieIs1NyZLWzbUQWTXeVfBEjZrwEI2ReSygeQ78hdmmFFZuHNMQ==
Ironport-phdr: A9a23:tcMGJBMaJerTYq8FaREl6nagDRdPi9zP1u491JMrhvp0f7i5+Ny6ZQqDvKQr1gORFtmEo9t/yMPu+5j6XmIB5ZvT+FsjS7drEyE/tMMNggY7C9SEA0CoZNTjbig9AdgQHAQ9pyLzPkdaAtvxaEPPqXOu8zESBg//NQ1oLejpB4Lelcu62/229pHJfQlFiyaxbbx9IRi0sA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KODE5/m/ZicJ+kbxVrw66qhNl34LZepuYOOZicq7fe94RWGpPXtxWVyxEGo6xcYsPD/AAPeZDs4n9oEMOrRugCgm2GejhxSVIhnno0q0hz+QqDBzI0xYkH9IKsHXfsdL4O7sSUeCvzanI1inDb/RO2Tf99ofIaA4uoeuKXb1uasrR1VIvGBnBjlWUqY3oJDyV1uEXvGia6+psT/6gi2kiqwxopDWk28gjhJXTiI0P1lDE6Tt2wJwzJdCgVkJ3f9+pHIZMuiybKoZ7X8cvTm9ptSs1zrALu5C1cSsUxZklxxDSaf6KfoiK7x7+V+ucPyp0iGx7db+7hRu//06twfD/WMmsyFtGsDZJn93Wun0O1xHf8NWLR/p880u72TuC2Abe4fxeL08uj6rUMZshz6YwlpUNtUTDGTf7mEDsg6+XckUo4+mo6+P6brn/qJ+RN4B5hhvxMqQpncy/DuA4PRYUU2eH/uS80aXv/Uz/QLpUkv07irfVvIzeKMgBpaO0AxVZ3psi5hu+FTur0NsVkWECLF1feRKHi4bpO0vJIPD9Ffqwn1SskC1qx/DdIr3hBY3NLnjdn7f7Y7l98UhcxxQozdBD/JJbELUBIPbzW0Lqu9zYCwU2Mw2ww+r9FNp90YYeVXqVAqCFKKPSrUOI5uU3LuaQY48VoS/xJOQh5/7zlnA0gkQdfKms3ZsPcn+0BPVmI0ODYXrtmNgNC2kKvhBtBNDt3VaFSHtYY2u4F/Y34Sh+A4a7B6/CQJqsifqPxnHoMIdRYzVtCkqNCmvvb4WJQb8hciSfOdMpqTUAUanpH4QhzxC1qAjiy7d9I/DS9zYErpvn0Mld6OjalBV0/jtxWZfOm1qRRn15yztbDwQ927py9BQVIrar1KF5h7lZEoUW6a4VFAg9MpHYwqpxDNWgAmopkf+GTV+nRpOtBjRjF7rZJvcBZk98H5OpiRWRh0KX

Hi Club

In a dev, I'm working with a common representation of fixed width integers, i.e. int := (Z, <a proof that the Z is in some bound>).

When doing arithmetic over the Z, I want to ignore the proof (and having proof irrelevance is fine for the dev).

I have 2 questions

Is there an easy / already-common way to set the dev up for this?
Or am I left with declaring eq' x y:= fst x = fst y and then a whole bunch of compat axioms, Morphisms etc?
A more general problem I have is when working with functions that return an in, (e.g. f x = y) I obviously have Logic.eq, and when rewriting with such equalities, I sometimes get a goal where I'm trying to prove Logic.eq x y from a eq' x y hypothesis. Is there a general fix for this? from both a mathematical and Coq (mechanisms) perspective.

[Coq-Club] Rewriting/Morphism/Partial Point-wise equality, Christopher Ernest Sally, 05/06/2021
- Re: [Coq-Club] Rewriting/Morphism/Partial Point-wise equality, Xavier Leroy, 05/06/2021
  - Re: [Coq-Club] Rewriting/Morphism/Partial Point-wise equality, Christopher Ernest Sally, 05/08/2021
- Re: [Coq-Club] Rewriting/Morphism/Partial Point-wise equality, Emilio Jesús Gallego Arias, 05/06/2021