-- 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 : ★) : ★ := A × B;
infixl 10 ∧;

-- introduction rule
def and_intro (A B : ★) (a : A) (b : B) : A ∧ B := (a, b);

-- left elimination rule
def and_elim_l (A B : ★) (ab : A ∧ B) : A := π₁ ab;

-- right elimination rule
def and_elim_r (A B : ★) (ab : A ∧ B) : B := π₂ ab;

-- --------------------------------------------------------------------------------------------------------------

-- 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 :=
        ( [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 (π₁ h) (π₂ 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 (π₁ contra))
                (fun (nb : not B) => nb (π₂ contra));

    -- the last one (~(A ∧ B) => ~A ∨ ~B) is not possible constructively

    -- A ∧ B => B ∧ A
    def and_comm (h : A ∧ B) : B ∧ A := (π₂ h, π₁ 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 :=
        ((π₁ h, π₁ (π₂ h)), π₂ (π₂ h));

    -- (A ∧ B) ∧ C => A ∧ (B ∧ C)
    def and_assoc_r (h : (A ∧ B) ∧ C) : A ∧ (B ∧ C) :=
        (π₁ (π₁ h), (π₂ (π₁ h), π₂ h));

    -- 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) (π₂ h)
            (fun (b : B) => or_intro_l (A ∧ B) (A ∧ C) (π₁ h, b))
            (fun (c : C) => or_intro_r (A ∧ B) (A ∧ 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) => (π₁ ab, or_intro_l B C (π₂ ab)))
            (fun (ac : A ∧ C) => (π₁ ac, or_intro_r B 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