From 15c331591e36334c1bfcb9a3645d92a51124729e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 24 Apr 2015 09:20:44 -0700
Subject: [PATCH] feat(library/logic/examples/colog88): add example from
 COLOG-88 paper

---
 library/logic/examples/colog88.lean | 92 +++++++++++++++++++++++++++++
 1 file changed, 92 insertions(+)
 create mode 100644 library/logic/examples/colog88.lean

diff --git a/library/logic/examples/colog88.lean b/library/logic/examples/colog88.lean
new file mode 100644
index 000000000..f1cc73238
--- /dev/null
+++ b/library/logic/examples/colog88.lean
@@ -0,0 +1,92 @@
+/-
+Example from "Inductively defined types",
+from Thierry Coquand and Christine Paulin,
+COLOG-88.
+
+It shows it is inconsistent to allow inductive datatypes such as
+
+inductive A : Type :=
+| intro : ((A → Prop) → Prop) → A
+
+-/
+
+/- Phi is a positive, but not strictly positive, operator. -/
+definition Phi (A : Type) := (A → Prop) → Prop
+
+/- If we were allowed to form the inductive type
+
+     inductive A: Type :=
+     | introA : Phi A -> A
+
+   we would get the following
+-/
+
+universe l
+-- The new type A
+axiom A : Type.{l}
+-- The constructor
+axiom introA : Phi A → A
+-- The eliminator
+axiom recA   : Π {C : A → Type}, (Π (p : Phi A), C (introA p)) → (Π (a : A), C a)
+-- The "computational rule"
+axiom recA_comp : Π {C : A → Type} (H : Π (p : Phi A), C (introA p)) (p : Phi A), recA H (introA p) = H p
+
+-- The recursor could be used to define matchA
+definition matchA (a : A) : Phi A :=
+recA (λ p, p) a
+
+-- and the computation rule would allows us to define
+lemma betaA (p : Phi A) : matchA (introA p) = p :=
+!recA_comp
+
+-- As in all inductive datatypes, we would be able to prove that constructors are injective.
+lemma introA_injective : ∀ {p p' : Phi A}, introA p = introA p' → p = p' :=
+λ p p' h,
+  assert aux : matchA (introA p) = matchA (introA p'), by rewrite h,
+  by rewrite [*betaA at aux]; exact aux
+
+-- For any type T, there is an injection from T to (T → Prop)
+definition i {T : Type} : T → (T → Prop) :=
+λ x y, x = y
+
+lemma i_injective {T : Type} {a b : T} : i a = i b → a = b :=
+λ h,
+  have e₁ : i a a = i b a,     by rewrite [h],
+  have e₂ : (a = a) = (b = a), from e₁,
+  have e₃ : b = a,             from eq.subst e₂ rfl,
+  eq.symm e₃
+
+-- Hence, by composition, we get an injection f from (A → Prop) to A
+definition f : (A → Prop) → A :=
+λ p, introA (i p)
+
+lemma f_injective : ∀ {p p' : A → Prop}, f p = f p' → p = p':=
+λ (p p' : A → Prop) (h : introA (i p) = introA (i p')),
+  i_injective (introA_injective h)
+
+/-
+  We are now back to the usual Cantor-Russel paradox.
+  We can define
+-/
+definition P0 (a : A) : Prop :=
+∃ (P : A → Prop), f P = a ∧ ¬ P a
+-- i.e., P0 a := codes a set P such that x∉P
+
+definition x0 : A := f P0
+
+lemma fP0_eq : f P0 = x0 :=
+rfl
+
+lemma not_P0_x0 : ¬ P0 x0 :=
+λ h : P0 x0,
+  obtain (P : A → Prop) (hp : f P = x0 ∧ ¬ P x0), from h,
+  have   fp_eq : f P = f P0,  from and.elim_left hp,
+  assert p_eq  : P = P0,      from f_injective fp_eq,
+  have   nh    : ¬ P0 x0,     by rewrite [p_eq at hp]; exact (and.elim_right hp),
+  absurd h nh
+
+lemma P0_x0 : P0 x0 :=
+exists.intro P0 (and.intro fP0_eq not_P0_x0)
+
+theorem inconsistent : false :=
+absurd @P0_x0 @not_P0_x0