Partial implementation of stupid Gentzen proof search

gentzen.lean

import Mathlib.Data.Multiset.Basic
import Mathlib.Algebra.Group.Defs
import Mathlib.Algebra.Group.Nat.Defs
import Mathlib.Data.Multiset.MapFold

inductive Wff
  | var (name : String)
  | imp (a b : Wff)
  | not (a : Wff)
  | or (a b : Wff)
  | and (a b : Wff)
  deriving DecidableEq

structure Sequent where
  antecedents : Multiset Wff
  consequents : Multiset Wff
  deriving DecidableEq

def Wff.numConnectives : Wff → Nat
  | .var _ => 0
  | .imp a b => a.numConnectives + b.numConnectives + 1
  | .not a => a.numConnectives + 1
  | .or a b => a.numConnectives + b.numConnectives + 1
  | .and a b => a.numConnectives + b.numConnectives + 1

def Multiset.foldMap [AddCommMonoid m] (s : Multiset α) (f : α → m) : m :=
  let reducer x y := f x + y
  have : LeftCommutative reducer := by
    constructor
    intro a₁ a₂ b
    unfold reducer
    repeat rw [← add_assoc]
    rw [add_comm (a := f a₁)]
  s.foldr reducer 0

@[simp]
theorem pre_foldmap [AddCommMonoid m] (f : α → m) : Multiset.foldMap (x ::ₘ a) f = f x + Multiset.foldMap a f := by
  unfold Multiset.foldMap
  simp

def Sequent.numConnectives (s : Sequent) :=
  s.antecedents.foldMap Wff.numConnectives + s.consequents.foldMap Wff.numConnectives

@[simp]
theorem numConnectives_ante_cons : Sequent.numConnectives ⟨a ::ₘ as, bs⟩ = a.numConnectives + Sequent.numConnectives ⟨as, bs⟩ := by
  simp +arith [Sequent.numConnectives]

@[simp]
theorem numConnectives_cons_cons : Sequent.numConnectives ⟨as, b ::ₘ bs⟩ = b.numConnectives + Sequent.numConnectives ⟨as, bs⟩ := by
  simp +arith [Sequent.numConnectives]

abbrev PickAntecedent (s : Sequent) := (a : Wff) × (as bs : Multiset Wff) ×' (s = ⟨a ::ₘ as, bs⟩) ∧ (a.numConnectives ≠ 0)
abbrev PickConsequent (s : Sequent) := (b : Wff) × (as bs : Multiset Wff) ×' (s = ⟨as, b ::ₘ bs⟩) ∧ (b.numConnectives ≠ 0)

inductive PickResult (s : Sequent)
  | antecedent : PickAntecedent s → PickResult s
  | consequent : PickConsequent s → PickResult s
  | none : s.numConnectives = 0 → PickResult s

def Sequent.pick (s : Sequent) : PickResult s := sorry

inductive Proof : Sequent → Type where
  | a x : x ∈ a → x ∈ c → Proof ⟨a, c⟩
  | andl : Proof ⟨a ::ₘ b ::ₘ as, bs⟩ → Proof ⟨.and a b ::ₘ as, bs⟩
  | orl : Proof ⟨a ::ₘ as, bs⟩ → Proof ⟨b ::ₘ as, bs⟩ → Proof ⟨.or a b ::ₘ as, bs⟩
  | impl : Proof ⟨as, a ::ₘ bs⟩ → Proof ⟨b ::ₘ as, bs⟩ → Proof ⟨.imp a b ::ₘ as, bs⟩
  | notl : Proof ⟨as, a ::ₘ bs⟩ → Proof ⟨.not a ::ₘ as, bs⟩
  | andr : Proof ⟨as, a ::ₘ bs⟩ → Proof ⟨as, b ::ₘ bs⟩ → Proof ⟨as, .and a b ::ₘ bs⟩
  | orr : Proof ⟨as, a ::ₘ b ::ₘ bs⟩ → Proof ⟨as, .or a b ::ₘ bs⟩
  | impr : Proof ⟨a ::ₘ as, b ::ₘ bs⟩ → Proof ⟨as, .imp a b ::ₘ bs⟩
  | notr : Proof ⟨a ::ₘ as, bs⟩ → Proof ⟨as, .not a ::ₘ bs⟩

def prove {s : Sequent} : Option (Proof s) := do
  match s.pick with
  | .antecedent ⟨x, as, bs, hx, hc⟩ => hx ▸ match x with
    | .var _ => by contradiction
    | .and a b => return .andl (← prove)
    | .or a b => return .orl (← prove) (← prove)
    | .imp a b => return .impl (← prove) (← prove)
    | .not a => return .notl (← prove)
  | .consequent ⟨x, as, bs, hx, hc⟩ => hx ▸ match x with
    | .var _ => by contradiction
    | .and a b => return .andr (← prove) (← prove)
    | .or a b => return .orr (← prove)
    | .imp a b => return .impr (← prove)
    | .not a => return .notr (← prove)
  | .none h => sorry
termination_by s.numConnectives
decreasing_by
  all_goals (rw [hx]; simp +arith [Wff.numConnectives])

abbrev prove' s := @prove s

#print axioms prove