The Coq mailing list

[Georgi Guninski <guninski AT guninski.com>]

On Mon, May 30, 2011 at 07:51:47AM -0700, Brandon Moore wrote:
> I don't see the point. If you are worried about people playing syntactic 
> games,
> examine the statement with notations and coercions turned off. You
> might as well say you have a "contradiction" because you can write
> 
> Notation "'Truth'" := False.
> 
> Lemma contradiction : Truth -> False. auto. Qed.
> 
> "t" isn't a sort, so it's obvious your goal won't typecheck without
> coercions. Displaying coercions, you have
> 
> exists a : t, exp2 a -> False.
> 
> We see exp2 = (fun _ => False), so this should be equivalent to
> exists a : t, (fun _ => False) a -> False.
> 
> Unfolding exp2 gives
> 
> ex _ (fun _ : True => False -> False).
> 
> And there's nothing wrong with being able to prove that.
> 
> Brandon

i asked how to check for cheating proofs.

Bruno (appears a coq developer) replied:
https://sympa-roc.inria.fr/wws/arc/coq-club/2011-05/msg00101.html?checked_cas=2

how a client should check a Coq proof for cheating?

If I were the client I would disable all customized notations with
Unset Printing All.  
^ Bruno wrote this.

so i follow his advice:

Coq < Require Import b.
Ambiguous paths:
[b.expr2] : b.type >-> Sortclass

Coq < Unset Printing All.

Coq < Check a1.
a1
     : FUCKMS

Coq < Check a2.
a2
     : FUCKMS -> False

all of a sudden, coqtop doesn't see a contradiction, possibly due to
what coq fanboys call "Anomaly" in your source. 

the error message coqtop gives is borderline insane "X is not X" (or sthg 
very close to this).

which parts of coq should i trust?