The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi,

> If you want to avoid using axiom, I think you should really avoid using
> Type for proofs. In my experience, once you do this choice, either you
> decide to put everything in Type (thus giving up on impredicativity), or
> you have to use some sort of axiom of choice.
> 
> What is the actual reason justifying this choice ?

We have a partial order on a PCM-like structure defined the usual way

  a <= b := exists c, b = a * c

If you now, e.g., have a function "nat -> T" for some PCM T, and you
lift the PCM pointwise as usual, you obtain a relation on "nat -> T"
like this (after unfolding a little)

  f <= g := exists h, forall n, g n = f n * h n

but you really want this to hold:

  f <= g <-> forall n, f n <= g n

To prove this, as far as I can see, you either have to assume choice, or
you have to replace the "exists" in "<=" with a sigma type.

I managed to push this through our entire development ("<=" defined with
a sigma), but losing rewriting was rather annoying.

Kind regards,
Ralf