type label =
  | Axiom
  | AndI
  | AndE
  | OrI
  | OrE
  | ArrI
  | ArrE
  | NegI
  | NegE
  | RAA
  | IffI
  | IffE
  | EqI
  | EqE
  | ForallI
  | ForallE
  | ExistsI
  | ExistsE

type pref = Linenum of int | Named of string
type t = { children : pref list; label : label; formula : Formula.t }

let rec valid res a { children; label; formula } =
  let children = List.map res children in
  match (children, label, formula) with
  | [], Axiom, phi -> List.mem phi a
  | [ left; right ], AndI, Conj (phi, psi) ->
      left.formula = phi && right.formula = psi && valid res a left
      && valid res a right
  | [ ({ formula = Conj (phi, psi); _ } as kid) ], AndE, chi ->
      (chi = phi || chi = psi) && valid res a kid
  | [ kid ], OrI, Disj (phi, psi) ->
      (kid.formula = phi || kid.formula = psi) && valid res a kid
  | [ ({ formula = Disj (phi, psi); _ } as left); middle; right ], OrE, chi ->
      middle.formula = chi && right.formula = chi && valid res a left
      && valid res (phi :: a) middle
      && valid res (psi :: a) right
  | [ kid ], ArrI, Impl (phi, psi) ->
      kid.formula = psi && valid res (phi :: a) kid
  | [ left; right ], ArrE, psi ->
      left.formula = Impl (right.formula, psi)
      && valid res a left && valid res a right
  | [ kid ], NegI, Neg phi -> kid.formula = Bottom && valid res (phi :: a) kid
  | [ left; right ], NegE, Bottom ->
      left.formula = Neg right.formula && valid res a left && valid res a right
  | [ kid ], RAA, phi -> kid.formula = Bottom && valid res (Neg phi :: a) kid
  | [ left; right ], IffI, Iff (phi, psi) ->
      left.formula = Impl (phi, psi)
      && right.formula = Impl (psi, phi)
      && valid res a left && valid res a right
  | [ left; right ], IffE, phi ->
      (left.formula = Iff (right.formula, phi)
      || left.formula = Iff (phi, right.formula))
      && valid res a left && valid res a right
  | [], EqI, Equal (x, y) -> x = y

(* TODO:
   - EqE
   - ForallI
   - ForallE
   - ExistsI
   - ExistsE
*)