From a5306e70ebbe672c73669e6376633eba6200fbb8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 24 Apr 2015 09:31:55 -0700 Subject: [PATCH] feat(library/logic/examples/negative): add example showing that allowing negative inductive datatypes would lead to inconsistency --- library/logic/examples/negative.lean | 30 ++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) create mode 100644 library/logic/examples/negative.lean diff --git a/library/logic/examples/negative.lean b/library/logic/examples/negative.lean new file mode 100644 index 0000000000..07da4775b6 --- /dev/null +++ b/library/logic/examples/negative.lean @@ -0,0 +1,30 @@ +/- +This example demonstrates why allowing types such as + +inductive D : Type := +| intro : (D → D) → D + +would make the system inconsistent +-/ + +/- If we were allowed to form the inductive type + + inductive D : Type := + | intro : (D → D) → D + + we would get the following +-/ +universe l +-- The new type A +axiom D : Type.{l} +-- The constructor +axiom introD : (D → D) → D +-- The eliminator +axiom recD : Π {C : D → Type}, (Π (f : D → D) (r : Π d, C (f d)), C (introD f)) → (Π (d : D), C d) +-- We would also get a computational rule for the eliminator, but we don't need it for deriving the inconsistency. + +definition id : D → D := λd, d +definition v : D := introD id + +theorem inconsistent : false := +recD (λ f ih, ih v) v