(* from Bart Jacobs (Leuven), The Essence of Coq as a Formal System*) (* based on a proof by Paolo Capriotti *) (* to make coq accept it, use the -type-in-type option *) (* otherwise coq will qualm about the def of spec *) (* to see why Display universe levels *) Inductive And(P Q: Type) := and_(p: P)(q: Q). Inductive Exists(T: Type)(P: T -> Type) := exists_(t: T)(p: P t). Inductive Equals(A: Type)(a: A): A -> Type := equals_: Equals A a a. Inductive False :=. Definition Not(P: Type) := P -> False. Inductive U := set(J: Type)(P: J -> Type)(f: J -> U). Definition In(x X: U): Type := match X with set J P f => Exists J (fun i => And (P i) (Equals U (f i) x)) end. Definition id(x: U): U := x. Definition spec(P: U -> Type): U := set U P id. Definition spec_intro(P: U -> Type)(x: U)(H: P x): In x (spec P) := exists_ U (fun (i: U) => And (P i) (Equals U (id i) x)) x (and_ (P x) (Equals U (id x) x) H (equals_ U (id x))). Definition spec_elim(P: U -> Type)(x: U)(H: In x (spec P)): P x := match H with exists_ _ _ i H0 => match H0 with and_ _ _ H1 H2 => match H2 in Equals _ _ X return P X with equals_ _ _ => H1 end end end. Definition PR(x: U): Type := Not (In x x). Definition R: U := spec PR. Check (spec_intro PR). (* P -> Not P, for P = In R R *) Check (spec_elim PR R). (* Not P -> P, for P = In R R *) Definition contradiction(P: Type)(H1: Not P -> P)(H2: P -> Not P): False := (fun (H3: Not P) => H3 (H1 H3)) (fun (HP: P) => H2 HP HP). Definition absurd: False := contradiction (In R R) (spec_intro PR R) (spec_elim PR R). Theorem omnipotence : 4 = 3. Proof. apply False_ind. apply absurd. Qed.