Lindenbaum.lean

import Mathlib
-- 相対パスはローカル環境のまま、使うなら適宜変更を
import Topology.TopologyAndLogic.ch2_proposition.Logic

instance {var : Type _} : Preorder (form var) where
  le φ ψ := Deduction ∅ (φ.Imp ψ)
  le_refl φ := by
    apply Deduction.imp_intro
    apply Deduction.AX; simp
  le_trans {φ ψ χ} h1 h2 := by
    apply Deduction.HS h1 h2


def Deduction.setoid {var : Type _} : Setoid (form var) where
  r φ ψ := φ ≤ ψ ∧ ψ ≤ φ
    -- Deduction ∅ (φ.Imp ψ) ∧ Deduction ∅ (ψ.Imp φ)
  iseqv := {
    refl φ := by simp
    symm {φ ψ} h := by
      rw [And.comm]; assumption
    trans {φ ψ χ} h1 h2 := by
      rcases h1 with ⟨Hl1, Hl2⟩
      rcases h2 with ⟨Hr1, Hr2⟩
      constructor<;> grind
  }

def Lindenbaum (var : Type _) := Quotient (Deduction.setoid : Setoid (form var))

instance {var} : Preorder (Lindenbaum var)
where
  le x y := by
    apply Quotient.liftOn₂ x y (fun φ ψ => φ ≤ ψ)
    intro φ1 φ2 ψ1 ψ2 ⟨Hl1, Hr1⟩ ⟨Hl2, Hr2⟩
    apply propext; constructor<;> intro H
    · apply le_trans Hr1
      apply le_trans H Hl2
    · apply le_trans Hl1
      apply le_trans H Hr2
  le_refl x := by
    rw [<- Quotient.out_eq x, Quotient.liftOn₂_mk]
  le_trans a b c:= by
    rw [<- Quotient.out_eq a, <- Quotient.out_eq b, <- Quotient.out_eq c, Quotient.liftOn₂_mk, Quotient.liftOn₂_mk, Quotient.liftOn₂_mk]
    intro H1 H2; grind

open Deduction

instance {var} : PartialOrder (Lindenbaum var)
:= by
  apply PartialOrder.mk
  intro x y H1 H2
  rw [<- Quotient.out_eq x, <- Quotient.out_eq y] at ⊢ H1 H2
  apply Quotient.sound
  exact ⟨H1, H2⟩

instance {var} : SemilatticeSup (Lindenbaum var)
where
  sup x y := by
    apply Quotient.liftOn₂ x y (fun φ ψ => ⟦φ.Or ψ⟧)
    intro φ1 φ2 ψ1 ψ2 ⟨Hl1, Hr1⟩ ⟨Hl2, Hr2⟩
    apply Quotient.sound
    constructor
    · apply Deduction.MP (φ1.Imp (ψ1.Or ψ2)); swap
      · apply Deduction.imp_intro; simp
        apply MP ψ1; swap
        · have E : {φ1} = insert φ1 (∅ : Set (form var)) := by simp
          rw [E]; clear E
          apply imp_elim
          exact Hl1
        · apply weakening (Γ := ∅); simp
          apply Deduction.imp_intro; simp
          apply or_intro_left
      · apply Deduction.imp_intro; simp
        apply MP (φ2.Imp (ψ1.Or ψ2)); swap
        · apply weakening (Γ := ∅); simp
          apply Deduction.imp_intro; simp
          apply MP ψ2; swap
          · have E : {φ2} = insert φ2 (∅ : Set (form var)) := by simp
            rw [E]; clear E
            apply imp_elim
            exact Hl2
          · apply weakening (Γ := ∅); simp
            apply Deduction.imp_intro; simp
            apply or_intro_right
        · apply Deduction.imp_intro
          have E : {φ2.Imp (ψ1.Or ψ2), φ1.Imp (ψ1.Or ψ2)} = ({φ1.Imp (ψ1.Or ψ2), φ2.Imp (ψ1.Or ψ2)} : Set (form var)) := by ext x; simp; grind
          rw [E]; clear E
          apply or_imp_intro
    · apply MP (ψ2.Imp (φ1.Or φ2)); swap
      · apply Deduction.imp_intro; simp
        apply MP φ2; swap
        · have E : {ψ2} = insert ψ2 (∅ : Set (form var)) := by simp
          rw [E]; clear E
          apply imp_elim
          exact Hr2
        · apply weakening (Γ := ∅); simp
          apply Deduction.imp_intro; simp
          apply or_intro_right
      · apply Deduction.imp_intro; simp
        apply MP (ψ1.Imp (φ1.Or φ2)); swap
        · apply weakening (Γ := ∅); simp
          apply Deduction.imp_intro; simp
          apply MP φ1; swap
          · have E : {ψ1} = insert ψ1 (∅ : Set (form var)) := by simp
            rw [E]; clear E
            apply imp_elim
            exact Hr1
          · apply weakening (Γ := ∅); simp
            apply Deduction.imp_intro; simp
            apply or_intro_left
        · apply Deduction.imp_intro
          apply or_imp_intro
  le_sup_left x y := by
    rw [<- Quotient.out_eq x, <- Quotient.out_eq y, Quotient.liftOn₂_mk]
    change Quotient.out x ≤ (Quotient.out x).Or (Quotient.out y)
    apply Deduction.imp_intro; simp
    apply or_intro_left
  le_sup_right x y := by
    rw [<- Quotient.out_eq x, <- Quotient.out_eq y, Quotient.liftOn₂_mk]
    change Quotient.out y ≤ (Quotient.out x).Or (Quotient.out y)
    apply Deduction.imp_intro; simp
    apply or_intro_right
  sup_le {x y z} := by
    rw [<- Quotient.out_eq x, <- Quotient.out_eq y, <- Quotient.out_eq z, Quotient.liftOn₂_mk]
    set X := x.out
    set Y := y.out
    set Z := z.out
    intro (H1 : X ≤ Z) (H2 : Y ≤ Z)
    change X.Or Y ≤ Z
    apply MP; swap; exact H1
    apply MP; swap; exact H2
    apply Deduction.imp_intro; apply Deduction.imp_intro; simp
    apply or_imp_intro


instance {var} : Lattice (Lindenbaum var)
where
  inf x y := by
    apply Quotient.liftOn₂ x y (fun φ ψ => ⟦φ.And ψ⟧)
    intro φ1 φ2 ψ1 ψ2 ⟨Hl1, Hr1⟩ ⟨Hl2, Hr2⟩
    apply Quotient.sound
    constructor
    · apply Deduction.imp_intro; simp
      apply MP ψ1; swap
      · apply MP φ1; swap
        · have E :  ({φ1.And φ2} : Set (form var)) = insert (φ1.And φ2) ∅ := by simp
          rw [E]; clear E
          apply imp_elim; apply and_elim_left
        · apply weakening (Γ := ∅); simp
          exact Hl1
      · apply MP ψ2; swap
        · apply MP φ2
          · apply weakening (Γ := ∅); simp
            exact Hl2
          · have E : ({φ1.And φ2} : Set (form var)) = insert (φ1.And φ2) ∅ := by ext; simp
            rw [E]; clear E
            apply imp_elim; apply and_elim_right
        · apply weakening (Γ := ∅); simp
          apply Deduction.imp_intro; apply Deduction.imp_intro; simp
          apply and_intro
    · apply Deduction.imp_intro; simp
      apply MP φ1; swap
      · apply MP ψ1; swap
        · have E : ({ψ1.And ψ2} : Set (form var)) = insert (ψ1.And ψ2) ∅ := by simp
          rw [E]; clear E
          apply imp_elim; apply and_elim_left
        · apply weakening (Γ := ∅); simp
          exact Hr1
      · apply MP φ2; swap
        · apply MP ψ2; swap
          · have E : ({ψ1.And ψ2} : Set (form var)) = insert (ψ1.And ψ2) ∅ := by simp
            rw [E]; clear E
            apply imp_elim; apply and_elim_right
          · apply weakening (Γ := ∅); simp
            exact Hr2
        · apply weakening (Γ := ∅); simp
          apply Deduction.imp_intro; apply Deduction.imp_intro; simp
          apply and_intro
  inf_le_left x y := by
    rw [<- Quotient.out_eq x, <- Quotient.out_eq y, Quotient.liftOn₂_mk]
    set X := x.out
    set Y := y.out
    change X.And Y ≤ X
    apply and_elim_left
  inf_le_right x y := by
    rw [<- Quotient.out_eq x, <- Quotient.out_eq y, Quotient.liftOn₂_mk]
    set X := x.out
    set Y := y.out
    change X.And Y ≤ Y
    apply and_elim_right
  le_inf {x y z} := by
    rw [<- Quotient.out_eq x, <- Quotient.out_eq y, <- Quotient.out_eq z, Quotient.liftOn₂_mk]
    set X := x.out
    set Y := y.out
    set Z := z.out
    intro (H1 : X ≤ Y) (H2 : X ≤ Z)
    change X ≤ Y.And Z
    apply MP (X.Imp Y); swap; exact H1
    apply MP (X.Imp Z); swap; exact H2
    apply Deduction.imp_intro; apply Deduction.imp_intro; simp
    apply imp_and_intro

instance {var} : DistribLattice (Lindenbaum var)
where
  le_sup_inf x y z := by
    suffices H : ∀ (a b c : Lindenbaum var), a ⊓ (b ⊔ c) ≤ (a ⊓ b) ⊔ (a ⊓ c)
    · have H1 := H (x ⊔ y) x z
      apply le_trans H1
      rw [inf_comm _ x, inf_sup_self]
      apply sup_le le_sup_left
      rw [inf_comm _ z]
      have H2 := H z x y
      apply le_trans H2
      rw [inf_comm y z]
      apply sup_le _ le_sup_right
      apply le_trans inf_le_right le_sup_left
    · intro a b c
      rw [<- Quotient.out_eq a, <- Quotient.out_eq b, <- Quotient.out_eq c]
      set A := a.out
      set B := b.out
      set C := c.out
      change A.And (B.Or C) ≤ (A.And B).Or (A.And C)
      apply Deduction.imp_intro; simp
      apply Deduction.and_or_left

instance {var} : BooleanAlgebra (Lindenbaum var)
where
  compl x := by
    apply Quotient.liftOn x  (fun x => ⟦x.Not⟧)
    intro x y ⟨xy, yx⟩
    apply Quotient.sound
    constructor<;> apply MP<;> try apply contra
    · assumption
    · assumption
  bot := ⟦form.Bot⟧
  top := ⟦form.Bot.Not⟧
  bot_le x := by
    rw [<- Quotient.out_eq x]
    change form.Bot ≤ x.out
    apply MP; apply exfalso_left
    apply Deduction.Top
  le_top x := by
    rw [<- Quotient.out_eq x]
    change x.out ≤ form.Bot.Not
    apply Deduction.imp_intro; simp
    apply weakening (Γ := ∅); simp
    apply Deduction.Top
  inf_compl_le_bot x := by
    rw [<- Quotient.out_eq x, Quotient.liftOn_mk]
    change x.out.And x.out.Not ≤ form.Bot
    set X := x.out
    apply MP
    apply exfalso_left
    apply Deduction.and_not
  top_le_sup_compl x := by
    rw [<- Quotient.out_eq x, Quotient.liftOn_mk]
    set X := x.out
    change form.Bot.Not ≤ X.Or X.Not
    apply Deduction.imp_intro; simp
    apply weakening (Γ := ∅); simp
    apply Deduction.or_not

Logic.lean

import Mathlib


/-------
- form -
-------/

inductive form (var : Type _) where
  | Bot : form var
  | Var : var → form var
  | Not : form var → form var
  | Imp : form var → form var → form var


def form.Or {var : Type _} (φ ψ : form var):= Imp (Not φ) ψ
def form.And {var : Type _} (φ ψ : form var):= Not (Imp φ (Not ψ))

@[simp]
def form.valuation {var} (v : var → Bool) : form var → Bool
  | .Bot => false
  | .Var x => v x
  | .Not φ => (valuation v φ)ᶜ
  | .Imp φ ψ => (valuation v φ) ⇨ (valuation v ψ)

/------------
- valuation -
-------------/

def form.valuation_or {var} (v : var → Bool) (φ ψ : form var) :
  valuation v (φ.Or ψ) = (valuation v φ) ⊔ (valuation v ψ)
:= by
  simp [Or, himp]
  rw [Bool.or_comm]

@[simp]
lemma form.valuation_and {var} (v : var → Bool) (φ ψ : form var) :
  valuation v (φ.And ψ) = (valuation v φ) ⊓ (valuation v ψ)
:= by
  simp [And, valuation, sdiff]


/------------
- tautology -
------------/

def form.isTautology {var} (φ : form var) : Prop :=
  ∀ v : var → Bool, form.valuation v φ = true



/---------
- Provable -
----------/

inductive Deduction {var : Type _} (Γ : Set (form var)) : form var → Prop where
  | AX φ : φ ∈ Γ → Deduction Γ φ
  -- φ → ψ → φ
  | L1 (φ ψ : form var) :
    Deduction Γ (φ.Imp (ψ.Imp φ))
  -- (φ → (ψ → χ)) → ((φ → ψ) → (φ → χ))
  | L2 (φ ψ χ : form var) :
    Deduction Γ ((φ.Imp (ψ.Imp χ)).Imp ((φ.Imp ψ).Imp (φ.Imp χ)))
  -- (¬φ → ¬ψ) → (ψ → φ)
  | L3 (φ ψ : form var) :
    Deduction Γ (((φ.Not).Imp (ψ.Not)).Imp (ψ.Imp φ))
  | MP (φ ψ : form var) :
    Deduction Γ (φ.Imp ψ) → Deduction Γ φ → Deduction Γ ψ
  | Top : Deduction Γ (form.Bot.Not) --- ???

inductive Provable {var : Type _} : form var → Prop where
  | L1 (φ ψ : form var) :
    Provable (φ.Imp (ψ.Imp φ))
  | L2 (φ ψ χ : form var) :
    Provable ((φ.Imp (ψ.Imp χ)).Imp ((φ.Imp ψ).Imp (φ.Imp χ)))
  | L3 (φ ψ : form var) :
    Provable (((φ.Not).Imp (ψ.Not)).Imp (ψ.Imp φ))
  | MP (φ ψ : form var) :
    Provable (φ.Imp ψ) → Provable φ → Provable ψ
  | Top : Provable (form.Bot.Not) --- ???

lemma Deduction_Provable {var}  {φ : form var} :
  Deduction ∅ φ ↔ Provable φ
:= by
  constructor<;> intro H
  · induction H; contradiction
    · apply Provable.L1
    · apply Provable.L2
    · apply Provable.L3
    · case mp.MP s t Hs Ht IHs IHt =>
        apply Provable.MP; assumption; assumption
    · apply Provable.Top
  · induction H
    · apply Deduction.L1
    · apply Deduction.L2
    · apply Deduction.L3
    · case mpr.MP s t Hs Ht IHs IHt =>
        apply Deduction.MP; assumption; assumption
    · apply Deduction.Top







lemma soundness {var} (φ : form var) :
  Provable φ → φ.isTautology
:= by
  intro H
  induction H with
  | L1 φ ψ =>
    intro v
    rcases φ<;> simp [himp]
    case Var a => cases v a<;> simp
    case Not φ => rcases form.valuation v φ<;> simp
    case Imp φ₁ φ₂ => rcases form.valuation v φ₁<;> rcases form.valuation v φ₂<;> simp
  | L2 φ ψ χ =>
    intro v
    rcases φ<;> simp [himp]
    case Var a =>
      cases v a<;> simp
      rcases form.valuation v ψ<;> simp
    case Not φ =>
      rcases form.valuation v φ<;> simp
      rcases form.valuation v ψ<;> simp
    case Imp φ₁ φ₂ =>
      rcases form.valuation v φ₁<;>
      rcases form.valuation v φ₂<;>
      rcases form.valuation v ψ<;> simp
  | L3 φ ψ =>
    intro v
    rcases φ<;> simp [himp]
    case Var a =>
      rcases form.valuation v ψ<;> simp
    case Not φ =>
      rcases form.valuation v φ<;>
      rcases form.valuation v ψ<;> simp
    case Imp φ₁ φ₂ =>
      rcases form.valuation v φ₁<;>
      rcases form.valuation v φ₂<;>
      rcases form.valuation v ψ<;> simp
  | MP φ ψ H1 H2 IH1 IH2 =>
    intro v
    have IH1' := IH1 v
    have IH2' := IH2 v
    simp [himp] at IH1'
    revert IH1' IH2'
    rcases form.valuation v φ<;> rcases form.valuation v ψ
    <;> intro IH1 IH2<;> rcases IH2<;> try simp<;> contradiction
  | Top =>
    intro v; simp



lemma form.imp_self_provable {var} (φ : form var) :
  Provable (φ.Imp φ)
:= by
  have H1 := Provable.L2 φ (φ.Imp φ) φ
  have H2 := Provable.L1 φ (φ.Imp φ)
  have H3 :=  Provable.MP _ _ H1 H2
  have H4 := Provable.L1 φ φ
  have H :=  Provable.MP _ _ H3 H4
  exact H


lemma Deduction.imp_intro {var} {Γ : Set (form var)} {φ ψ : form var} :
  Deduction (insert φ Γ) ψ → Deduction Γ (φ.Imp ψ)
:= by
  intro H
  induction H with
  | AX χ H =>
    simp at H
    rcases H with E | H
    · subst χ
      have h1 := Deduction.L2 (Γ := Γ) φ (φ.Imp φ) φ
      have h2 := Deduction.L1 (Γ := Γ) φ (φ.Imp φ)
      have h3 := Deduction.MP (Γ := Γ) _ _ h1 h2
      have h4 := Deduction.L1 (Γ := Γ) φ φ
      have h := Deduction.MP (Γ := Γ) _ _ h3 h4
      exact h
    · apply Deduction.MP χ
      · apply Deduction.L1
      · apply Deduction.AX _ H
  | L1 χ ξ =>
    apply Deduction.MP (χ.Imp (ξ.Imp χ))
    · apply Deduction.L1
    · apply Deduction.L1
  | L2 χ ξ ρ =>
    apply Deduction.MP (((χ.Imp (ξ.Imp ρ)).Imp ((χ.Imp ξ).Imp (χ.Imp ρ))))
    · apply Deduction.L1
    · apply Deduction.L2
  | L3 χ ξ =>
    apply Deduction.MP ((((χ.Not).Imp (ξ.Not)).Imp (ξ.Imp χ)))
    · apply Deduction.L1
    · apply Deduction.L3
  | MP χ ξ H1 H2 IH1 IH2 =>
    apply Deduction.MP (φ.Imp χ)
    apply Deduction.MP
    apply Deduction.L2; assumption
    assumption
  | Top =>
    apply MP (form.Bot.Not)
    · apply Deduction.L1
    · apply Deduction.Top


lemma Deduction.weakening {var} {Γ Δ : Set (form var)} {φ : form var} :
  Γ ⊆ Δ → Deduction Γ φ → Deduction Δ φ
:= by
  intro H0 H
  revert Δ
  induction H with
  | AX χ H =>
    intro Δ H0
    apply Deduction.AX; apply H0 H
  | L1 χ ξ =>
    intro Δ H0
    apply Deduction.L1
  | L2 χ ξ ρ =>
    intro Δ H0
    apply Deduction.L2
  | L3 χ ξ =>
    intro Δ H0
    apply Deduction.L3
  | MP χ ξ H1 H2 IH1 IH2 =>
    intro Δ H0
    apply Deduction.MP
    · apply IH1; assumption
    · apply IH2; assumption
  | Top =>
    intro Δ H0
    apply Deduction.Top

lemma Deduction.imp_elim {var} {Γ : Set (form var)} {φ ψ : form var} :
  Deduction Γ (φ.Imp ψ) → Deduction (insert φ Γ) ψ
:= by
  intro H
  have := weakening (Γ := Γ) (by simp : Γ ⊆ insert φ Γ) H
  apply Deduction.MP _ _ this
  apply Deduction.AX _ (by simp)

lemma Deduction.HS {var} {Γ : Set (form var)} {φ ψ χ : form var} :
  Deduction Γ (φ.Imp ψ) → Deduction Γ (ψ.Imp χ) → Deduction Γ (φ.Imp χ)
:= by
  intro H1 H2
  apply imp_intro
  apply imp_elim at H1
  apply MP ψ _ _ H1
  apply imp_elim
  apply MP _ _ _ H2
  apply L1


/- ------------
- properties -
-------------/


#check himp_self
example [BooleanAlgebra B] (a : B) :
  a ⇨ a = ⊤
:= by
  rw [himp_eq, sup_compl_eq_top]

lemma himp_contrapose [BooleanAlgebra B] (a b : B) :
  (a ⇨ b) ⇨ (bᶜ ⇨ aᶜ) = ⊤
:= by
  rw [himp_eq, himp_eq, himp_eq, compl_sup, compl_compl, compl_compl, sup_inf_left]
  rw [sup_assoc, sup_compl_eq_top, sup_top_eq, top_inf_eq]
  rw [sup_comm, <- sup_assoc, sup_compl_eq_top, top_sup_eq]

lemma himp_contrapose' [BooleanAlgebra B] (a b : B) :
  (aᶜ ⇨ bᶜ) ⇨ (b ⇨ a) = ⊤
:= by
  rw [himp_eq, himp_eq, himp_eq, compl_sup, compl_compl, compl_compl, sup_inf_left]
  rw [sup_assoc, compl_sup_eq_top, sup_top_eq, top_inf_eq]
  rw [sup_comm, <- sup_assoc, compl_sup_eq_top, top_sup_eq]


lemma himp_self_taut {var} (φ : form var) :
  (φ.Imp φ).isTautology
:= by
  intro v
  rcases φ<;> simp

lemma himp_conrrapose'_taut {var} (φ ψ : form var) :
  ((φ.Not.Imp ψ.Not).Imp (ψ.Imp φ)).isTautology
:= by
  intro v
  rcases φ <;>simp [himp]
  case Var a => rcases v a <;> simp
  case Not φ => rcases form.valuation v ψ <;> simp
  case Imp φ₁ φ₂ => rcases form.valuation v φ₁ <;> rcases form.valuation v φ₂ <;> simp


lemma Deduction.stability {var : Type _}  {φ : form var} :
  -- (¬ φ → φ) → φ
  Deduction ∅ ((φ.Not.Imp φ).Imp φ)
:= by
  apply imp_intro; simp
  apply MP (φ.Not.Imp φ); swap
  apply AX; simp
  apply MP
  apply L3
  apply MP (φ.Not.Imp φ);
  swap; apply AX; simp
  apply MP; apply L2
  apply HS; swap
  apply L3
  apply L1

lemma Deduction.exfalso_left {var : Type _}  {φ ψ: form var} :
  -- ¬ φ → (φ → ψ)
  Deduction ∅ (φ.Not.Imp (φ.Imp ψ))
:= by
  apply imp_intro; simp
  apply MP; apply L3
  apply MP φ.Not; swap; apply AX; simp
  apply L1

lemma Deduction.exfalso_right {var : Type _}  {φ ψ: form var} :
  -- φ → (¬ φ → ψ)
  Deduction ∅ (φ.Imp (φ.Not.Imp ψ))
:= by
  apply imp_intro; apply imp_intro; simp
  have : {φ.Not, φ} = insert φ ({φ.Not} : Set (form var)) := by ext; simp; rw [Or.comm]
  rw [this]; clear this
  apply imp_elim;
  have : {φ.Not} = insert φ.Not (∅ : Set (form var)) := by ext; simp
  rw [this]; clear this
  apply imp_elim
  apply exfalso_left

lemma Deduction.not_not_imp {var} {φ : form var} :
  -- ¬ ¬ φ → φ
  Deduction ∅ (φ.Not.Not.Imp φ)
:= by
  apply imp_intro; simp
  apply MP (φ.Not.Imp φ)
  · apply weakening (Γ := ∅); simp
    apply stability
  · apply MP; apply L3
    apply MP (φ.Not.Not)
    apply L1; apply AX; simp

lemma Deduction.imp_not_not {var} {φ : form var} :
  -- φ → ¬ ¬ φ
  Deduction ∅ (φ.Imp φ.Not.Not)
:= by
  apply MP; apply L3
  apply not_not_imp

lemma Deduction.contra {var : Type _}  {φ ψ: form var} :
  -- (φ → ψ) → (¬ ψ → ¬ φ)
  Deduction ∅ ((φ.Imp ψ).Imp (ψ.Not.Imp φ.Not))
:= by
  apply imp_intro; simp
  apply MP
  · apply weakening (Γ := ∅); simp
    apply L3
  · apply imp_intro
    apply MP ψ
    · apply weakening (Γ := ∅); simp
      apply imp_not_not
    · apply MP φ; apply AX; simp
      apply MP
      · apply weakening (Γ := ∅); simp
        apply not_not_imp
      · apply AX; simp

lemma Deduction.and_elim_left {var}  {φ ψ : form var} :
  Deduction ∅ ((φ.And ψ).Imp φ)
:= by
  simp [form.And]
  apply MP; apply L3
  apply imp_intro; simp
  apply MP; apply weakening (Γ := ∅); simp
  apply imp_not_not
  apply MP
  apply weakening (Γ := ∅); simp
  apply exfalso_left
  apply AX; simp

lemma Deduction.and_elim_right {var}  {φ ψ : form var} :
  Deduction ∅ ((φ.And ψ).Imp ψ)
:= by
  simp [form.And]
  apply MP; apply L3
  apply imp_intro; simp
  apply MP; apply weakening (Γ := ∅); simp
  apply imp_not_not
  apply imp_intro
  apply AX; simp

lemma Deduction.or_intro_left {var} {φ ψ : form var} :
  Deduction {φ} (φ.Or ψ)
:= by
  simp [form.Or]
  have E : {φ} = insert φ (∅ : Set (form var)) := by simp
  rw [E]; clear E; apply imp_elim
  apply exfalso_right

lemma Deduction.or_intro_right {var} {φ ψ : form var} :
  Deduction {ψ} (φ.Or ψ)
:= by
  simp [form.Or]
  apply imp_intro; apply AX; simp


lemma Deduction.or_imp_intro {var}  {φ ψ χ : form var} :
  Deduction {φ.Imp χ, ψ.Imp χ} ((φ.Or ψ).Imp χ)
:= by
  simp [form.Or]
  apply imp_intro
  apply MP
  · apply weakening (Γ := ∅); simp
    apply stability
  · apply HS (ψ := φ.Not)
    · apply MP
      · apply weakening (Γ := ∅); simp
        apply contra
      · apply AX; simp
    · apply HS
      · apply AX; simp; left; rfl
      · apply AX; simp

lemma Deduction.and_intro {var}  {φ ψ : form var} :
  Deduction {φ, ψ} (φ.And ψ)
:= by
  simp [form.And]
  apply MP φ.Not.Not; swap
  · apply imp_elim
    apply weakening (Γ := ∅); simp
    apply imp_not_not
  · apply MP
    · apply weakening (Γ := ∅); simp
      apply contra
    · apply imp_intro
      apply MP ψ.Not; swap
      · apply MP φ<;> apply AX<;> simp
      · apply MP
        · apply weakening (Γ := ∅); simp
          apply contra
        · apply imp_intro; apply AX; simp

lemma Deduction.imp_and_intro {var} {φ ψ χ : form var} :
  Deduction {χ.Imp φ, χ.Imp ψ} (χ.Imp (φ.And ψ))
:= by
  apply imp_intro
  apply MP φ; swap
  · apply MP χ<;> apply AX<;> simp
  apply imp_intro
  apply MP ψ; swap
  · apply MP χ<;> apply AX<;> simp
  · apply imp_intro
    apply weakening (Γ := {φ, ψ})
    · intro x; simp; intro Hx
      rcases Hx<;> subst x<;> simp
    · apply and_intro

lemma Deduction.and_or_left {var} {φ ψ χ : form var} :
  Deduction {φ.And (ψ.Or χ)} ((φ.And ψ).Or (φ.And χ))
:= by
  apply MP φ; swap
  · have E : {φ.And (ψ.Or χ)} = insert (φ.And (ψ.Or χ)) (∅ : Set (form var)) := by simp
    rw [E]
    apply imp_elim
    apply and_elim_left
  apply MP (ψ.Or χ); swap
  · have E : {φ.And (ψ.Or χ)} = insert (φ.And (ψ.Or χ)) (∅ : Set (form var)) := by simp
    rw [E]
    apply imp_elim
    apply and_elim_right
  apply weakening (Γ := ∅); simp
  apply imp_intro; apply imp_intro; simp
  apply imp_elim
  have E : {ψ.Or χ} = insert (ψ.Or χ) (∅ : Set (form var)) := by simp
  rw [E]; clear E
  apply imp_elim
  set μ := φ.Imp ((φ.And ψ).Or (φ.And χ))
  apply MP (χ.Imp μ); swap
  · apply imp_intro; simp [μ]
    apply imp_intro
    apply MP (φ.And χ); swap
    · apply and_intro
    · apply weakening (Γ := ∅); simp
      apply imp_intro; simp
      apply or_intro_right
  apply imp_intro; simp
  apply MP (ψ.Imp μ); swap
  · apply weakening (Γ := ∅); simp
    apply imp_intro; simp [μ]
    apply imp_intro
    apply MP (φ.And ψ); swap
    · apply and_intro
    · apply weakening (Γ := ∅); simp
      apply imp_intro; simp
      apply or_intro_left
  apply imp_intro
  apply or_imp_intro

lemma Deduction.or_not {var} {φ : form var} :
  Deduction ∅ (φ.Or φ.Not)
:= by
  simp [form.Or]
  apply imp_intro; simp
  apply AX; simp

lemma Deduction.and_not {var} {φ : form var} :
  Deduction ∅ (φ.And φ.Not).Not
:= by
  simp [form.And]
  apply MP (φ.Imp φ.Not.Not)
  · apply imp_not_not
  · apply imp_not_not