inductive Formula : Type
  | var (s : String)       : Formula
  | bot                    : Formula
  | conj (f1 f2 : Formula) : Formula
  | disj (f1 f2 : Formula) : Formula
  | impl (f1 f2 : Formula) : Formula -- You may also define negation here
  deriving Repr, BEq

-- Custom notation for convenience
local infixl:35 " ∧ₚ " => Formula.conj
local infixl:30 " ∨ₚ " => Formula.disj
local infixr:25 " →ₚ " => Formula.impl
local notation "⊥ₚ"   => Formula.bot

structure Sequent where
  gamma : List Formula -- Left side (antecedents)
  delta : List Formula -- Right side (succedents)

-- A sequent is an axiom if ⊥ₚ is on the left, or if a formula is on both sides
def isAxiom (seq : Sequent) : Bool :=
  seq.gamma.contains Formula.bot || seq.gamma.any (fun f => seq.delta.contains f)

def proveSequent (fuel : Nat) (seq : Sequent) : Bool :=
  if isAxiom seq then true
  else match fuel with
  | 0 => false -- Out of fuel
  | n + 1 =>
    -- 1. Try to decompose the FIRST formula on the Left (Gamma)
    match seq.gamma with
    | Formula.conj f1 f2 :: rest => 
      proveSequent n ⟨f1 :: f2 :: rest, seq.delta⟩
    | Formula.disj f1 f2 :: rest => 
      proveSequent n ⟨f1 :: rest, seq.delta⟩ && proveSequent n ⟨f2 :: rest, seq.delta⟩
    | Formula.impl f1 f2 :: rest => 
      proveSequent n ⟨rest, f1 :: seq.delta⟩ && proveSequent n ⟨f2 :: rest, seq.delta⟩
    | Formula.var s :: rest => 
      -- It's a variable; cycle it to the back of gamma to check other formulas
      proveSequent n ⟨rest ++ [Formula.var s], seq.delta⟩
    | Formula.bot :: _ => 
      true -- Handled by isAxiom
    | [] =>
      -- 2. If Left is fully processed (only variables left), decompose the Right (Delta)
      match seq.delta with
      | [] => false -- No rules left to apply and it's not an axiom
      | Formula.conj f1 f2 :: rest =>
        proveSequent n ⟨seq.gamma, f1 :: rest⟩ && proveSequent n ⟨seq.gamma, f2 :: rest⟩
      | Formula.disj f1 f2 :: rest =>
        proveSequent n ⟨seq.gamma, f1 :: f2 :: rest⟩
      | Formula.impl f1 f2 :: rest =>
        proveSequent n ⟨f1 :: seq.gamma, f2 :: rest⟩
      | Formula.var s :: rest =>
        -- It's a variable; cycle it to the back of delta
        proveSequent n ⟨seq.gamma, rest ++ [Formula.var s]⟩
      | Formula.bot :: rest =>
        proveSequent n ⟨seq.gamma, rest ++ [Formula.bot]⟩

-- Top-level prover: starts with an empty Gamma and the formula in Delta
def proveFormula (f : Formula) : Bool :=
  proveSequent 100 ⟨[], [f]⟩

-- Test Case A: Peirce's Law 
def pierce : Formula :=
  ((Formula.var "P" →ₚ Formula.var "Q") →ₚ Formula.var "P") →ₚ Formula.var "P"

-- Test Case B: Ex Falso Quodlibet
def exFalso : Formula := ⊥ₚ →ₚ Formula.var "P"

-- Test Case C: An invalid formula
def invalidFormula : Formula := Formula.var "P" →ₚ Formula.var "Q"

-- Test Case D: Modus Ponens
def mp : Formula := Formula.var "P" ∨ₚ (Formula.var "P" →ₚ ⊥ₚ) 

#eval proveFormula pierce          -- Returns: true
#eval proveFormula exFalso         -- Returns: true
#eval proveFormula invalidFormula  -- Returns: false
#eval proveFormula mp              -- Returns: true