done with kernel I think

lib/formula.ml

@@ -9,3 +9,38 @@ type t =
   | Iff of t * t
   | Forall of t
   | Exists of t
+
+let rec match_term t phi psi =
+  match (phi, psi) with
+  | Relation (r1, ts1), Relation (r2, ts2) ->
+      if r1 = r2 && List.length ts1 = List.length ts2 then
+        List.map2 (Term.match_term t) ts1 ts2
+        |> List.fold_left Term.merge_result None
+      else MatchErr
+  | Equal (t1, s1), Equal (t2, s2) ->
+      Term.(merge_result (match_term t t1 t2) (match_term t s1 s2))
+  | Bottom, Bottom -> None
+  | Neg phi, Neg psi -> match_term t phi psi
+  | Conj (phi1, psi1), Conj (phi2, psi2) ->
+      Term.merge_result (match_term t phi1 phi2) (match_term t psi1 psi2)
+  | Disj (phi1, psi1), Disj (phi2, psi2) ->
+      Term.merge_result (match_term t phi1 phi2) (match_term t psi1 psi2)
+  | Impl (phi1, psi1), Impl (phi2, psi2) ->
+      Term.merge_result (match_term t phi1 phi2) (match_term t psi1 psi2)
+  | Iff (phi1, psi1), Iff (phi2, psi2) ->
+      Term.merge_result (match_term t phi1 phi2) (match_term t psi1 psi2)
+  | Forall phi, Forall psi -> match_term (Term.inc_var t) phi psi
+  | Exists phi, Exists psi -> match_term (Term.inc_var t) phi psi
+  | _ -> MatchErr
+
+let rec occurs t = function
+  | Relation (_, ts) -> List.exists (Term.occurs t) ts
+  | Equal (t1, t2) -> Term.occurs t t1 || Term.occurs t t2
+  | Bottom -> false
+  | Neg phi -> occurs t phi
+  | Conj (phi, psi) -> occurs t phi || occurs t psi
+  | Disj (phi, psi) -> occurs t phi || occurs t psi
+  | Impl (phi, psi) -> occurs t phi || occurs t psi
+  | Iff (phi, psi) -> occurs t phi || occurs t psi
+  | Forall phi -> occurs (Term.inc_var t) phi
+  | Exists phi -> occurs (Term.inc_var t) phi

lib/formula.mli

@@ -9,3 +9,6 @@ type t =
   | Iff of t * t
   | Forall of t
   | Exists of t
+
+val match_term : Term.t -> t -> t -> Term.match_result
+val occurs : Term.t -> t -> bool

lib/proof.ml

@@ -54,11 +54,42 @@ let rec valid res a { children; label; formula } =
       || left.formula = Iff (phi, right.formula))
       && valid res a left && valid res a right
   | [], EqI, Equal (x, y) -> x = y
-
+  | [ ({ formula = Equal (t, s); _ } as left); right ], EqE, phi -> (
-(* TODO:
+      valid res a left && valid res a right
-   - EqE
+      &&
-   - ForallI
+      match Formula.match_term t right.formula phi with
-   - ForallE
+      | All s' -> s = s'
-   - ExistsI
+      | Some s' -> s = s'
-   - ExistsE
+      | None -> true
-*)
+      | MatchErr -> false)
+  | [ kid ], ForallI, Forall phi -> (
+      valid res a kid
+      &&
+      match Formula.match_term (Var 0) phi kid.formula with
+      | All (Free x) -> List.exists (Formula.occurs (Free x)) a |> not
+      | All _ -> false
+      | None -> true
+      | Some _ | MatchErr -> false)
+  | [ ({ formula = Forall phi; _ } as kid) ], ForallE, psi -> (
+      valid res a kid
+      &&
+      match Formula.match_term (Var 0) phi psi with
+      | All _ -> true
+      | None -> Formula.occurs (Var 0) phi |> not
+      | Some _ | MatchErr -> false)
+  | [ kid ], ExistsI, Exists phi -> (
+      valid res a kid
+      &&
+      match Formula.match_term (Var 0) phi kid.formula with
+      | All _ -> true
+      | None -> Formula.occurs (Var 0) phi |> not
+      | Some _ | MatchErr -> false)
+  | [ ({ formula = Exists phi; _ } as kid) ], ExistsE, psi -> (
+      valid res a kid
+      &&
+      match Formula.match_term (Var 0) phi psi with
+      | All (Free x) -> List.exists (Formula.occurs (Free x)) a |> not
+      | All _ -> false
+      | None -> true
+      | Some _ | MatchErr -> false)
+  | _ -> false

lib/term.ml

@@ -1,5 +1,42 @@
+type var = int
+
 type t =
-  | Var of int
+  | Var of var
   | Const of string
   | Free of string
   | Function of string * t list
+
+type match_result = All of t | Some of t | None | MatchErr
+
+let merge_result m1 m2 =
+  match (m1, m2) with
+  | All t1, All t2 -> if t1 = t2 then All t1 else MatchErr
+  | All t1, Some _ -> Some t1
+  | Some _, All t2 -> Some t2
+  | Some t1, Some t2 -> if t1 = t2 then Some t1 else MatchErr
+  | None, _ -> m2
+  | _, None -> m1
+  | _ -> MatchErr
+
+let rec match_term x t1 t2 =
+  if x = t1 then if t1 = t2 then Some t2 else All t2
+  else
+    match (t1, t2) with
+    | Var v1, Var v2 -> if v1 = v2 then None else MatchErr
+    | Const s1, Const s2 -> if s1 = s2 then None else MatchErr
+    | Free s1, Free s2 -> if s1 = s2 then None else MatchErr
+    | Function (f1, ts1), Function (f2, ts2) ->
+        if f1 = f2 && List.(length ts1 = length ts2) then
+          List.(map2 (match_term x) ts1 ts2 |> fold_left merge_result None)
+        else MatchErr
+    | _ -> MatchErr
+
+let rec inc_var = function
+  | Var v -> Var (v + 1)
+  | Const s -> Const s
+  | Free s -> Free s
+  | Function (f, ts) -> Function (f, List.map inc_var ts)
+
+let rec occurs t = function
+  | Function (_, ts) -> List.exists (occurs t) ts
+  | s -> t = s

lib/term.mli

@@ -1,5 +1,14 @@
+type var = int
+
 type t =
-  | Var of int
+  | Var of var
   | Const of string
   | Free of string
   | Function of string * t list
+
+type match_result = All of t | Some of t | None | MatchErr
+
+val merge_result : match_result -> match_result -> match_result
+val match_term : t -> t -> t -> match_result
+val inc_var : t -> t
+val occurs : t -> t -> bool