The Coq mailing list

[Emilio Jesús Gallego Arias <e AT x80.org>]

Hi Christopher,

Christopher Ernest Sally <christopherernestsally AT gmail.com> writes:

> 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?
>    Or am I left with declaring eq' x y:= fst x = fst y and then a whole
>    bunch of compat axioms, Morphisms etc?
>
>    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.

My reference setup when working with this kind of structures is to use
the `subType` pattern provided by the mathematical components library,
which is indeed applicable to any type of the shape:

{ x : T | P x } where P : T -> T -> bool [so irrelevance holds for free]

This provides reasonable support for both going to the base type, as
well as inferring the invariant for common operations [see for example
math-comp's tuple implementation]

For modular arithmetic, at least in the reasoning part, I find it easier
to work with the representation for ints used in math-comp again, which
re-defines the operations to be modular, then you can handle them using
the regular machinery for algebra.

Kind regards,
Emilio