From 116d57ae14362b10a217278cf99f075c7b147359 Mon Sep 17 00:00:00 2001 From: Daniel Nezamabadi <55559979+dnezam@users.noreply.github.com> Date: Fri, 17 Apr 2026 09:58:36 +0800 Subject: [PATCH 1/5] candle/nums.ml: change comparisons to return int instead of order --- candle/nums.ml | 24 +++++++++++++----------- 1 file changed, 13 insertions(+), 11 deletions(-) diff --git a/candle/nums.ml b/candle/nums.ml index 30258644..b3c8797a 100644 --- a/candle/nums.ml +++ b/candle/nums.ml @@ -45,7 +45,7 @@ module type NUM = sig val min_num : num -> num -> num val max_num : num -> num -> num - val compare : num -> num -> order + val compare : num -> num -> int val gcd_num : num -> num -> num val ( **/) : num -> num -> num @@ -220,19 +220,21 @@ let floor_num n = ;; let compare x y = + let rat_compare x y = + if Cake.Rat.(<) x y then -1 else if Cake.Rat.(>) x y then 1 else 0 in match x, y with - | Int i, Int j -> Cake.Int.compare i j - | Int i, Rat r -> Cake.Rat.compare (Cake.Rat.fromInt i) r - | Rat r, Int j -> Cake.Rat.compare r (Cake.Rat.fromInt j) - | Rat i, Rat j -> Cake.Rat.compare i j + | Int i, Int j -> if i < j then -1 else if i > j then 1 else 0 + | Int i, Rat r -> rat_compare (Cake.Rat.fromInt i) r + | Rat r, Int j -> rat_compare r (Cake.Rat.fromInt j) + | Rat i, Rat j -> rat_compare i j ;; -let ( Greater;; -let ( >/) x y = compare x y = Greater;; -let ( >=/) x y = compare x y <> Less;; -let ( =/) x y = compare x y = Equal;; -let ( <>/) x y = compare x y <> Equal;; +let ( /) x y = compare x y > 0;; +let ( >=/) x y = compare x y >= 0;; +let ( =/) x y = compare x y = 0;; +let ( <>/) x y = compare x y <> 0;; let lt_num = ( Date: Fri, 17 Apr 2026 12:22:35 +0800 Subject: [PATCH 2/5] Fix Multivariate/vectors.ml --- Multivariate/vectors.ml | 36 +++++++++++++++++++++--------------- 1 file changed, 21 insertions(+), 15 deletions(-) diff --git a/Multivariate/vectors.ml b/Multivariate/vectors.ml index b54a81bc..b75a3506 100644 --- a/Multivariate/vectors.ml +++ b/Multivariate/vectors.ml @@ -725,11 +725,15 @@ let NORM_ARITH = augment_norm (rat_of_term c >=/ num 0) n acc | _ -> augment_norm true tm acc in find_normedterms in - let lincomb_neg t = mapf minus_num t in - let lincomb_cmul c t = if c =/ num 0 then undefined else mapf (( */ ) c) t in - let lincomb_add l r = combine (+/) (fun x -> x =/ num 0) l r in + (* Due to the lack of let-polymorphism in Candle, we avoid type variables + here to avoid confusing problems down the road. *) + let lincomb_neg (t: (term,num) func) = mapf minus_num t in + let lincomb_cmul c t = + if c =/ num 0 then undefined Term.compare else mapf (( */ ) c) t in + let lincomb_add (l: (term,num) func) r = + combine (+/) (fun x -> x =/ num 0) l r in let lincomb_sub l r = lincomb_add l (lincomb_neg r) in - let lincomb_eq l r = lincomb_sub l r = undefined in + let lincomb_eq l r = lincomb_sub l r = undefined Term.compare in let rec vector_lincomb tm = match tm with Comb(Comb(Const("vector_add",_),l),r) -> @@ -741,8 +745,8 @@ let NORM_ARITH = | Comb(Const("vector_neg",_),t) -> lincomb_neg (vector_lincomb t) | Comb(Const("vec",_),n) when is_numeral n && dest_numeral n =/ num 0 -> - undefined - | _ -> (tm |=> num 1) in + undefined Term.compare + | _ -> (tm |=> num 1) Term.compare in let vector_lincombs tms = itlist (fun t fns -> if can (assoc t) fns then fns else @@ -767,8 +771,10 @@ let NORM_ARITH = let evaluate env lin = foldr (fun x c s -> s +/ c */ apply env x) lin (num 0) in let rec solve (vs,eqs) = + let lincomb_add l r = combine (+/) (fun x -> x =/ num 0) l r in + let lincomb_cmul c t = if c =/ num 0 then undefined Int.compare else mapf (( */ ) c) t in match (vs,eqs) with - [],[] -> (0 |=> num 1) + [],[] -> (0 |=> num 1) Int.compare | _,eq::oeqs -> let v = hd(intersect vs (dom eq)) in let c = apply eq v in @@ -872,10 +878,10 @@ let NORM_ARITH = match tm with Comb(Comb(Const("vector_add",_),lt),rt) -> let l = headvector lt and r = headvector rt in - if l < r then (APPLY_pthb THENC + if Term.(<) l r then (APPLY_pthb THENC RAND_CONV VECTOR_ADD_CONV THENC APPLY_pthd) tm - else if r < l then (APPLY_pthc THENC + else if Term.(<) r l then (APPLY_pthc THENC RAND_CONV VECTOR_ADD_CONV THENC APPLY_pthd) tm else (APPLY_pth9 THENC @@ -910,7 +916,7 @@ let NORM_ARITH = let sources = map (rand o rand o concl) nubs and rawdests = itlist (find_normedterms o lhand o concl) (ges @ gts) [] in if not (forall fst rawdests) then failwith "Sanity check" else - let dests = setify (map snd rawdests) in + let dests = setify Term.(<=) (map snd rawdests) in let srcfuns = map vector_lincomb sources and destfuns = map vector_lincomb dests in let vvs = itlist (union o dom) (srcfuns @ destfuns) [] in @@ -919,18 +925,18 @@ let NORM_ARITH = let srccombs = zip srcfuns nvs in let consider d = let coefficients x = - let inp = if defined d x then 0 |=> minus_num(apply d x) - else undefined in + let inp = if defined d x then (0 |=> minus_num(apply d x)) Int.compare + else undefined Int.compare in itlist (fun (f,v) g -> if defined f x then (v |-> apply f x) g else g) srccombs inp in let equations = map coefficients vvs - and inequalities = map (fun n -> (n |=> num 1)) nvs in + and inequalities = map (fun n -> (n |=> num 1) Int.compare) nvs in let plausiblevertices f = let flippedequations = map (itlist flip f) equations in let constraints = flippedequations @ inequalities in let rawverts = vertices nvs constraints in let check_solution v = - let f = itlist2 (|->) nvs v (0 |=> num 1) in + let f = itlist2 (|->) nvs v ((0 |=> num 1) Int.compare) in forall (fun e -> evaluate f e =/ num 0) flippedequations in let goodverts = filter check_solution rawverts in let signfixups = map (fun n -> if mem n f then -1 else 1) nvs in @@ -1818,7 +1824,7 @@ let EXPAND_VSUM_CONV = let nty = hd(tl(snd(dest_type(snd(dest_fun_ty(type_of ftm)))))) in let ilist = [nty,n_ty] in let ifn = inst ilist and tfn = INST_TYPE ilist in - if n < m then + if n Date: Fri, 17 Apr 2026 19:56:56 +0800 Subject: [PATCH 3/5] Uncomment assoceq in grobner.ml This fixes Multivariate/determinants.ml, which previously got stuck at Generating HOL version of proof. --- grobner.ml | 21 ++++++++++++--------- 1 file changed, 12 insertions(+), 9 deletions(-) diff --git a/grobner.ml b/grobner.ml index 06556132..0c8b18b6 100644 --- a/grobner.ml +++ b/grobner.ml @@ -481,21 +481,19 @@ let RING_AND_IDEAL_CONV = CONV_RULE (BINOP_CONV RING_NORMALIZE_CONV) (AP_TERM (mk_comb(ring_mul_tm,holify_polynomial vars [m])) th) in - (* OA Lack of pointer equality makes this useless in Candle, - and lack of let polymorphism gets type checking to fail - on this definition. *) - (* let rec assoceq a l = - match l with - [] -> failwith "assoceq" - | (x,y)::t -> if x==a then y else assoceq a t in *) let run_proof = if is_iff(snd(strip_forall(concl RABINOWITSCH_THM))) then (Format.print_string("Generating HOL version of proof"); Format.print_newline(); let execache = ref [] in let memoize prf x = (execache := (prf,x)::(!execache)); x in + (* Copied due to current lack of let polymorphism *) + let rec assoceq a l = + match l with + [] -> failwith "assoceq" + | (x,y)::t -> if x = a then y else assoceq a t in let rec run_proof vars prf = - (* try assoceq prf (!execache) with Failure _ -> *) + try assoceq prf (!execache) with Failure _ -> (match prf with Start m -> el m initpols | Add(p1,p2) -> @@ -511,8 +509,13 @@ let RING_AND_IDEAL_CONV = let km = map (fun x -> 0) vars in let execache = ref [] in let memoize prf x = (execache := (prf,x)::(!execache)); x in + (* Copied due to current lack of let polymorphism *) + let rec assoceq a l = + match l with + [] -> failwith "assoceq" + | (x,y)::t -> if x = a then y else assoceq a t in let rec run_scaled_proof vars prf = - (* try assoceq prf (!execache) with Failure _ -> *) + try assoceq prf (!execache) with Failure _ -> (match prf with Start m -> (num_1,el m initpols) | Add(p1,p2) -> From d944eb63fa1424008ecad1026df9c96abe29fdd9 Mon Sep 17 00:00:00 2001 From: Daniel Nezamabadi <55559979+dnezam@users.noreply.github.com> Date: Fri, 17 Apr 2026 20:26:56 +0800 Subject: [PATCH 4/5] Fix Multivariate/complexes.ml --- Multivariate/complexes.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Multivariate/complexes.ml b/Multivariate/complexes.ml index 11505b68..1846288a 100644 --- a/Multivariate/complexes.ml +++ b/Multivariate/complexes.ml @@ -685,7 +685,7 @@ let COMPLEX_POLY_NEG_CONV,COMPLEX_POLY_ADD_CONV,COMPLEX_POLY_SUB_CONV, SEMIRING_NORMALIZERS_CONV COMPLEX_POLY_CLAUSES COMPLEX_POLY_NEG_CLAUSES (is_complex_const, COMPLEX_RAT_ADD_CONV,COMPLEX_RAT_MUL_CONV,COMPLEX_RAT_POW_CONV) - (<);; + Term.(<);; (* ------------------------------------------------------------------------- *) (* Extend it to handle "inv" and division, by constants after normalization. *) @@ -874,7 +874,7 @@ let COMPLEX_FIELD = not(is_ratconst(rand tm)) in let BASIC_COMPLEX_FIELD tm = let is_freeinv t = is_inv t && free_in t tm in - let itms = setify(map rand (find_terms is_freeinv tm)) in + let itms = setify Term.(<=) (map rand (find_terms is_freeinv tm)) in let hyps = map (fun t -> CONV_RULE easy_nz_conv (SPEC t COMPLEX_MUL_RINV)) itms in let tm' = itlist (fun th t -> mk_imp(concl th,t)) hyps tm in From 60aa98f1cc87a2cd8f8b1ff1422ea45cfb50a55a Mon Sep 17 00:00:00 2001 From: Daniel Nezamabadi <55559979+dnezam@users.noreply.github.com> Date: Fri, 17 Apr 2026 20:30:49 +0800 Subject: [PATCH 5/5] Add 100/cayley_hamilton to regression --- candle/regression.py | 1 + 1 file changed, 1 insertion(+) diff --git a/candle/regression.py b/candle/regression.py index 2962c5c6..c5b47a77 100644 --- a/candle/regression.py +++ b/candle/regression.py @@ -75,6 +75,7 @@ class TestResult: "100/lhopital", "100/stirling", "100/liouville", + "100/cayley_hamilton", ]