coqlogic

Require Export Utf8.
Require Export String.
Require Export Lists.List.
Import ListNotations.

Inductive Term :=
| Var : string → Term
| Const : string → Term
| Fun : string → list Term → Term.

Inductive Formula :=
| Tr : Formula
| Fa : Formula
| Rel : string → list Term → Formula
| Eq : Term → Term → Formula
| Neg : Formula → Formula
| Con : Formula → Formula → Formula
| Dis : Formula → Formula → Formula
| Imp : Formula → Formula → Formula
| All : string → Formula → Formula
| Ex : string → Formula → Formula.

Fixpoint subformulas (f : Formula) : list Formula :=
match f with
  | Tr => Tr :: nil
  | Fa => Fa :: nil
  | Rel r ts => Rel r ts :: nil
  | Eq t1 t2 => Eq t1 t2 :: nil
  | Neg f1 => Neg f1 :: (subformulas f1)
  | Con f1 f2 => Con f1 f2 :: ((subformulas f1) ++ (subformulas f2))
  | Dis f1 f2 => Dis f1 f2 :: ((subformulas f1) ++ (subformulas f2))
  | Imp f1 f2 => Imp f1 f2 :: ((subformulas f1) ++ (subformulas f2))
  | All var f1 => All var f1 :: (subformulas f1)
  | Ex var f1 => Ex var f1 :: (subformulas f1)
end.

Definition termvars (t : Term) : list Term :=
match t with
  | Var v => [Var v]
  | Const c => []
  | Fun f ts => ts
end.

Fixpoint freevars (f : Formula) : list Term
match f with
  | Tr => []
  | Fa => []
  | Rel r ts => flat_map termvars ts
  | Eq t1 t2 => termvars t1 ++ termvars t2
  | Neg f1 => freevars f1
  | Con f1 f2 => freevars f1 ++ (freevars f2)
  | Dis f1 f2 => freevars f1 ++ (freevars f2)
  | Imp f1 f2 => freevars f1 ++ (freevars f2)
  | All var f1 => remove (Var var) (freevars f1)
  | Ex var f1 => remove (Var var) (freevars f1)
end.