Lean Kernel Arena / bugs/forged-quot-ind

Proof of False via a quotient induction principle declared before Quot and Quot.mk, which are then ordinary definitions.

The export declares, in this order:

1. a structure TightPair (A : Type) with two fields of type A;
2. a quotient declaration Quot.ind, with the type the real one has;
3. def Quot (A) (r) := TightPair A and def Quot.mk (r) (a) := ⟨a, a⟩;
4. theorem fakeQuotFalse : False.

Read with these definitions, Quot.ind says that a predicate holding for every pair ⟨a, a⟩ holds for every pair. At the predicate fun q => q.1 → q.2 and the pair ⟨True, False⟩ it gives True → False. The file has no axioms.

A checker that validates a quotient declaration by comparing its type with one built from the names Quot and Quot.mk, without requiring them to be the quotient primitives already in the environment, accepts it. The official kernel installs the quotient declarations together and rejects the file.

Nanoda, nanoclo and nanobruijn accepted this export. Found by a differential run of Pestka against other checkers.