1 (* ========================================================================= *)
2 (* Knuth-Bendix completion done by HOL inference. John Harrison 2005 *)
4 (* This was written by fairly mechanical modification of the code at *)
6 (* http://www.cl.cam.ac.uk/users/jrh/atp/order.ml *)
7 (* http://www.cl.cam.ac.uk/users/jrh/atp/completion.ml *)
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. *)
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 (* ========================================================================= *)
19 let is_realvar w x = is_var x & not(mem x w);;
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];;
26 (* ------------------------------------------------------------------------- *)
27 (* Construct a weighting function. *)
28 (* ------------------------------------------------------------------------- *)
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;;
34 (* ------------------------------------------------------------------------- *)
35 (* Generic lexicographic ordering function. *)
36 (* ------------------------------------------------------------------------- *)
38 let rec lexord ord l1 l2 =
40 (h1::t1,h2::t2) -> if ord h1 h2 then length t1 = length t2
41 else h1 = h2 & lexord ord t1 t2
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 (* ------------------------------------------------------------------------- *)
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;;
60 (* ------------------------------------------------------------------------- *)
61 (* Unification. Again we have the weights "w" fixing the set of constants. *)
62 (* ------------------------------------------------------------------------- *)
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";;
70 let rec unify w env tp =
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";;
78 (* ------------------------------------------------------------------------- *)
79 (* Full unification, unravelling graph into HOL-style instantiation list. *)
80 (* ------------------------------------------------------------------------- *)
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
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;;
90 (* ------------------------------------------------------------------------- *)
91 (* Construct "overlaps": ways of rewriting subterms using unification. *)
92 (* ------------------------------------------------------------------------- *)
94 let LIST_MK_COMB f ths = rev_itlist (fun s t -> MK_COMB(t,s)) ths (REFL f);;
96 let rec listcases fn rfn lis 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;;
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 _ -> []);;
109 (* ------------------------------------------------------------------------- *)
110 (* Rename variables canonically to avoid clashes or remove redundancy. *)
111 (* ------------------------------------------------------------------------- *)
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;;
119 let renamepair (th1,th2) = fixvariables "x" th1,fixvariables "y" th2;;
121 (* ------------------------------------------------------------------------- *)
122 (* Find all critical pairs. *)
123 (* ------------------------------------------------------------------------- *)
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));;
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
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) []));;
143 (* ------------------------------------------------------------------------- *)
144 (* Normalize an equation and try to orient it. *)
145 (* ------------------------------------------------------------------------- *)
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";;
153 (* ------------------------------------------------------------------------- *)
154 (* Print out status report to reduce user boredom. *)
155 (* ------------------------------------------------------------------------- *)
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");
163 (* ------------------------------------------------------------------------- *)
164 (* Basic completion, throwing back left-reducible rules. *)
165 (* ------------------------------------------------------------------------- *)
167 let left_reducible eqs eq =
168 can (CHANGED_CONV(GEN_REWRITE_CONV (LAND_CONV o ONCE_DEPTH_CONV) eqs))
171 let rec complete w (eqs,crits) =
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
181 ocrits @ crits' @ itlist ((@) o critical_pairs w eq') eqs'' []
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
189 (* ------------------------------------------------------------------------- *)
190 (* Overall completion. *)
191 (* ------------------------------------------------------------------------- *)
193 let complete_equations wts eqs =
194 let eqs' = map (normalize_and_orient wts []) eqs in
195 complete wts ([],eqs');;
197 (* ------------------------------------------------------------------------- *)
198 (* Knuth-Bendix example 4: the inverse property. *)
199 (* ------------------------------------------------------------------------- *)
201 complete_equations [`1`; `(*):num->num->num`; `i:num->num`]
202 [SPEC_ALL(ASSUME `!a b. i(a) * a * b = b`)];;
204 (* ------------------------------------------------------------------------- *)
205 (* Knuth-Bendix example 6: central groupoids. *)
206 (* ------------------------------------------------------------------------- *)
208 complete_equations [`(*):num->num->num`]
209 [SPEC_ALL(ASSUME `!a b c. (a * b) * (b * c) = b`)];;
211 (* ------------------------------------------------------------------------- *)
212 (* Knuth-Bendix example 9: cancellation law. *)
213 (* ------------------------------------------------------------------------- *)
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) /\
221 (!a. 1 * a = a)`)));;
223 (* ------------------------------------------------------------------------- *)
224 (* Another example: pure congruence closure (no variables). *)
225 (* ------------------------------------------------------------------------- *)
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)`)));;
231 (* ------------------------------------------------------------------------- *)
232 (* Knuth-Bendix example 1: group theory. *)
233 (* ------------------------------------------------------------------------- *)
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)`));;
239 complete_equations [`1`; `(*):num->num->num`; `i:num->num`] eqs;;
241 (* ------------------------------------------------------------------------- *)
242 (* Near-rings (from Aichinger's Diplomarbeit). *)
243 (* ------------------------------------------------------------------------- *)
245 let eqs = map SPEC_ALL (CONJUNCTS (ASSUME
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))`));;
254 [`0`; `(+):num->num->num`; `neg:num->num`; `( * ):num->num->num`] eqs;;
256 (*** This weighting also works OK, though the system is a bit bigger
260 [`0`; `(+):num->num->num`; `( * ):num->num->num`; `INV`] eqs;;
264 (* ------------------------------------------------------------------------- *)
265 (* A "completion" tactic. *)
266 (* ------------------------------------------------------------------------- *)
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';;
273 (* ------------------------------------------------------------------------- *)
274 (* Solve example problems in groups and near-rings. *)
275 (* ------------------------------------------------------------------------- *)
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`;;
282 e (DISCH_THEN(COMPLETE_TAC [`1`; `(*):num->num->num`; `i:num->num`]));;
283 e (ASM_REWRITE_TAC[]);;
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) =
293 e (DISCH_THEN(COMPLETE_TAC
294 [`0`; `(+):num->num->num`; `neg:num->num`; `( * ):num->num->num`]));;
295 e (ASM_REWRITE_TAC[]);;