-- Project: Soundness of propositional logic
--
-- Math 4680/5680, "Topics in Logic and Computation"
-- Fall 2026
--
-- Name: _______________________
--
-- ============================================================
--
-- Projects must be done individually. You may not collaborate with
-- other students, and you may not use AI tools. If you have questions
-- or are stuck, ask the instructor.
--
-- In some places, you will need additional lemmas. Please state and
-- prove your own lemmas as appropriate.
--
-- For full marks, complete Parts 1-4. Part 5 is a bonus.
--
-- ============================================================

set_option autoImplicit false
set_option linter.unusedVariables false

namespace Project_Logic

-- ============================================================
-- Introduction
--
-- So far in this course, we have used Lean's own logic: a
-- proposition is an element of `Prop`, and a proof is a term. In this
-- project, we take a step back and study a logic from the outside.
-- We formalize classical propositional logic as a *data type* of
-- formulas, define what it means for a judgement to be *derivable*
-- using the inference rules from class, give a semantics in terms of
-- truth tables, and prove the soundness theorem: every derivable
-- judgement is valid in the truth table interpretation.
--
-- This is the difference between "using" a logic and "studying" a
-- logic. The formulas below are not elements of `Prop`; they are
-- elements of an inductive type, just like natural numbers or lists.
-- Derivations are not Lean proofs of the formulas; they are elements
-- of an inductive family that describes the inference rules.

-- ============================================================
-- Formulas
--
-- Informally, the _formulas_ of propositional logic are given by the
-- following grammar. In case you have not seen this notation before:
-- it means that the set of formulas is the smallest set closed under
-- the given operations.
--
--   Formula   A, B ::= P n | A ⋀ B | A ⇒ B | ⊥ | ⊤
--
-- Here, `n` is a natural number, and `P n` is the nth propositional
-- symbol. `A ⋀ B` is conjunction, `A ⇒ B` is implication, `⊥` is
-- "false", and `⊤` is "true".
--
-- Type these symbols as \bigwedge, \=>, \bot, and \top. We use `⋀`
-- instead of `∧` to avoid confusion with the conjunction of `Prop`.

inductive Formula : Type where
  | P : Nat → Formula
  | and : Formula → Formula → Formula
  | imp : Formula → Formula → Formula
  | bot : Formula
  | top : Formula

infixl:70 " ⋀ " => Formula.and
infixr:60 " ⇒ " => Formula.imp
notation "⊥" => Formula.bot
notation "⊤" => Formula.top

open Formula

-- ============================================================
-- Contexts
--
-- A _context_ is a list of formulas (the hypotheses). On paper, we
-- write `Γ, A` for the context `Γ` extended by one more formula
-- `A`. In Lean, we use lists, and write `A :: Γ` instead. So the
-- most recently added hypothesis comes *first* in the list. For
-- example, the context that we write `A₁, A₂, A₃` on paper is
-- written as `[A₃, A₂, A₁]` in Lean.

abbrev Context := List Formula

-- We use Lean's built-in membership relation for lists. It is
-- defined as an inductive family, essentially as follows:
--
--   inductive List.Mem {α : Type} (a : α) : List α → Prop where
--     | head (as : List α) : List.Mem a (a :: as)
--     | tail (b : α) {as : List α} : List.Mem a as → List.Mem a (b :: as)
--
-- and `A ∈ Γ` is notation for `List.Mem A Γ`. In terms of inference
-- rules:
--
--   ───────────── (head)          A ∈ Γ
--    A ∈ A :: Γ               ───────────── (tail)
--                               A ∈ B :: Γ
--
-- For convenience, you can write `.head` instead of `List.Mem.head`,
-- and similarly for `.tail`.
--
-- For example, `.tail _ (.head _) : A ∈ [B, A]`.

-- ============================================================
-- Derivations
--
-- The judgement `Γ ⊢ A` means: "the conclusion `A` can be derived
-- from the hypotheses `Γ`". It is defined by the following inference
-- rules.
--
--    A ∈ Γ                Γ ⊢ A   Γ ⊢ B          Γ ⊢ A ⋀ B        Γ ⊢ A ⋀ B
-- ─────────── (assump)  ──────────────── (andI) ─────────── (andE1) ─────────── (andE2)
--    Γ ⊢ A                Γ ⊢ A ⋀ B                Γ ⊢ A            Γ ⊢ B
--
--   Γ, A ⊢ B            Γ ⊢ A ⇒ B    Γ ⊢ A       Γ ⊢ (A ⇒ ⊥) ⇒ ⊥
-- ─────────── (impI)  ─────────────────── (impE) ─────────────── (dneg) ───────── (topI)
--  Γ ⊢ A ⇒ B                 Γ ⊢ B                  Γ ⊢ A             Γ ⊢ ⊤
--
-- The rule (dneg), double negation, makes the logic classical. Recall
-- that "not `A`" can be expressed as `A ⇒ ⊥`.
--
-- Note that `Deriv` is an inductive family with two indices: the
-- context and the conclusion. We write `Deriv Γ A` for `Γ ⊢ A` at
-- first, but we introduce the `⊢` notation immediately afterwards.
-- Type `⊢` as \|- or \vdash.

inductive Deriv : Context → Formula → Prop where
  | assump {Γ A} : A ∈ Γ → Deriv Γ A
  | andI {Γ A B} : Deriv Γ A → Deriv Γ B → Deriv Γ (A ⋀ B)
  | andE1 {Γ A B} : Deriv Γ (A ⋀ B) → Deriv Γ A
  | andE2 {Γ A B} : Deriv Γ (A ⋀ B) → Deriv Γ B
  | impI {Γ A B} : Deriv (A :: Γ) B → Deriv Γ (A ⇒ B)
  | impE {Γ A B} : Deriv Γ (A ⇒ B) → Deriv Γ A → Deriv Γ B
  | dneg {Γ A} : Deriv Γ ((A ⇒ ⊥) ⇒ ⊥) → Deriv Γ A
  | topI {Γ} : Deriv Γ ⊤

infix:40 " ⊢ " => Deriv

open Deriv

-- ============================================================
-- Part 1: Some derivations
--
-- Let's practice the proof rules. You have proved similar things
-- before using Lean's own logic; this time, build derivations using
-- the constructors of `Deriv`.

section
  variable {A B C : Formula}

  -- 1.1 (On paper, this would be written as: A, B ⊢ A ⋀ B.)
  theorem derivation1 : [B, A] ⊢ A ⋀ B :=
    sorry

  -- 1.2
  theorem derivation2 : [] ⊢ A ⇒ B ⇒ A ⋀ B :=
    sorry

  -- 1.3
  theorem derivation3 : [] ⊢ A ⋀ B ⇒ B ⋀ A :=
    sorry

  -- 1.4 (On paper: A ⇒ B, B ⇒ C ⊢ A ⇒ C.)
  theorem derivation4 : [B ⇒ C, A ⇒ B] ⊢ A ⇒ C :=
    sorry

  -- 1.5
  theorem derivation5 : [] ⊢ A ⇒ A ⇒ A :=
    sorry

  -- 1.6
  theorem derivation6 : [(A ⇒ A) ⇒ B] ⊢ B :=
    sorry
end

-- ============================================================
-- Part 2: Weakening, and some derived rules
--
-- _Weakening_ is the property that if we add additional hypotheses
-- to an entailment (or change their order), the entailment remains
-- valid. More formally: if `Γ ⊢ A` and `Γ ⊆ Γ'`, then `Γ' ⊢ A`.
--
-- We use Lean's built-in subset relation on lists, which is defined
-- as follows:
--
--   Γ ⊆ Γ'   means   ∀ ⦃A⦄, A ∈ Γ → A ∈ Γ'
--
-- The binder `⦃A⦄` is a "strict implicit" argument. You can mostly
-- treat it like an implicit argument: if `h : Γ ⊆ Γ'` and
-- `hm : A ∈ Γ`, then `h hm : A ∈ Γ'`. The only difference is that
-- when you *construct* a proof of `Γ ⊆ Γ'` with `fun`, you have to
-- bind the formula `A` explicitly, as in `fun A hm => ...`.

-- 2.1 A lemma about `⊆`.
theorem subset_cons {Γ Γ' : Context} {A : Formula} (h : Γ ⊆ Γ') : A :: Γ ⊆ A :: Γ' :=
  sorry

-- 2.2 Prove the weakening lemma.
theorem weakening {Γ Γ' : Context} {A : Formula} : Γ ⊢ A → Γ ⊆ Γ' → Γ' ⊢ A :=
  sorry

-- 2.3 A special case that is often useful. Recall that `::` is a
-- notation for `List.cons`, so `B :: Γ` is the context that would be
-- written as `Γ, B` on paper.
theorem weaken1 {Γ : Context} {A B : Formula} (d : Γ ⊢ A) : (B :: Γ) ⊢ A :=
  sorry

-- Classical logic also has the following rule, called "ex falso
-- quodlibet", or (botE):
--
--     Γ ⊢ ⊥
--   ───────── (botE)
--     Γ ⊢ A
--
-- We did not include it in the rules above, because it follows from
-- the other rules.

-- 2.4 Prove it.
theorem botE {Γ : Context} {A : Formula} (d : Γ ⊢ ⊥) : Γ ⊢ A :=
  sorry

-- 2.5 Peirce's law is classically, but not intuitionistically, valid.
-- It is a relatively difficult derivation; you will need (dneg), and
-- probably (botE). (Hint: first find the derivation on paper, then
-- translate it.)
theorem peirce {A B : Formula} : [] ⊢ ((B ⇒ A) ⇒ B) ⇒ B :=
  sorry

-- ============================================================
-- Part 3: Truth table semantics
--
-- In the truth table semantics, a formula is either true or false,
-- depending on the truth values of its propositional symbols. We
-- represent truth values by booleans.
--
-- Lean already provides the operations `&&` (and), `||` (or), and `!`
-- (not) on `Bool`. Lean does not provide a predefined notation for
-- `implies` on `Bool`, so we define it here:
def implies : Bool → Bool → Bool
  | true, b => b
  | false, _ => true

-- A _truth assignment_ is a map from propositional symbols to `Bool`.
-- Instead of assigning booleans to the actual symbols, it is more
-- convenient to assign booleans to the indices.
abbrev Assign := Nat → Bool

-- Given a truth assignment, we can compute the boolean value of any
-- formula.
def interp (ρ : Assign) : Formula → Bool
  | P n => ρ n
  | A ⋀ B => interp ρ A && interp ρ B
  | A ⇒ B => implies (interp ρ A) (interp ρ B)
  | ⊥ => false
  | ⊤ => true

-- 3.1 Extend the interpretation to contexts. A context should be
-- interpreted as the conjunction of its formulas; in particular, the
-- empty context is true.
def interps (ρ : Assign) : Context → Bool :=
  sorry

-- We write `Γ ⊧ A` ("`Γ` models `A`") if under every truth assignment
-- that makes all of `Γ` true, `A` is also true. This is also called
-- "semantic entailment". Type `⊧` as \models. (Note: this is not
-- `⊨`.)

def Models (Γ : Context) (A : Formula) : Prop :=
  ∀ ρ : Assign, interps ρ Γ = true → interp ρ A = true

infix:40 " ⊧ " => Models

-- 3.2 Some lemmas about the boolean operations. (Hint: pattern match
-- on the booleans. Lean will often notice by itself that some cases
-- are impossible.)

theorem and_intro : ∀ {a b : Bool}, a = true → b = true → (a && b) = true :=
  sorry

theorem and_elim1 : ∀ {a b : Bool}, (a && b) = true → a = true :=
  sorry

theorem and_elim2 : ∀ {a b : Bool}, (a && b) = true → b = true :=
  sorry

theorem implies_intro : ∀ {a b : Bool}, (a = true → b = true) → implies a b = true :=
  sorry

theorem implies_elim : ∀ {a b : Bool}, implies a b = true → a = true → b = true :=
  sorry

theorem double_negation : ∀ {a : Bool}, implies (implies a false) false = true → a = true :=
  sorry

-- 3.3 If a context is true, then each of its members is true.
theorem interps_mem {ρ : Assign} : ∀ {Γ : Context} {A : Formula},
    interps ρ Γ = true → A ∈ Γ → interp ρ A = true :=
  sorry

-- ============================================================
-- Part 4: The soundness theorem
--
-- _Soundness_ states that `Γ ⊢ A` implies `Γ ⊧ A`; in other words,
-- every derivable entailment is valid.

-- 4.1 Prove soundness.
theorem soundness {Γ : Context} {A : Formula} : Γ ⊢ A → Γ ⊧ A :=
  sorry

-- ============================================================
-- Part 5 (bonus)

-- Each bonus question is independent; you may do some, all, or none
-- of them.

-- 5.1 A logic is called _consistent_ if `⊥` is not derivable from
-- the empty context. Use soundness to prove that our logic is
-- consistent.
theorem consistent : ¬ ([] ⊢ ⊥) :=
  sorry

-- 5.2 Instead of truth tables, we can also interpret formulas as
-- elements of `Prop`. Then `⋀` becomes `∧`, `⇒` becomes `→`, and so
-- on. Define the interpretation, and prove soundness for it. What is
-- special about the (dneg) case? (Hint: you may use
-- `Classical.byContradiction`. Would soundness still be provable
-- without it?)

def interpP (ρ : Nat → Prop) : Formula → Prop :=
  sorry

def interpsP (ρ : Nat → Prop) : Context → Prop :=
  sorry

theorem soundP {Γ : Context} {A : Formula} :
    Γ ⊢ A → ∀ ρ : Nat → Prop, interpsP ρ Γ → interpP ρ A :=
  sorry

-- 5.3 If you feel adventurous, add more connectives, such as `¬A` or
-- `A ∨ B`, with their proof rules, and extend everything accordingly.
-- (Do this in a copy of the file, or in a separate namespace.)
--
--     Γ ⊢ A                Γ ⊢ B           Γ ⊢ A ∨ B   Γ, A ⊢ C   Γ, B ⊢ C
--  ─────────── (orI1)   ─────────── (orI2) ───────────────────────────────── (orE)
--   Γ ⊢ A ∨ B            Γ ⊢ A ∨ B                      Γ ⊢ C

-- 5.4 The converse of soundness is called _completeness_. It states
-- that every valid entailment is derivable from the rules of logic.
--
-- Completeness holds, but is much more difficult to prove than
-- soundness. (In the case of predicate logic, which also includes
-- quantifiers, completeness was proved by Gödel and is known as
-- _Gödel's completeness theorem_ – not to be confused with Gödel's
-- incompleteness theorem).
--
-- If you feel extremely ambitious, try to prove the completeness
-- theorem for classical propositional logic.

theorem completeness {Γ : Context} {A : Formula} : Γ ⊧ A → Γ ⊢ A :=
  sorry

end Project_Logic