Formalizing Bertrand Russell's Principia Mathematica Using Lean4
(the HTML export of this file is rendered better than the GitHub's rendering of org files; check https://ndrwnaguib.com/principia)

open Lean Meta Elab Tactic Term

structure ImpProof where
  (ant cons : Expr)
  (proof : Expr)
  deriving Inhabited

theorem compose {p q r : Prop} (a : p → q) (b : q → r) : p → r :=
  b ∘ a

/-- Compose two implication proofs using the `compose` theorem. -/
def ImpProof.compose (a : ImpProof) (b : ImpProof) : MetaM ImpProof := do
  unless ← isDefEq a.cons b.ant do
    throwError "\
      Consequent{indentD a.cons}\n\
      is not definitionally equal to antecedent{indentD b.ant}"
  let proof := mkApp5 (.const ``compose []) a.ant a.cons b.cons a.proof b.proof
  return { ant := a.ant, cons := b.cons, proof := proof }

/-- Create the proof of `p -> p` using the `id` function. -/
def ImpProof.rfl (p : Expr) : ImpProof :=
  { ant := p, cons := p, proof := .app (.const ``id [.zero]) p}

syntax "Syll" (ppSpace "[" term,* "]")? : tactic

elab_rules : tactic
  | `(tactic| Syll $[[$[$terms?],*]]?) => withMainContext do

    -- Elaborate all the supplied hypotheses, or use the entire local context if not provided.
    let hyps ←
      match terms? with
      | none => getLocalHyps
      | some terms => terms.mapM fun term => Tactic.elabTerm term none

    liftMetaTactic1 fun goal => do
      let goalType ← goal.getType

      -- A list of implications extracted from `hyps`.
      let mut chain : Array ImpProof := #[]

      let getImplication? (e : Expr) : MetaM (Option (Expr × Expr)) := do
        -- There may be metadata and metavariables, so do some unfolding if necessary:
        let ty ← instantiateMVars (← whnfR e)
        -- Check if it is a non-dependent forall:
        if ty.isArrow then
          return (ty.bindingDomain!, ty.bindingBody!)
        else
          return none

      for hyp in hyps do
        match ← getImplication? (← inferType hyp) with
        | some (p, q) => chain := chain.push {ant := p, cons := q, proof := hyp}
        | none => logInfo m!"Expression {hyp} is not of the form `p → q`"

      let some (p, q) ← getImplication? goalType
        | throwError "Goal type is not of the form `p → q`"

      if chain.isEmpty then
        throwError "Local context has no implications"

      unless ← isExprDefEq chain[0]!.ant p do
        throwError "The first hypothesis does not match the goal's antecedent"

      unless ← isExprDefEq chain[chain.size - 1]!.cons q do
        throwError "The last hypothesis does not match the goal's consequent"

      let comp ← chain.foldlM (init := ImpProof.rfl p) (fun pf1 pf2 => pf1.compose pf2)

      -- It's good to do one last check that the proof has the correct type before assignment.
      unless ← isDefEq (← inferType comp.proof) goalType do
        throwError "Invalid proof of goal"
      goal.assign comp.proof

      return none