Fix + Add 100/cayley_hamilton.ml to regression

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

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 </ m then
       let th1 = INST [ftm,ifn f_tm; mtm,m_tm; ntm,n_tm] (tfn pth_0) in
       MP th1 (EQT_ELIM(NUM_LT_CONV(lhand(concl th1))))
     else if n = m then CONV_RULE (RAND_CONV(TRY_CONV BETA_CONV))

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 ( </) x y = compare x y = Less;;
-let ( <=/) x y = compare x y <> 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 ( =/) x y = compare x y = 0;;
+let ( <>/) x y = compare x y <> 0;;
 
 let lt_num = ( </);;
 let le_num = ( <=/);;

candle/regression.py

@@ -75,6 +75,7 @@ class TestResult:
     "100/lhopital",
     "100/stirling",
     "100/liouville",
+    "100/cayley_hamilton",
 ]
 
 

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) ->