The Coq mailing list

[Christopher Ernest Sally <christopherernestsally AT gmail.com>]

Thanks for the tips!

On Thu, 6 May 2021 at 23:46, Xavier Leroy <Xavier.Leroy AT inria.fr> wrote:

On Thu, May 6, 2021 at 6:02 PM Christopher Ernest Sally <christopherernestsally AT gmail.com> wrote:

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

1. Is there an easy / already-common way to set the dev up for this?
   

You can look at CompCert's Integers module, it follows exactly this approach: https://github.com/AbsInt/CompCert/blob/master/lib/Integers.v

1. Or am I left with declaring eq' x y:= fst x = fst y and then a whole bunch of compat axioms, Morphisms etc?
   

No, because

        forall (x y: {n : Z | P n}), proj1_sig x = proj1_sig y -> x = y

if you assume proof irrelevance or if you define P such that proofs of P n are unique.

So, your eq' implies Logic.eq, and you don't need setoids, morphisms, etc.

 Hope this helps,

- Xavier Leroy

1. 
   
2. 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.