The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

On 06/24/2011 01:48 PM, Pierre Courtieu wrote:
> *Replacing* T by T_ax may be useful (for efficiency if T is slow to
> compile). It may seem unharmful however it may lead to inconsistencies
> if you prove new theorems after that. Even if these theorems are not
> about T itself. The reason is that the proof of T comes with universe
> constraints which guarantee the consistency of the global proof
> environment. Replacing T by T_ax would delete these constraints and
> make coq accept proofs that would be inconsistent with the real proof
> of T.
>
>    
I would not call that "inconsistency". You have proven "T", and then you 
can prove "T -> False" (by deriving a contradiction from a new 
assumption of type T). But you can't prove False because when you try to 
feed the latter proof with the former, you get a type error (universe 
inconsistency). This situation can happen only when T is a compound 
expression involving "Type", which is an ambiguous notation for "some 
universe" on which you can put constraints, only in an indirect manner.
This is not so different from, say, "nat=nat is not the same type as 
nat=nat", because nat=nat might mean (eq Set nat nat) or (eq Type nat 
nat) which are not the same type. In the latter case, it's easier to 
spot the difference.

If you want to see a concrete instance, check out
http://coq.inria.fr/pylons/pylons/contribs/view/Paradoxes/v8.3 and
http://coq.inria.fr/pylons/contribs/files/Paradoxes/v8.3/Paradoxes.BuraliForti.html
There you can derive False from 3 assumptions A0 i0 inj and you can 
build A0 i0 inj with the same apparent types, but in fact these two 
occurrences rely on incompatible sets of universe constraints. 
(Unfortunately, coqdoc removed the comments that explain what's going 
on, so you'd better download the contrib sources).

> An interesting question is: since in this case the potential
> inconsistency would not be a consequence of T but a consequence of the
> absence of the universe constraints of T, does this provide a way to
> build a proof H of False such that Print Assumptions H = \emptyset?
>    
This should not happen. As I said above, you could have a proof of T and 
a proof of ~T, without assumptions, when T contains Type, but not a 
single constant of type False without assumptions.

> Maybe someone who knows how Print Assumptions works can tell? If yes
> then this may be called a "fake proof that looks plausible to human
> forensics". However there *is* an axiom somewhere in the environment
> that should be detectable in some sense.
>    
Complex reasoning sometimes need complex tools, and complex tools might 
be dangerous for people who don't know how to use them. Universe 
ambiguity in Coq is definitely complex (and some people will complain 
it's not as powerful and usable as it could be).

Who can address this challenge: find a "simple" statement T (simple in 
the sense that anyone with a minimal background in logics can 
understand) such that you can prove both T and ~T in Coq.

Bruno.