import Mathlib.Tactic.Ring

inductive WFF : Type
  | p_atm : String → WFF
  | p_not : WFF → WFF
  | p_and : WFF → WFF → WFF
  | p_or  : WFF → WFF → WFF
  | p_imp : WFF → WFF → WFF
  | p_iff : WFF → WFF → WFF

open WFF


/-1.1 递归定义函数 size(φ) ,表示公式中构造子的总数（包括原子命题和所有连接词）-/
def WFF_size : WFF → Nat
  | p_atm _   => 1
  | p_not φ   => 1 + WFF_size φ
  | p_and φ ψ => 1 + WFF_size φ + WFF_size ψ
  | p_or  φ ψ => 1 + WFF_size φ + WFF_size ψ
  | p_imp φ ψ => 1 + WFF_size φ + WFF_size ψ
  | p_iff φ ψ => 1 + WFF_size φ + WFF_size ψ

/-1.2 证明：对任意公式φ，都有 size(φ) ≥ 1-/
theorem WFF_size_pos :
  ∀ f : WFF, WFF_size f ≥ 1 := by
  intro f
  induction f with
  | p_atm s =>
      simp [WFF_size]
  | p_not φ ih =>
      simp [WFF_size]
  | p_and φ ψ ihφ ihψ =>
      simp [WFF_size]
      exact le_add_of_le_right ihψ
  | p_or φ ψ ihφ ihψ =>
      simp [WFF_size]
      exact le_add_of_le_right ihψ
  | p_imp φ ψ ihφ ihψ =>
      simp [WFF_size]
      exact le_add_of_le_right ihψ
  | p_iff φ ψ ihφ ihψ =>
      simp [WFF_size]
      exact le_add_of_le_right ihψ



/-2.1 递归定义函数num_not(φ)，表示公式中not出现的个数-/
def WFF_num_not : WFF → Nat
  | p_atm _   => 0
  | p_not φ   => 1 + WFF_num_not φ
  | p_and φ ψ => WFF_num_not φ + WFF_num_not ψ
  | p_or  φ ψ => WFF_num_not φ + WFF_num_not ψ
  | p_imp φ ψ => WFF_num_not φ + WFF_num_not ψ
  | p_iff φ ψ => WFF_num_not φ + WFF_num_not ψ

/-2.2 证明：对任意公式φ，都有num_not(φ) ≤ size(φ)-/
theorem WFF_num_not_le_size :
  ∀ f : WFF, WFF_num_not f ≤ WFF_size f := by
  intro f
  induction f with
  | p_atm s =>
      simp [WFF_num_not, WFF_size]
  | p_not φ ih =>
      simp [WFF_num_not, WFF_size]
      exact ih
  | p_and φ ψ ihφ ihψ =>
      simp [WFF_num_not, WFF_size]
      refine Nat.add_le_add ?_ ihψ
      exact le_add_of_le_right ihφ
  | p_or φ ψ ihφ ihψ =>
      simp [WFF_num_not, WFF_size]
      refine Nat.add_le_add ?_ ihψ
      exact le_add_of_le_right ihφ
  | p_imp φ ψ ihφ ihψ =>
      simp [WFF_num_not, WFF_size]
      refine Nat.add_le_add ?_ ihψ
      exact le_add_of_le_right ihφ
  | p_iff φ ψ ihφ ihψ =>
      simp [WFF_num_not, WFF_size]
      refine Nat.add_le_add ?_ ihψ
      exact le_add_of_le_right ihφ

/-3.1 递归定义函数
（1）num_atom(φ)，表示公式中原子命题的个数
（2）num_binary(φ)，表示公式中所有二元连接词的个数-/
def WFF_num_atom : WFF → Nat
  | p_atm _   => 1
  | p_not φ   => WFF_num_atom φ
  | p_and φ ψ => WFF_num_atom φ + WFF_num_atom ψ
  | p_or  φ ψ => WFF_num_atom φ + WFF_num_atom ψ
  | p_imp φ ψ => WFF_num_atom φ + WFF_num_atom ψ
  | p_iff φ ψ => WFF_num_atom φ + WFF_num_atom ψ

def WFF_num_binary : WFF → Nat
  | p_atm _   => 0
  | p_not φ   => WFF_num_binary φ
  | p_and φ ψ => 1 + WFF_num_binary φ + WFF_num_binary ψ
  | p_or  φ ψ => 1 + WFF_num_binary φ + WFF_num_binary ψ
  | p_imp φ ψ => 1 + WFF_num_binary φ + WFF_num_binary ψ
  | p_iff φ ψ => 1 + WFF_num_binary φ + WFF_num_binary ψ

/-3.2 证明：对任意公式φ，都有num_atom(φ)=num_binary(φ)+1-/
theorem WFF_atom_binary_relation :
  ∀ f : WFF, WFF_num_atom f = WFF_num_binary f + 1 := by
  intro f
  induction f with
  | p_atm s =>
      simp [WFF_num_atom, WFF_num_binary]
  | p_not φ ih =>
      simp [WFF_num_atom, WFF_num_binary]
      exact ih
  | p_and φ ψ ihφ ihψ =>
      simp [WFF_num_atom, WFF_num_binary]
      rw [ihφ, ihψ]
      ring
  | p_or φ ψ ihφ ihψ =>
      simp [WFF_num_atom, WFF_num_binary]
      rw [ihφ, ihψ]
      ring
  | p_imp φ ψ ihφ ihψ =>
      simp [WFF_num_atom, WFF_num_binary]
      rw [ihφ, ihψ]
      ring
  | p_iff φ ψ ihφ ihψ =>
      simp [WFF_num_atom, WFF_num_binary]
      rw [ihφ, ihψ]
      ring

/-4.1 递归定义函数
（1）L(φ)，表示公式中左括号的个数
（2）R(φ)，表示公式中右括号的个数-/
def WFF_num_left_brackets : WFF → Nat
  | p_atm _   => 0
  | p_not φ   => 1 + WFF_num_left_brackets φ
  | p_and φ ψ => 1 + WFF_num_left_brackets φ + WFF_num_left_brackets ψ
  | p_or  φ ψ => 1 + WFF_num_left_brackets φ + WFF_num_left_brackets ψ
  | p_imp φ ψ => 1 + WFF_num_left_brackets φ + WFF_num_left_brackets ψ
  | p_iff φ ψ => 1 + WFF_num_left_brackets φ + WFF_num_left_brackets ψ

def WFF_num_right_brackets : WFF → Nat
  | p_atm _   => 0
  | p_not φ   => 1 + WFF_num_right_brackets φ
  | p_and φ ψ => 1 + WFF_num_right_brackets φ + WFF_num_right_brackets ψ
  | p_or  φ ψ => 1 + WFF_num_right_brackets φ + WFF_num_right_brackets ψ
  | p_imp φ ψ => 1 + WFF_num_right_brackets φ + WFF_num_right_brackets ψ
  | p_iff φ ψ => 1 + WFF_num_right_brackets φ + WFF_num_right_brackets ψ

/-4.2证明：对任意公式φ，都有L(φ)=R(φ)-/
theorem WFF_balance_of_brackets :
  ∀ f : WFF, WFF_num_left_brackets f = WFF_num_right_brackets f := by
  intro f
  induction f with
  | p_atm s =>
      simp [WFF_num_left_brackets, WFF_num_right_brackets]
  | p_not φ ih =>
      simp [WFF_num_left_brackets, WFF_num_right_brackets]
      exact ih
  | p_and φ ψ ihφ ihψ =>
      simp [WFF_num_left_brackets, WFF_num_right_brackets]
      rw [ihφ, ihψ]
  | p_or φ ψ ihφ ihψ =>
      simp [WFF_num_left_brackets, WFF_num_right_brackets]
      rw [ihφ, ihψ]
  | p_imp φ ψ ihφ ihψ =>
      simp [WFF_num_left_brackets, WFF_num_right_brackets]
      rw [ihφ, ihψ]
  | p_iff φ ψ ihφ ihψ =>
      simp [WFF_num_left_brackets, WFF_num_right_brackets]
      rw [ihφ, ihψ]