Examples/kb.ml

   1 (* ========================================================================= *)
   2 (* Knuth-Bendix completion done by HOL inference. John Harrison 2005         *)
   3 (*                                                                           *)
   4 (* This was written by fairly mechanical modification of the code at         *)
   5 (*                                                                           *)
   6 (*   http://www.cl.cam.ac.uk/users/jrh/atp/order.ml                          *)
   7 (*   http://www.cl.cam.ac.uk/users/jrh/atp/completion.ml                     *)
   8 (*                                                                           *)
   9 (* for HOL's slightly different term structure, with ad hoc term             *)
  10 (* manipulations replaced by inference on equational theorems. We also have  *)
  11 (* the optimization of throwing left-reducible rules back into the set of    *)
  12 (* critical pairs. However, we don't prioritize smaller critical pairs or    *)
  13 (* anything like that; this is still a very naive implementation.            *)
  14 (*                                                                           *)
  15 (* For something very similar done 15 years ago, see Konrad Slind's Master's *)
  16 (* thesis: "An Implementation of Higher Order Logic", U Calgary 1991.        *)
  17 (* ========================================================================= *)
  18
  19 let is_realvar w x = is_var x & not(mem x w);;
  20
  21 let rec real_strip w tm =
  22   if mem tm w then tm,[] else
  23   let l,r = dest_comb tm in
  24   let f,args = real_strip w l in f,args@[r];;
  25
  26 (* ------------------------------------------------------------------------- *)
  27 (* Construct a weighting function.                                           *)
  28 (* ------------------------------------------------------------------------- *)
  29
  30 let weight lis (f,n) (g,m) =
  31   let i = index f lis and j = index g lis in
  32   i > j or i = j & n > m;;
  33
  34 (* ------------------------------------------------------------------------- *)
  35 (* Generic lexicographic ordering function.                                  *)
  36 (* ------------------------------------------------------------------------- *)
  37
  38 let rec lexord ord l1 l2 =
  39   match (l1,l2) with
  40     (h1::t1,h2::t2) -> if ord h1 h2 then length t1 = length t2
  41                        else h1 = h2 & lexord ord t1 t2
  42   | _ -> false;;
  43
  44 (* ------------------------------------------------------------------------- *)
  45 (* Lexicographic path ordering. Note that we also use the weights            *)
  46 (* to define the set of constants, so they don't literally have to be        *)
  47 (* constants in the HOL sense.                                               *)
  48 (* ------------------------------------------------------------------------- *)
  49
  50 let rec lpo_gt w s t =
  51   if is_realvar w t then not(s = t) & mem t (frees s)
  52   else if is_realvar w s or is_abs s or is_abs t then false else
  53   let f,fargs = real_strip w s and g,gargs = real_strip w t in
  54   exists (fun si -> lpo_ge w si t) fargs or
  55         forall (lpo_gt w s) gargs &
  56         (f = g & lexord (lpo_gt w) fargs gargs or
  57          weight w (f,length fargs) (g,length gargs))
  58 and lpo_ge w s t = (s = t) or lpo_gt w s t;;
  59
  60 (* ------------------------------------------------------------------------- *)
  61 (* Unification. Again we have the weights "w" fixing the set of constants.   *)
  62 (* ------------------------------------------------------------------------- *)
  63
  64 let rec istriv w env x t =
  65   if is_realvar w t then t = x or defined env t & istriv w env x (apply env t)
  66   else if is_const t then false else
  67   let f,args = strip_comb t in
  68   exists (istriv w env x) args & failwith "cyclic";;
  69
  70 let rec unify w env tp =
  71   match tp with
  72    ((Var(_,_) as x),t) | (t,(Var(_,_) as x)) when not(mem x w) ->
  73         if defined env x then unify w env (apply env x,t)
  74         else if istriv w env x t then env else (x|->t) env
  75   | (Comb(f,x),Comb(g,y)) -> unify w (unify w env (x,y)) (f,g)
  76   | (s,t) -> if s = t then env else failwith "unify: not unifiable";;
  77
  78 (* ------------------------------------------------------------------------- *)
  79 (* Full unification, unravelling graph into HOL-style instantiation list.    *)
  80 (* ------------------------------------------------------------------------- *)
  81
  82 let fullunify w (s,t) =
  83   let env = unify w undefined (s,t) in
  84   let th = map (fun (x,t) -> (t,x)) (graph env) in
  85   let rec subs t =
  86     let t' = vsubst th t in
  87     if t' = t then t else subs t' in
  88   map (fun (t,x) -> (subs t,x)) th;;
  89
  90 (* ------------------------------------------------------------------------- *)
  91 (* Construct "overlaps": ways of rewriting subterms using unification.       *)
  92 (* ------------------------------------------------------------------------- *)
  93
  94 let LIST_MK_COMB f ths = rev_itlist (fun s t -> MK_COMB(t,s)) ths (REFL f);;
  95
  96 let rec listcases fn rfn lis acc =
  97   match lis with
  98     [] -> acc
  99   | h::t -> fn h (fun i h' -> rfn i (h'::map REFL t)) @
 100             listcases fn (fun i t' -> rfn i (REFL h::t')) t acc;;
 101
 102 let rec overlaps w th tm rfn =
 103   let l,r = dest_eq(concl th) in
 104   if not (is_comb tm) then [] else
 105   let f,args = strip_comb tm in
 106   listcases (overlaps w th) (fun i a -> rfn i (LIST_MK_COMB f a)) args
 107             (try [rfn (fullunify w (l,tm)) th] with Failure _ -> []);;
 108
 109 (* ------------------------------------------------------------------------- *)
 110 (* Rename variables canonically to avoid clashes or remove redundancy.       *)
 111 (* ------------------------------------------------------------------------- *)
 112
 113 let fixvariables s th =
 114   let fvs = subtract (frees(concl th)) (freesl(hyp th)) in
 115   let gvs = map2 (fun v n -> mk_var(s^string_of_int n,type_of v))
 116                  fvs (1--(length fvs)) in
 117   INST (zip gvs fvs) th;;
 118
 119 let renamepair (th1,th2) = fixvariables "x" th1,fixvariables "y" th2;;
 120
 121 (* ------------------------------------------------------------------------- *)
 122 (* Find all critical pairs.                                                  *)
 123 (* ------------------------------------------------------------------------- *)
 124
 125 let crit1 w eq1 eq2 =
 126   let l1,r1 = dest_eq(concl eq1)
 127   and l2,r2 = dest_eq(concl eq2) in
 128   overlaps w eq1 l2 (fun i th -> TRANS (SYM(INST i th)) (INST i eq2));;
 129
 130 let thm_union l1 l2 =
 131   itlist (fun th ths -> let th' = fixvariables "x" th in
 132                         let tm = concl th' in
 133                         if exists (fun th'' -> concl th'' = tm) ths then ths
 134                         else th'::ths)
 135          l1 l2;;
 136
 137 let critical_pairs w tha thb =
 138   let th1,th2 = renamepair (tha,thb) in
 139   if concl th1 = concl th2 then crit1 w th1 th2 else
 140   filter (fun th -> let l,r = dest_eq(concl th) in l <> r)
 141          (thm_union (crit1 w th1 th2) (thm_union (crit1 w th2 th1) []));;
 142
 143 (* ------------------------------------------------------------------------- *)
 144 (* Normalize an equation and try to orient it.                               *)
 145 (* ------------------------------------------------------------------------- *)
 146
 147 let normalize_and_orient w eqs th =
 148   let th' = GEN_REWRITE_RULE TOP_DEPTH_CONV eqs th in
 149   let s',t' = dest_eq(concl th') in
 150   if lpo_ge w s' t' then th' else if lpo_ge w t' s' then SYM th'
 151   else failwith "Can't orient equation";;
 152
 153 (* ------------------------------------------------------------------------- *)
 154 (* Print out status report to reduce user boredom.                           *)
 155 (* ------------------------------------------------------------------------- *)
 156
 157 let status(eqs,crs) eqs0 =
 158   if eqs = eqs0 & (length crs) mod 1000 <> 0 then () else
 159   (print_string(string_of_int(length eqs)^" equations and "^
 160                 string_of_int(length crs)^" pending critical pairs");
 161    print_newline());;
 162
 163 (* ------------------------------------------------------------------------- *)
 164 (* Basic completion, throwing back left-reducible rules.                     *)
 165 (* ------------------------------------------------------------------------- *)
 166
 167 let left_reducible eqs eq =
 168   can (CHANGED_CONV(GEN_REWRITE_CONV (LAND_CONV o ONCE_DEPTH_CONV) eqs))
 169       (concl eq);;
 170
 171 let rec complete w (eqs,crits) =
 172   match crits with
 173     (eq::ocrits) ->
 174         let trip =
 175           try let eq' = normalize_and_orient w eqs eq in
 176               let s',t' = dest_eq(concl eq') in
 177               if s' = t' then (eqs,ocrits) else
 178               let crits',eqs' = partition(left_reducible [eq']) eqs in
 179               let eqs'' = eq'::eqs' in
 180               eqs'',
 181               ocrits @ crits' @ itlist ((@) o critical_pairs w eq') eqs'' []
 182           with Failure _ ->
 183               if exists (can (normalize_and_orient w eqs)) ocrits
 184               then (eqs,ocrits@[eq])
 185               else failwith "complete: no orientable equations" in
 186         status trip eqs; complete w trip
 187   | [] -> eqs;;
 188
 189 (* ------------------------------------------------------------------------- *)
 190 (* Overall completion.                                                       *)
 191 (* ------------------------------------------------------------------------- *)
 192
 193 let complete_equations wts eqs =
 194   let eqs' = map (normalize_and_orient wts []) eqs in
 195   complete wts ([],eqs');;
 196
 197 (* ------------------------------------------------------------------------- *)
 198 (* Knuth-Bendix example 4: the inverse property.                             *)
 199 (* ------------------------------------------------------------------------- *)
 200
 201 complete_equations [`1`; `(*):num->num->num`; `i:num->num`]
 202   [SPEC_ALL(ASSUME `!a b. i(a) * a * b = b`)];;
 203
 204 (* ------------------------------------------------------------------------- *)
 205 (* Knuth-Bendix example 6: central groupoids.                                *)
 206 (* ------------------------------------------------------------------------- *)
 207
 208 complete_equations [`(*):num->num->num`]
 209  [SPEC_ALL(ASSUME `!a b c. (a * b) * (b * c) = b`)];;
 210
 211 (* ------------------------------------------------------------------------- *)
 212 (* Knuth-Bendix example 9: cancellation law.                                 *)
 213 (* ------------------------------------------------------------------------- *)
 214
 215 complete_equations
 216  [`1`; `( * ):num->num->num`; `(+):num->num->num`; `(-):num->num->num`]
 217  (map SPEC_ALL (CONJUNCTS (ASSUME
 218   `(!a b:num. a - a * b = b) /\
 219    (!a b:num. a * b - b = a) /\
 220    (!a. a * 1 = a) /\
 221    (!a. 1 * a = a)`)));;
 222
 223 (* ------------------------------------------------------------------------- *)
 224 (* Another example: pure congruence closure (no variables).                  *)
 225 (* ------------------------------------------------------------------------- *)
 226
 227 complete_equations [`c:A`; `f:A->A`]
 228  (map SPEC_ALL (CONJUNCTS (ASSUME
 229    `((f(f(f(f(f c))))) = c:A) /\ (f(f(f c)) = c)`)));;
 230
 231 (* ------------------------------------------------------------------------- *)
 232 (* Knuth-Bendix example 1: group theory.                                     *)
 233 (* ------------------------------------------------------------------------- *)
 234
 235 let eqs = map SPEC_ALL (CONJUNCTS (ASSUME
 236   `(!x. 1 * x = x) /\ (!x. i(x) * x = 1) /\
 237    (!x y z. (x * y) * z = x * y * z)`));;
 238
 239 complete_equations [`1`; `(*):num->num->num`; `i:num->num`] eqs;;
 240
 241 (* ------------------------------------------------------------------------- *)
 242 (* Near-rings (from Aichinger's Diplomarbeit).                               *)
 243 (* ------------------------------------------------------------------------- *)
 244
 245 let eqs = map SPEC_ALL (CONJUNCTS (ASSUME
 246   `(!x. 0 + x = x) /\
 247    (!x. neg x + x = 0) /\
 248    (!x y z. (x + y) + z = x + y + z) /\
 249    (!x y z. (x * y) * z = x * y * z) /\
 250    (!x y z. (x + y) * z = (x * z) + (y * z))`));;
 251
 252 let nreqs =
 253 complete_equations
 254   [`0`; `(+):num->num->num`; `neg:num->num`; `( * ):num->num->num`] eqs;;
 255
 256 (*** This weighting also works OK, though the system is a bit bigger
 257
 258 let nreqs =
 259 complete_equations
 260   [`0`; `(+):num->num->num`; `( * ):num->num->num`; `INV`] eqs;;
 261
 262 ****)
 263
 264 (* ------------------------------------------------------------------------- *)
 265 (* A "completion" tactic.                                                    *)
 266 (* ------------------------------------------------------------------------- *)
 267
 268 let COMPLETE_TAC w th =
 269   let eqs = map SPEC_ALL (CONJUNCTS(SPEC_ALL th)) in
 270   let eqs' = complete_equations w eqs in
 271   MAP_EVERY (ASSUME_TAC o GEN_ALL) eqs';;
 272
 273 (* ------------------------------------------------------------------------- *)
 274 (* Solve example problems in groups and near-rings.                          *)
 275 (* ------------------------------------------------------------------------- *)
 276
 277 g `(!x. 1 * x = x) /\
 278    (!x. i(x) * x = 1) /\
 279    (!x y z. (x * y) * z = x * y * z)
 280    ==> !x y. i(y) * i(i(i(x * i(y)))) * x = 1`;;
 281
 282 e (DISCH_THEN(COMPLETE_TAC [`1`; `(*):num->num->num`; `i:num->num`]));;
 283 e (ASM_REWRITE_TAC[]);;
 284
 285 g `(!x. 0 + x = x) /\
 286    (!x. neg x + x = 0) /\
 287    (!x y z. (x + y) + z = x + y + z) /\
 288    (!x y z. (x * y) * z = x * y * z) /\
 289    (!x y z. (x + y) * z = (x * z) + (y * z))
 290    ==> (neg 0  * (x * y + z + neg(neg(w + z))) + neg(neg b + neg a) =
 291         a + b)`;;
 292
 293 e (DISCH_THEN(COMPLETE_TAC
 294      [`0`; `(+):num->num->num`; `neg:num->num`; `( * ):num->num->num`]));;
 295 e (ASM_REWRITE_TAC[]);;