The Coq mailing list

[Georgi Guninski <guninski AT guninski.com>]

On Fri, Jun 24, 2011 at 03:03:38PM +0200, Bruno Barras wrote:
> 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.
>

i am somewhat surprised why you don't print False->stuff here:

Section S.
Lemma T : Prop.
exact False.
Defined.

Variable VAR : T.

Lemma L_2: exists a : T, a = VAR.
eexists. instantiate (1:=VAR). reflexivity.
Defined.


Lemma L_1: ~(exists a : T, a = VAR).

change ((exists a : T, a = VAR) -> False); intro H; refine (ex_ind _ H);
       clear H; intro x; intro H; auto with *.
Defined.

End S.