From 21465b897f799264b635a9aee391fc57d7486f2a Mon Sep 17 00:00:00 2001 From: William Ball Date: Fri, 30 Aug 2024 11:43:13 -0700 Subject: [PATCH] done with kernel I think --- lib/formula.ml | 35 +++++++++++++++++++++++++++++++++++ lib/formula.mli | 3 +++ lib/proof.ml | 47 +++++++++++++++++++++++++++++++++++++++-------- lib/term.ml | 39 ++++++++++++++++++++++++++++++++++++++- lib/term.mli | 11 ++++++++++- 5 files changed, 125 insertions(+), 10 deletions(-) diff --git a/lib/formula.ml b/lib/formula.ml index e4b7d57..2639152 100644 --- a/lib/formula.ml +++ b/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 diff --git a/lib/formula.mli b/lib/formula.mli index e4b7d57..1e5861a 100644 --- a/lib/formula.mli +++ b/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 diff --git a/lib/proof.ml b/lib/proof.ml index 52b5264..d92c9a4 100644 --- a/lib/proof.ml +++ b/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 - -(* TODO: - - EqE - - ForallI - - ForallE - - ExistsI - - ExistsE -*) + | [ ({ formula = Equal (t, s); _ } as left); right ], EqE, phi -> ( + valid res a left && valid res a right + && + match Formula.match_term t right.formula phi with + | All s' -> s = s' + | Some s' -> s = s' + | 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 diff --git a/lib/term.ml b/lib/term.ml index 5d9027d..791fc58 100644 --- a/lib/term.ml +++ b/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 diff --git a/lib/term.mli b/lib/term.mli index 5d9027d..e3b9f35 100644 --- a/lib/term.mli +++ b/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