An algorithm for the substitution of formulas for predicates in first order logic

Question

I am trying to find a detailed description of the definition of substitution of formulas for predicates in first order logic and an implementation of this as a function in Lean or Haskell. The aim is to prove in Lean that this substitution preserves validity and to use it as part of a proof checker for first order logic. I have these definitions in Lean:

import data.finset

/-
Term schemes.
var "x" : An object variable named "x". Ranges over the domain of each interpretation.
func 0 "c" [] : A constant named "c".
func n "f" [x1 ... xn] : A function named "f" of n terms (arguments).
-/
inductive term : Type
| var : string → term
| func (n : ℕ) : string → (fin n → term) → term

open term

/-
Formula schemes.
atom 0 "P" [] : A propositional variable named "P".
atom n "P" [x1 ... xn] : A predicate variable named "P" of n terms (arguments).
-/
inductive formula : Type
| bottom : formula
| top : formula
| atom (n : ℕ) : string → (fin n → term) → formula
| not : formula → formula
| and : formula → formula → formula
| or : formula → formula → formula
| imp : formula → formula → formula
| iff : formula → formula → formula
| forall_ : string → formula → formula
| exists_ : string → formula → formula

open formula

/-
domain: A nonempty set D called the domain of the interpretation. The intention is that all terms have values in D.

nonempty: A proof that there is at least one element in the domain.

func: (n : ℕ, f : string) → (f_{M} : (terms : fin n → domain) → v : domain)
A mapping of each n-ary function symbol f to a function f_{M}.
n : The arity of the function symbol.
f : The function symbol.
f_{M} : The function that the function symbol is mapped to.
terms : fin n → domain : The n terms (arguments) of the function expressed as a finite function.
v : domain : The result of the function. An element in the domain.

pred: (n : ℕ, P : string) → (P_{M} : (terms : fin n → domain) → v : Prop)
A mapping of each n-ary predicate symbol P to a predicate P_{M}.
n : The arity of the predicate symbol.
P : The predicate symbol.
P_{M} : The predicate that the predicate symbol is mapped to.
terms : fin n → domain : The n terms (arguments) of the predicate expressed as a finite function.
v : Prop : The result of the predicate. True or false.
-/
structure interpretation (domain : Type) : Type :=
(nonempty : nonempty domain)
(func (n : ℕ) : string → (fin n → domain) → domain)
(pred (n : ℕ) : string → (fin n → domain) → Prop)


/-
The type of mappings of object variable names to elements of a domain.
-/
def valuation (D : Type) := string → D

/-
The function mapping each term to an element of a domain by a given interpretation and valuation.
-/
def eval_term (D : Type) (m : interpretation D) (v : valuation D) : term → D
| (var x) := v x
| (func n f terms) := m.func n f (fun i : fin n, eval_term (terms i))

notation a' ` ↦ `:25 v := fun f, function.update f a' v

def holds (D : Type) (m : interpretation D) : valuation D → formula → Prop
| _ bottom := false
| _ top := true
| v (atom n x terms) := m.pred n x (fun i : fin n, eval_term D m v (terms i))
| v (not p) := ¬ holds v p
| v (and p q) := holds v p ∧ holds v q
| v (or p q) := holds v p ∨ holds v q
| v (imp p q) := holds v p → holds v q
| v (iff p q) := holds v p ↔ holds v q
| v (forall_ x p) := ∀ a : D, holds ((x ↦ a) v) p
| v (exists_ x p) := ∃ a : D, holds ((x ↦ a) v) p

def is_valid (p : formula) : Prop :=
∀ D : Type, ∀ m : interpretation D, ∀ v : valuation D, holds D m v p

EDIT:

The immediate issue is that I don't understand the fundamental idea of what it means to substitute a predicate for a predicate. That is, I don't have an algorithm using any of the techniques for handling binders. If it is a propositional variable I believe it is only a name replacement, but I don't understand the case for general predicates. What is being replaced by what in the terms and why? A few basic examples would be very helpful. I'm having a hard time finding much of any kind of reference to it.

EDIT:

It appears that if P is a valid formula then uniformly replacing a formula Q for any predicate in P results in a valid formula as long as the free variables in Q do not become bound in the replacement: https://github.com/pthomas505/lean3/blob/cad06c04fbe96e14e1dc76822225a917ba29b76c/src/metalogic/pred.lean#L1176

I am a little confused by this, because I had expected there to be more conditions required, such as those described here: https://math.stackexchange.com/a/1374989/245129

UPDATE:

The sub_pred_formula function in the code below is my attempt to define the substitution in Haskell, but I think it is probably wrong. I would be really grateful if someone could help me fix it, if it is.

{-
References:

https://www.cambridge.org/core/books/handbook-of-practical-logic-and-automated-reasoning/EB6396296813CB562987E8C37AC4520D
https://www.cl.cam.ac.uk/~jrh13/atp/index.html
Harrison, J. (2009).
Handbook of Practical Logic and Automated Reasoning.
Cambridge: Cambridge University Press.
doi:10.1017/CBO9780511576430
-}


import Data.List
import Data.Set
import Data.Foldable


data Term = Var String
          | Func String [Term]
            deriving (Show, Eq, Ord)


data Formula = Pred String [Term]
             | Not Formula
             | Imp Formula Formula
             | Forall String Formula
               deriving (Show, Eq)


{-
all_var_set t = The set of the names of all of the variables that occur in
the term t.
-}
all_var_set :: Term -> Data.Set.Set String
all_var_set (Var x) = Data.Set.singleton x
all_var_set (Func _ ts) = Data.Set.unions (Data.List.map all_var_set ts)


{-
free_var_set p = The set of the names of all of the variables that occur
free in the formula p.
-}
free_var_set :: Formula -> Data.Set.Set String
free_var_set (Pred _ ts) = Data.Set.unions (Data.List.map all_var_set ts)
free_var_set (Not p) = free_var_set p
free_var_set (Imp p q) = Data.Set.union (free_var_set p) (free_var_set q)
free_var_set (Forall x p) = Data.Set.delete x (free_var_set p)


{-
sub_var_term sigma t = The simultaneous substitution of each variable x
in t by sigma x.
-}
sub_var_term :: (String -> Term) -> Term -> Term
sub_var_term sigma (Var x) = sigma x
sub_var_term sigma (Func f ts) = Func f (Data.List.map (sub_var_term sigma) ts)


{-
variant x xs = If x is not in xs then x. If x is in xs then the string
obtained by appending a single quote to x until the resulting string is not in
xs.
-}
variant :: String -> Data.Set.Set String -> String
variant x xs = if Data.Set.member x xs then variant (x ++ "'") xs else x

{-
update_function f x y = The function that maps x to y and all other
values z to f z.
-}
update_function :: (Eq a) => (a -> b) -> a -> b -> (a -> b)
update_function f x y = \z -> if z == x then y else f z

{-
sub_var_formula sigma p = The simultaneous substitution of each free variable
x in p by sigma x. Each binding variable in p is replaced as needed to ensure
that no variable in sigma x becomes bound in the substitution.
-}
sub_var_formula :: (String -> Term) -> Formula -> Formula
sub_var_formula sigma (Pred p ts) =
  Pred p (Data.List.map (sub_var_term sigma) ts)
sub_var_formula sigma (Not p) =
  Not (sub_var_formula sigma p)
sub_var_formula sigma (Imp p q) =
  Imp (sub_var_formula sigma p) (sub_var_formula sigma q)
sub_var_formula sigma (Forall x p) =
  let free = Data.Set.difference (free_var_set p) (Data.Set.singleton x) in
  let x' = if Data.Foldable.any
             (\y -> Data.Set.member x (all_var_set (sigma y))) free
           then variant x
             (free_var_set
               (sub_var_formula (update_function sigma x (Var x)) p))
           else x
  in Forall x' (sub_var_formula (update_function sigma x (Var x')) p)


sub_single_var :: String -> Term -> Formula -> Formula
sub_single_var x t p =
  let sigma = update_function (\y -> Var y) x t in
  sub_var_formula sigma p

zip_check_length :: (a -> b -> c) -> [a] -> [b] -> [c]
zip_check_length _ [] [] = []
zip_check_length f (x : xs) (y : ys) = (f x y) : zip_check_length f xs ys
zip_check_length _ _ _ = error "zip_check_length"


-- uniform simultaneous replacement of the predicates in a formula by formulas

all_pred_set :: Formula -> Data.Set.Set (String, [Term])
all_pred_set (Pred p ts) = Data.Set.singleton (p, ts)
all_pred_set (Not p) = all_pred_set p
all_pred_set (Imp p q) = Data.Set.union (all_pred_set p) (all_pred_set q)
all_pred_set (Forall _ p) = all_pred_set p

zip_to_function :: (Eq a) => [a] -> [b] -> (a -> b) -> (a -> b)
zip_to_function [] [] f = f
zip_to_function (x:xs) (y:ys) f = zip_to_function xs ys (update_function f x y)
zip_to_function _ _ _ = error "zip_to_function"

zip_var_to_term :: [String] -> [Term] -> (String -> Term)
zip_var_to_term xs ts = zip_to_function xs ts (\x -> Var x)

sub_pred_formula_aux ::
  (String -> Term) -> ((String, [Term]) -> ([String], Formula)) -> Formula -> Formula
sub_pred_formula_aux sigma m (Pred p ts) =
  let (params, q) = m (p, ts) in
  let sigma' = zip_to_function params ts sigma in
  sub_var_formula sigma' q
sub_pred_formula_aux sigma m (Not p) =
  Not (sub_pred_formula_aux sigma m p)
sub_pred_formula_aux sigma m (Imp p q) =
  Imp (sub_pred_formula_aux sigma m p) (sub_pred_formula_aux sigma m q)
sub_pred_formula_aux sigma m (Forall x p) =
  let x' = if Data.Foldable.any
             (\r -> Data.Set.member x
               (Data.Set.difference (free_var_set (snd (m r))) (Data.Set.fromList (fst (m r)))))
             (all_pred_set p)
           then variant x (free_var_set
             (sub_pred_formula_aux (update_function sigma x (Var x)) m p))
           else x
  in Forall x' (sub_pred_formula_aux (update_function sigma x (Var x')) m p)

sub_pred_formula :: ((String, [Term]) -> ([String], Formula)) -> Formula -> Formula
sub_pred_formula m p = sub_pred_formula_aux (\x -> Var x) m p

sub_single_pred :: (String, [Term]) -> ([String], Formula) -> Formula -> Formula
sub_single_pred (p, ts) (params, q) r =
  let m = update_function (\(p', ts') -> ([], Pred p' ts')) (p, ts) (params, q) in
  sub_pred_formula m r



data Step = Modus_Ponens Int Int
          | Prop_1 Formula Formula
          | Prop_2 Formula Formula Formula
          | Prop_3 Formula Formula
          | Gen Int String
          | Pred_1 Formula Formula String
          | Pred_2 Formula String Term
          | Pred_3 Formula String
          | Eq_1 Term
          | Eq_2 String [Term] [Term]
          | Eq_3 String [Term] [Term]


check_step :: [Formula] -> Step -> [Formula]

-- |- p & |- (p -> q) => |- q
check_step context (Modus_Ponens p_index p_q_index) =
  let p = context !! p_index in
  let (Imp p' q) = context !! p_q_index in
  if p == p' then context ++ [q] else error "Modus_Ponens"

-- |- (p -> (q -> p))
check_step context (Prop_1 p q) =
  context ++ [(p `Imp` (q `Imp` p))]

-- |- ((p -> (q -> r)) -> ((p -> q) -> (p -> r)))
check_step context (Prop_2 p q r) =
  context ++ [((p `Imp` (q `Imp` r)) `Imp` ((p `Imp` q) `Imp` (p `Imp` r)))]

-- |- ((~p -> ~q) -> (q -> p))
check_step context (Prop_3 p q) =
  context ++ [(((Not p) `Imp` (Not q)) `Imp` (q `Imp` p))]


-- |- p => |- (forall x. p)
check_step context (Gen p_index x) =
  let p = context !! p_index in
  context ++ [(Forall x p)]

-- |- ((forall x. (p -> q)) -> ((forall x. p) -> (forall x. q)))
check_step context (Pred_1 p q x) =
  context ++ [((Forall x (p `Imp` q)) `Imp` ((Forall x p) `Imp` (Forall x q)))]

-- |- ((forall x. p) -> (p [x -> t]))
check_step context (Pred_2 p x t) =
  context ++ [((Forall x p) `Imp` (sub_single_var x t p))]

-- |- (p -> (forall x. p)) provided x is not free in p
check_step context (Pred_3 p x) =
  if Data.Set.notMember x (free_var_set p)
  then context ++ [(p `Imp` (Forall x p))]
  else error "Pred_3"


-- |- t = t
check_step context (Eq_1 t) =
  context ++ [(Pred "Eq" [t, t])]

-- |- s1 = t1 -> ... -> sn = tn -> f(s1,..,sn) = f(t1,..,tn)
check_step context (Eq_2 f ss ts) =
  -- eqs = [s1 = t1, ..., sn = tn]
  let eqs = zip_check_length (\s t -> (Pred "Eq" [s, t])) ss ts in
  -- z = f(s1,..,sn) = f(t1,..,tn)
  let z = Pred "Eq" [(Func f ss), (Func f ts)] in
  context ++ [(Prelude.foldr Imp z eqs)]

-- |- s1 = t1 -> ... -> sn = tn -> P(s1,..,sn) -> P(t1,..,tn)
check_step context (Eq_3 p ss ts) =
  -- eqs = [s1 = t1, ..., sn = tn]
  let eqs = zip_check_length (\s t -> (Pred "Eq" [s, t])) ss ts in
  -- z = P(s1,..,sn) ==> P(t1,..,tn)
  let z = (Pred p ss) `Imp` (Pred p ts) in
  context ++ [(Prelude.foldr Imp z eqs)]


check_step_list_aux :: [Formula] -> [Step] -> Formula
check_step_list_aux context [] = Data.List.last context
check_step_list_aux context (step : step_list) =
  let context' = check_step context step in
  check_step_list_aux context' step_list

check_step_list :: [Step] -> Formula
check_step_list step_list = check_step_list_aux [] step_list


example_1 = [
  (Prop_2 (Pred "P" []) ((Pred "P" []) `Imp` (Pred "P" [])) (Pred "P" [])),
  (Prop_1 (Pred "P" []) ((Pred "P" []) `Imp` (Pred "P" []))),
  (Modus_Ponens 1 0),
  (Prop_1 (Pred "P" []) (Pred "P" [])),
  (Modus_Ponens 3 2) ]
```