249 lines
9.1 KiB
Text
249 lines
9.1 KiB
Text
-- False
|
||
|
||
def false : ★ := forall (A : ★), A;
|
||
|
||
-- no introduction rule
|
||
|
||
-- elimination rule
|
||
def false_elim (A : ★) (contra : false) : A := contra A;
|
||
|
||
-- --------------------------------------------------------------------------------------------------------------
|
||
|
||
-- True
|
||
|
||
def true : ★ := forall (A : ★), A → A;
|
||
|
||
def true_intro : true := [A : ★][x : A] x;
|
||
|
||
-- --------------------------------------------------------------------------------------------------------------
|
||
|
||
-- Negation
|
||
|
||
def not (A : ★) : ★ := A → false;
|
||
|
||
-- introduction rule (kinda just the definition)
|
||
def not_intro (A : ★) (h : A → false) : not A := h;
|
||
|
||
-- elimination rule
|
||
def not_elim (A B : ★) (a : A) (na : not A) : B := na a B;
|
||
|
||
-- can introduce double negation (can't eliminate it as that isn't constructive)
|
||
def double_neg_intro (A : ★) (a : A) : not (not A) :=
|
||
fun (notA : not A) => notA a;
|
||
|
||
-- --------------------------------------------------------------------------------------------------------------
|
||
|
||
-- Conjunction
|
||
|
||
def ∧ (A B : ★) : ★ := forall (C : ★), (A → B → C) → C;
|
||
infixl 10 ∧;
|
||
|
||
-- introduction rule
|
||
def and_intro (A B : ★) (a : A) (b : B) : A ∧ B :=
|
||
fun (C : ★) (H : A → B → C) => H a b;
|
||
|
||
-- left elimination rule
|
||
def and_elim_l (A B : ★) (ab : A ∧ B) : A :=
|
||
ab A (fun (a : A) (b : B) => a);
|
||
|
||
-- right elimination rule
|
||
def and_elim_r (A B : ★) (ab : A ∧ B) : B :=
|
||
ab B (fun (a : A) (b : B) => b);
|
||
|
||
-- --------------------------------------------------------------------------------------------------------------
|
||
|
||
-- Disjunction
|
||
|
||
-- 2nd order disjunction
|
||
def ∨ (A B : ★) : ★ := forall (C : ★), (A → C) → (B → C) → C;
|
||
infixl 5 ∨;
|
||
|
||
-- left introduction rule
|
||
def or_intro_l (A B : ★) (a : A) : A ∨ B :=
|
||
fun (C : ★) (ha : A → C) (hb : B → C) => ha a;
|
||
|
||
-- right introduction rule
|
||
def or_intro_r (A B : ★) (b : B) : A ∨ B :=
|
||
fun (C : ★) (ha : A → C) (hb : B → C) => hb b;
|
||
|
||
-- elimination rule (kinda just the definition)
|
||
def or_elim (A B C : ★) (ab : A ∨ B) (ha : A → C) (hb : B → C) : C :=
|
||
ab C ha hb;
|
||
|
||
-- --------------------------------------------------------------------------------------------------------------
|
||
|
||
-- Existential
|
||
|
||
-- 2nd order existential
|
||
def exists (A : ★) (P : A → ★) : ★ := forall (C : ★), (forall (x : A), P x → C) → C;
|
||
|
||
-- introduction rule
|
||
def exists_intro (A : ★) (P : A → ★) (a : A) (h : P a) : exists A P :=
|
||
fun (C : ★) (g : forall (x : A), P x → C) => g a h;
|
||
|
||
-- elimination rule (kinda just the definition)
|
||
def exists_elim (A B : ★) (P : A → ★) (ex_a : exists A P) (h : forall (a : A), P a → B) : B :=
|
||
ex_a B h;
|
||
|
||
-- --------------------------------------------------------------------------------------------------------------
|
||
|
||
-- Universal
|
||
|
||
-- 2nd order universal (just ∏, including it for completeness)
|
||
def all (A : ★) (P : A → ★) : ★ := forall (a : A), P a;
|
||
|
||
-- introduction rule
|
||
def all_intro (A : ★) (P : A → ★) (h : forall (a : A), P a) : all A P := h;
|
||
|
||
-- elimination rule
|
||
def all_elim (A : ★) (P : A → ★) (h_all : all A P) (a : A) : P a := h_all a;
|
||
|
||
-- --------------------------------------------------------------------------------------------------------------
|
||
|
||
-- Equality
|
||
|
||
-- 2nd order Leibniz equality
|
||
def eq (A : ★) (x y : A) := forall (P : A → ★), P x → P y;
|
||
|
||
-- equality is reflexive
|
||
def eq_refl (A : ★) (x : A) : eq A x x := fun (P : A → ★) (Hx : P x) => Hx;
|
||
|
||
-- equality is symmetric
|
||
def eq_sym (A : ★) (x y : A) (Hxy : eq A x y) : eq A y x := fun (P : A → ★) (Hy : P y) =>
|
||
Hxy (fun (z : A) => P z → P x) (fun (Hx : P x) => Hx) Hy;
|
||
|
||
-- equality is transitive
|
||
def eq_trans (A : ★) (x y z : A) (Hxy : eq A x y) (Hyz : eq A y z) : eq A x z := fun (P : A → ★) (Hx : P x) =>
|
||
Hyz P (Hxy P Hx);
|
||
|
||
-- equality is a universal congruence
|
||
def eq_cong (A B : ★) (x y : A) (f : A → B) (H : eq A x y) : eq B (f x) (f y) :=
|
||
fun (P : B → ★) (Hfx : P (f x)) =>
|
||
H (fun (a : A) => P (f a)) Hfx;
|
||
|
||
-- --------------------------------------------------------------------------------------------------------------
|
||
|
||
-- unique existence
|
||
def exists_uniq (A : ★) (P : A → ★) : ★ :=
|
||
exists A (fun (x : A) => P x ∧ (forall (y : A), P y → eq A x y));
|
||
|
||
def exists_uniq_elim (A B : ★) (P : A → ★) (ex_a : exists_uniq A P) (h : forall (a : A), P a → (forall (y : A), P y → eq A a y) → B) : B :=
|
||
exists_elim A B (fun (x : A) => P x ∧ (forall (y : A), P y → eq A x y)) ex_a
|
||
(fun (a : A) (h2 : P a ∧ (forall (y : A), P y → eq A a y)) =>
|
||
h a (and_elim_l (P a) (forall (y : A), P y → eq A a y) h2)
|
||
(and_elim_r (P a) (forall (y : A), P y → eq A a y) h2));
|
||
|
||
def exists_uniq_t (A : ★) : ★ :=
|
||
exists A (fun (x : A) => forall (y : A), eq A x y);
|
||
|
||
def exists_uniq_t_elim (A B : ★) (ex_a : exists_uniq_t A) (h : forall (a : A), (forall (y : A), eq A a y) → B) : B :=
|
||
exists_elim A B (fun (x : A) => forall (y : A), eq A x y) ex_a (fun (a : A) (h2 : forall (y : A), eq A a y) => h a h2);
|
||
|
||
-- --------------------------------------------------------------------------------------------------------------
|
||
|
||
-- Some logic theorems
|
||
|
||
section Theorems
|
||
|
||
variable (A B C : ★);
|
||
|
||
-- ~(A ∨ B) => ~A ∧ ~B
|
||
def de_morgan1 (h : not (A ∨ B)) : not A ∧ not B :=
|
||
and_intro (not A) (not B)
|
||
([a : A] h (or_intro_l A B a))
|
||
([b : B] h (or_intro_r A B b));
|
||
|
||
-- ~A ∧ ~B => ~(A ∨ B)
|
||
def de_morgan2 (h : not A ∧ not B) : not (A ∨ B) :=
|
||
fun (contra : A ∨ B) =>
|
||
or_elim A B false contra
|
||
(and_elim_l (not A) (not B) h)
|
||
(and_elim_r (not A) (not B) h);
|
||
|
||
-- ~A ∨ ~B => ~(A ∧ B)
|
||
def de_morgan3 (h : not A ∨ not B) : not (A ∧ B) :=
|
||
fun (contra : A ∧ B) =>
|
||
or_elim (not A) (not B) false h
|
||
(fun (na : not A) => na (and_elim_l A B contra))
|
||
(fun (nb : not B) => nb (and_elim_r A B contra));
|
||
|
||
-- the last one (~(A ∧ B) => ~A ∨ ~B) is not possible constructively
|
||
|
||
-- A ∧ B => B ∧ A
|
||
def and_comm (h : A ∧ B) : B ∧ A :=
|
||
and_intro B A
|
||
(and_elim_r A B h)
|
||
(and_elim_l A B h);
|
||
|
||
-- A ∨ B => B ∨ A
|
||
def or_comm (h : A ∨ B) : B ∨ A :=
|
||
or_elim A B (B ∨ A) h
|
||
([a : A] or_intro_r B A a)
|
||
([b : B] or_intro_l B A b);
|
||
|
||
-- A ∧ (B ∧ C) => (A ∧ B) ∧ C
|
||
def and_assoc_l (h : A ∧ (B ∧ C)) : (A ∧ B) ∧ C :=
|
||
let (a := (and_elim_l A (B ∧ C) h))
|
||
(bc := (and_elim_r A (B ∧ C) h))
|
||
(b := (and_elim_l B C bc))
|
||
(c := (and_elim_r B C bc))
|
||
in
|
||
and_intro (A ∧ B) C (and_intro A B a b) c
|
||
end;
|
||
|
||
-- (A ∧ B) ∧ C => A ∧ (B ∧ C)
|
||
def and_assoc_r (h : (A ∧ B) ∧ C) : A ∧ (B ∧ C) :=
|
||
let (ab := and_elim_l (A ∧ B) C h)
|
||
(a := and_elim_l A B ab)
|
||
(b := and_elim_r A B ab)
|
||
(c := and_elim_r (A ∧ B) C h)
|
||
in
|
||
and_intro A (B ∧ C) a (and_intro B C b c)
|
||
end;
|
||
|
||
-- A ∨ (B ∨ C) => (A ∨ B) ∨ C
|
||
def or_assoc_l (h : A ∨ (B ∨ C)) : (A ∨ B) ∨ C :=
|
||
or_elim A (B ∨ C) (A ∨ B ∨ C) h
|
||
(fun (a : A) => or_intro_l (A ∨ B) C (or_intro_l A B a))
|
||
(fun (g : B ∨ C) =>
|
||
or_elim B C (A ∨ B ∨ C) g
|
||
(fun (b : B) => or_intro_l (A ∨ B) C (or_intro_r A B b))
|
||
(fun (c : C) => or_intro_r (A ∨ B) C c));
|
||
|
||
-- (A ∨ B) ∨ C => A ∨ (B ∨ C)
|
||
def or_assoc_r (h : (A ∨ B) ∨ C) : A ∨ (B ∨ C) :=
|
||
or_elim (A ∨ B) C (A ∨ (B ∨ C)) h
|
||
(fun (g : A ∨ B) =>
|
||
or_elim A B (A ∨ (B ∨ C)) g
|
||
(fun (a : A) => or_intro_l A (B ∨ C) a)
|
||
(fun (b : B) => or_intro_r A (B ∨ C) (or_intro_l B C b)))
|
||
(fun (c : C) => or_intro_r A (B ∨ C) (or_intro_r B C c));
|
||
|
||
-- A ∧ (B ∨ C) => A ∧ B ∨ A ∧ C
|
||
def and_distrib_l_or (h : A ∧ (B ∨ C)) : A ∧ B ∨ A ∧ C :=
|
||
or_elim B C (A ∧ B ∨ A ∧ C) (and_elim_r A (B ∨ C) h)
|
||
(fun (b : B) => or_intro_l (A ∧ B) (A ∧ C)
|
||
(and_intro A B (and_elim_l A (B ∨ C) h) b))
|
||
(fun (c : C) => or_intro_r (A ∧ B) (A ∧ C)
|
||
(and_intro A C (and_elim_l A (B ∨ C) h) c));
|
||
|
||
-- A ∧ B ∨ A ∧ C => A ∧ (B ∨ C)
|
||
def and_factor_l_or (h : A ∧ B ∨ A ∧ C) : A ∧ (B ∨ C) :=
|
||
or_elim (A ∧ B) (A ∧ C) (A ∧ (B ∨ C)) h
|
||
(fun (ab : A ∧ B) => and_intro A (B ∨ C)
|
||
(and_elim_l A B ab)
|
||
(or_intro_l B C (and_elim_r A B ab)))
|
||
(fun (ac : A ∧ C) => and_intro A (B ∨ C)
|
||
(and_elim_l A C ac)
|
||
(or_intro_r B C (and_elim_r A C ac)));
|
||
|
||
-- Thanks Quinn!
|
||
-- A ∨ B => ~B => A
|
||
def disj_syllog (nb : not B) (hor : A ∨ B) : A :=
|
||
or_elim A B A hor ([a : A] a) ([b : B] nb b A);
|
||
|
||
-- (A => B) => ~B => ~A
|
||
def contrapositive (f : A → B) (nb : not B) : not A :=
|
||
fun (a : A) => nb (f a);
|
||
|
||
end Theorems
|