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 _   => sorry
  | p_not φ   => sorry
  | p_and φ ψ => sorry
  | p_or  φ ψ => sorry
  | p_imp φ ψ => sorry
  | p_iff φ ψ => sorry

/-1.2 证明：对任意公式φ，都有 size(φ) ≥ 1-/
theorem WFF_size_pos :
  ∀ f : WFF, WFF_size f ≥ 1 := by
  sorry


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

/-2.2 证明：对任意公式φ，都有num_not(φ) ≤ size(φ)-/
theorem WFF_num_not_le_size :
  ∀ f : WFF, WFF_num_not f ≤ WFF_size f := by
  sorry


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

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

/-3.2 证明：对任意公式φ，都有num_atom(φ)=num_binary(φ)+1-/
theorem WFF_atom_binary_relation :
  ∀ f : WFF, WFF_num_atom f = WFF_num_binary f + 1 := by
  sorry


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

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

/-4.2证明：对任意公式φ，都有L(φ)=R(φ)-/
theorem WFF_balance_of_brackets :
  ∀ f : WFF, WFF_num_left_brackets f = WFF_num_right_brackets f := by
  sorry