1 (* Copyright (C) 2002, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
33 (** perform debugging output? *)
36 (** debugging print *)
39 prerr_endline ("RING WARNING: " ^ s)
44 Note: For constructors URIs aren't really URIs but rather triples of
45 the form (uri, typeno, consno). This discrepancy is to preserver an
46 uniformity of invocation of "mkXXX" functions.
49 let eqt_uri = uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind"
50 let refl_eqt_uri = (eqt_uri, 0, 1)
52 uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/sym_eqT.con"
53 let bool_uri = uri_of_string "cic:/Coq/Init/Datatypes/bool.ind"
54 let true_uri = (bool_uri, 0, 1)
55 let false_uri = (bool_uri, 0, 2)
57 let r_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/R.con"
58 let rplus_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/Rplus.con"
59 let rmult_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/Rmult.con"
60 let ropp_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/Ropp.con"
61 let r0_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/R0.con"
62 let r1_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/R1.con"
63 let rtheory_uri = uri_of_string "cic:/Coq/Reals/Rbase/RTheory.con"
67 "cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind"
68 let apvar_uri = (apolynomial_uri, 0, 1)
69 let ap0_uri = (apolynomial_uri, 0, 2)
70 let ap1_uri = (apolynomial_uri, 0, 3)
71 let applus_uri = (apolynomial_uri, 0, 4)
72 let apmult_uri = (apolynomial_uri, 0, 5)
73 let apopp_uri = (apolynomial_uri, 0, 6)
76 uri_of_string "cic:/Coq/ring/Quote/variables_map/varmap.ind"
77 let empty_vm_uri = (varmap_uri, 0, 1)
78 let node_vm_uri = (varmap_uri, 0, 2)
80 uri_of_string "cic:/Coq/ring/Quote/variables_map/varmap_find.con"
82 uri_of_string "cic:/Coq/ring/Quote/variables_map/index.ind"
83 let left_idx_uri = (index_uri, 0, 1)
84 let right_idx_uri = (index_uri, 0, 2)
85 let end_idx_uri = (index_uri, 0, 3)
88 uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/interp_ap.con"
90 uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/interp_sacs.con"
91 let apolynomial_normalize_uri =
93 "cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial_normalize.con"
94 let apolynomial_normalize_ok_uri =
96 "cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial_normalize_ok.con"
101 "Some" constructor's inverse
102 @raise Failure "unsome" if None is passed
104 let unsome = function None -> failwith "unsome" | Some item -> item
106 (** CIC PREDICATES *)
109 check whether a term is a constant or not, if argument "uri" is given and is
110 not "None" also check if the constant correspond to the given one or not
112 let cic_is_const ?(uri: uri option = None) term =
116 | Cic.Const _ -> true
120 | Cic.Const (u, _) when (eq u realuri) -> true
123 (** PROOF AND GOAL ACCESSORS *)
127 @return the uri of a given proof
129 let uri_of_proof ~proof:(uri, _, _, _) = uri
132 @param metano meta list index
133 @param metasenv meta list (environment)
134 @raise Failure if metano is not found in metasenv
135 @return conjecture corresponding to metano in metasenv
137 let conj_of_metano metano =
139 List.find (function (m, _, _) -> m = metano)
142 "Ring.conj_of_metano: " ^
143 (string_of_int metano) ^ " no such meta")
146 @param status current proof engine status
147 @raise Failure if proof is None
148 @return current goal's metasenv
150 let metasenv_of_status ~status:(proof, goal) =
152 | None -> failwith "Ring.metasenv_of_status invoked on None goal"
153 | Some (_, m, _, _) -> m
156 @param status a proof engine status
157 @raise Failure when proof or goal are None
158 @return context corresponding to current goal
160 let context_of_status ~status:(proof, goal) =
161 let metasenv = metasenv_of_status ~status:(proof, goal) in
164 | None -> failwith "Ring.context_of_status invoked on None goal"
165 | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
169 (** CIC TERM CONSTRUCTORS *)
172 Create a Cic term consisting of a constant
173 @param uri URI of the constant
176 let mkConst ~uri ~proof =
177 let cookingsno = relative_depth (uri_of_proof ~proof) uri 0 in
178 Cic.Const (uri, cookingsno)
181 Create a Cic term consisting of a constructor
182 @param uri triple <uri, typeno, consno> where uri is the uri of an inductive
183 type, typeno is the type number in a mutind structure (0 based), consno is
184 the constructor number (1 based)
185 @param proof current proof
187 let mkCtor ~uri:(uri, typeno, consno) ~proof =
188 let cookingsno = relative_depth (uri_of_proof ~proof) uri 0 in
189 Cic.MutConstruct (uri, cookingsno, typeno, consno)
192 Create a Cic term consisting of a type member of a mutual induction
193 @param uri pair <uri, typeno> where uri is the uri of a mutual inductive
194 type and typeno is the type number (0 based) in the mutual induction
196 let mkMutInd ~uri:(uri, typeno) ~proof =
197 let cookingsno = relative_depth (uri_of_proof ~proof) uri 0 in
198 Cic.MutInd (uri, cookingsno, typeno)
203 raised when the current goal is not ringable; a goal is ringable when is an
204 equality on reals (@see r_uri)
206 exception GoalUnringable
208 (** RING's FUNCTIONS LIBRARY *)
211 Check whether the ring tactic can be applied on a given term (i.e. that is
212 an equality on reals)
213 @param term term to be tested
214 @return true if the term is ringable, false otherwise
217 let is_equality = function
218 | Cic.MutInd uri _ 0 when (eq uri eqt_uri) -> true
221 let is_real = function
222 | Cic.Const (uri, _) when (eq uri r_uri) -> true
226 | Cic.Appl (app::set::_::_::[]) when (is_equality app && is_real set) ->
227 warn "Goal Ringable!";
230 warn "Goal Not Ringable :-((";
234 split an equality goal of the form "t1 = t2" in its two subterms t1 and t2
235 after checking that the goal is ringable
236 @param goal the current goal
237 @return a pair (t1,t2) that are two sides of the equality goal
238 @raise GoalUnringable if the goal isn't ringable
240 let split_eq = function
241 | (Cic.Appl (_::_::t1::t2::[])) as term when ringable term ->
242 warn ("<term1>" ^ (CicPp.ppterm t1) ^ "</term1>");
243 warn ("<term2>" ^ (CicPp.ppterm t2) ^ "</term2>");
245 | _ -> raise GoalUnringable
248 @param i an integer index representing a 1 based number of node in a binary
249 search tree counted in a fbs manner (i.e.: 1 is the root, 2 is the left
250 child of the root (if any), 3 is the right child of the root (if any), 4 is
251 the left child of the left child of the root (if any), ....)
252 @param proof the current proof
253 @return an index representing the same node in a varmap (@see varmap_uri),
254 the returned index is as defined in index (@see index_uri)
256 let path_of_int n proof =
257 let rec digits_of_int n =
258 if n=1 then [] else (n mod 2 = 1)::(digits_of_int (n lsr 1))
263 mkCtor (if (digit = true) then right_idx_uri else left_idx_uri) proof;
265 (List.rev (digits_of_int n)) (* remove leading true (i.e. digit 1) *)
266 (mkCtor end_idx_uri proof)
269 Build a variable map (@see varmap_uri) from a variables array.
270 A variable map is almost a binary tree so this function receiving a var list
271 like [v;w;x;y;z] will build a varmap of shape: v
276 @param vars variables array
277 @param proof current proof
278 @return a cic term representing the variable map containing vars variables
280 let btree_of_array ~vars ~proof =
281 let r = mkConst r_uri proof in (* cic objects *)
282 let empty_vm = mkCtor empty_vm_uri proof in
283 let empty_vm_r = Cic.Appl [empty_vm; r] in
284 let node_vm = mkCtor node_vm_uri proof in
285 let node_vm_r = Cic.Appl [node_vm; r] in
286 let size = Array.length vars in
287 let halfsize = size lsr 1 in
288 let rec aux n = (* build the btree starting from position n *)
290 n is the position in the vars array _1_based_ in order to access
291 left and right child using (n*2, n*2+1) trick
295 else if n > halfsize then (* no more children *)
296 Cic.Appl [node_vm; r; vars.(n-1); empty_vm_r; empty_vm_r]
297 else (* still children *)
298 Cic.Appl [node_vm; r; vars.(n-1); aux (n*2); aux (n*2+1)]
303 abstraction function:
304 concrete polynoms -----> (abstract polynoms, varmap)
305 @param terms list of conrete polynoms
306 @param proof current proof
307 @return a pair <aterms, varmap> where aterms is a list of abstract polynoms
308 and varmap is the variable map needed to interpret them
310 let abstract_poly ~terms ~proof =
311 let varhash = Hashtbl.create 19 in (* vars hash, to speed up lookup *)
312 let varlist = ref [] in (* vars list in reverse order *)
313 let counter = ref 1 in (* index of next new variable *)
314 let rec aux = function (* TODO not tail recursive *)
315 (* "bop" -> binary operator | "uop" -> unary operator *)
316 | Cic.Appl (bop::t1::t2::[])
317 when (cic_is_const ~uri:(Some rplus_uri) bop) -> (* +. *)
318 Cic.Appl [mkCtor applus_uri proof; aux t1; aux t2]
319 | Cic.Appl (bop::t1::t2::[])
320 when (cic_is_const ~uri:(Some rmult_uri) bop) -> (* *. *)
321 Cic.Appl [mkCtor apmult_uri proof; aux t1; aux t2]
322 | Cic.Appl (uop::t::[])
323 when (cic_is_const ~uri:(Some ropp_uri) uop) -> (* ~-. *)
324 Cic.Appl [mkCtor apopp_uri proof; aux t]
325 | t when (cic_is_const ~uri:(Some r0_uri) t) -> (* 0. *)
327 | t when (cic_is_const ~uri:(Some r1_uri) t) -> (* 1. *)
329 | t -> (* variable *)
331 Hashtbl.find varhash t (* use an old var *)
332 with Not_found -> begin (* create a new var *)
334 Cic.Appl [mkCtor apvar_uri proof; path_of_int !counter proof]
337 varlist := t :: !varlist;
338 Hashtbl.add varhash t newvar;
343 btree_of_array ~vars:(Array.of_list (List.rev !varlist)) ~proof)
346 given a list of abstract terms (i.e. apolynomials) build the ring "segments"
347 that is triples like (t', t'', t''') where
348 t' = interp_ap(varmap, at)
349 t'' = interp_sacs(varmap, (apolynomial_normalize at))
350 t''' = apolynomial_normalize_ok(varmap, at)
351 at is the abstract term built from t, t is a single member of aterms
353 let build_segments ~terms ~proof =
354 let r = mkConst r_uri proof in (* cic objects *)
355 let rplus = mkConst rplus_uri proof in
356 let rmult = mkConst rmult_uri proof in
357 let ropp = mkConst ropp_uri proof in
358 let r0 = mkConst r0_uri proof in
359 let r1 = mkConst r1_uri proof in
360 let interp_ap = mkConst interp_ap_uri proof in
361 let interp_sacs = mkConst interp_sacs_uri proof in
362 let apolynomial_normalize = mkConst apolynomial_normalize_uri proof in
363 let apolynomial_normalize_ok = mkConst apolynomial_normalize_ok_uri proof in
364 let rtheory = mkConst rtheory_uri proof in
365 let lxy_false = (** Cic funcion "fun (x,y):R -> false" *)
366 Cic.Lambda (Cic.Anonimous, r,
367 Cic.Lambda (Cic.Anonimous, r,
368 mkCtor false_uri proof))
370 let theory_args = [r; rplus; rmult; r1; r0; ropp] in
371 let (aterms, varmap) = abstract_poly ~terms ~proof in (* abstract polys *)
372 List.map (* build ring segments *)
374 Cic.Appl ((interp_ap :: theory_args) @ [varmap; t]),
378 [varmap; Cic.Appl [apolynomial_normalize; t]])),
380 (apolynomial_normalize_ok :: theory_args) @
381 [lxy_false; varmap; rtheory; t]))
384 (** AUX TACTIC{,AL}S *)
387 naive implementation of ORELSE tactical, try a sequence of tactics in turn:
388 if one fails pass to the next one and so on, eventually raises (failure "no
390 TODO warning: not tail recursive due to "try .. with" boxing
392 let rec try_tactics ~(tactics: (string * tactic) list) ~status =
393 warn "in Ring.try_tactics";
395 | (descr, tac)::tactics ->
396 warn ("Ring.try_tactics IS TRYING " ^ descr);
398 let res = tac ~status in
399 warn ("Ring.try_tactics: " ^ descr ^ " succedeed!!!");
402 | (Fail _) as e -> begin (* TODO: codice replicato perche' non funge il
403 binding multiplo con "as" *)
405 "Ring.try_tactics failed with exn: " ^
406 Printexc.to_string e);
407 try_tactics ~tactics ~status
409 | (CicTypeChecker.NotWellTyped _) as e -> begin (* TODO: si puo' togliere? *)
411 "Ring.try_tactics failed with exn: " ^
412 Printexc.to_string e);
413 try_tactics ~tactics ~status
415 | (CicUnification.UnificationFailed) as e -> begin
417 "Ring.try_tactics failed with exn: " ^
418 Printexc.to_string e);
419 try_tactics ~tactics ~status
422 | [] -> raise (Fail "try_tactics: no tactics left")
425 auxiliary tactic "elim_type"
426 @param status current proof engine status
427 @param term term to cut
429 let elim_type_tac ~status ~term =
430 warn "in Ring.elim_type_tac";
431 let status' = cut_tac ~term ~status in
432 elim_intros_simpl_tac ~term:(Cic.Rel 1) ~status:status'
436 @param status current proof engine status
438 let next_goal ~status =
439 warn "in Ring.next_goal";
441 | ((Some (_, metasenv, _, _)) as proof, goal) ->
443 | _::(n, _, _)::_ -> (proof, Some n)
444 | _ -> raise (Fail "No other goal available"))
448 auxiliary tactic, use elim_type and try to close 2nd subgoal using proof
449 @param status current proof engine status
450 @param term term to cut
451 @param proof term used to prove second subgoal generated by elim_type
453 let elim_type2_tac ~status ~term ~proof =
454 exact_tac ~term:proof ~status:(next_goal (elim_type_tac ~term ~status))
457 Reflexivity tactic, try to solve current goal using "refl_eqT"
458 Warning: this isn't equale to the coq's Reflexivity because this one tries
459 only refl_eqT, coq's one also try "refl_equal"
460 @param status current proof engine status
462 let reflexivity_tac ~status:(proof, goal) =
463 warn "in Ring.reflexivity_tac";
464 let refl_eqt = mkCtor ~uri:refl_eqt_uri ~proof:(unsome proof) in
466 apply_tac ~status:(proof, goal) ~term:refl_eqt
467 with (Fail _) as e ->
468 let e_str = Printexc.to_string e in
469 raise (Fail ("Reflexivity failed with exception: " ^ e_str))
471 (** lift an 8-uple of debrujins indexes of n *)
472 let lift ~n (a,b,c,d,e,f,g,h) =
473 match (List.map (CicSubstitution.lift n) [a;b;c;d;e;f;g;h]) with
474 | [a;b;c;d;e;f;g;h] -> (a,b,c,d,e,f,g,h)
478 remove hypothesis from a given status starting from the last one
479 @param count number of hypotheses to remove
480 @param status current proof engine status
482 let purge_hyps ~count ~status:(proof, goal) =
483 let module S = ProofEngineStructuralRules in
484 let rec aux n context status =
486 match (n, context) with
488 | (n, hd::tl) -> aux (n-1) tl (S.clear ~status ~hyp:hd)
489 | (_, []) -> failwith "Ring.purge_hyps: no hypotheses left"
493 | None -> failwith "Ring.purge_hyps invoked on None goal"
497 | None -> failwith "Ring.purge_hyps invoked on None proof"
498 | Some (_, metasenv, _, _) ->
499 let (_, context, _) = conj_of_metano metano metasenv in
500 aux count context (proof, goal)
505 Ring tactic, does associative and commutative rewritings in Reals ring
506 @param status current proof engine status
508 let ring_tac ~status:(proof, goal) =
509 warn "in Ring tactic";
510 let status = (proof, goal) in
511 let (proof, goal) = (unsome proof), (unsome goal) in
512 let eqt = mkMutInd (eqt_uri, 0) proof in
513 let r = mkConst r_uri proof in
514 let metasenv = metasenv_of_status ~status in
515 let (metano, context, ty) = conj_of_metano goal metasenv in
516 let (t1, t2) = split_eq ty in (* goal like t1 = t2 *)
517 match (build_segments ~terms:[t1; t2] ~proof) with
518 | (t1', t1'', t1'_eq_t1'')::(t2', t2'', t2'_eq_t2'')::[] -> begin
519 List.iter (* debugging, feel free to remove *)
520 (fun (descr, term) ->
521 warn (descr ^ " " ^ (CicPp.ppterm term)))
523 ["t1"; "t1'"; "t1''"; "t1'_eq_t1''";
524 "t2"; "t2'"; "t2''"; "t2'_eq_t2''"]
525 [t1; t1'; t1''; t1'_eq_t1'';
526 t2; t2'; t2''; t2'_eq_t2'']);
528 let new_hyps = ref 0 in (* number of new hypotheses created *)
532 "reflexivity", reflexivity_tac;
533 "exact t1'_eq_t1''", exact_tac ~term:t1'_eq_t1'';
534 "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2'';
535 "exact sym_eqt su t1 ...", exact_tac ~term:(
537 mkConst sym_eqt_uri proof; mkConst r_uri proof;
538 t1''; t1; t1'_eq_t1'']);
539 "elim_type eqt su t1 ...", (fun ~status ->
540 let status' = (* status after 1st elim_type use *)
541 let context = context_of_status ~status in
542 if not (are_convertible context t1'' t1) then begin
543 warn "t1'' and t1 are NOT CONVERTIBLE";
545 elim_type2_tac (* 1st elim_type use *)
546 ~status ~proof:t1'_eq_t1''
547 ~term:(Cic.Appl [eqt; r; t1''; t1])
549 incr new_hyps; (* elim_type add an hyp *)
552 warn "t1'' and t1 are CONVERTIBLE";
556 let (t1,t1',t1'',t1'_eq_t1'',t2,t2',t2'',t2'_eq_t2'') =
557 lift 1 (t1,t1',t1'',t1'_eq_t1'', t2,t2',t2'',t2'_eq_t2'')
560 try_tactics (* try to solve 1st subgoal *)
563 "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2'';
564 "exact sym_eqt su t2 ...",
567 mkConst sym_eqt_uri proof;
569 t2''; t2; t2'_eq_t2'']);
570 "elim_type eqt su t2 ...", (fun ~status ->
572 let context = context_of_status ~status in
573 if not (are_convertible context t2'' t2) then begin
574 warn "t2'' and t2 are NOT CONVERTIBLE";
576 elim_type2_tac (* 2nd elim_type use *)
577 ~status ~proof:t2'_eq_t2''
578 ~term:(Cic.Appl [eqt; r; t2''; t2])
580 incr new_hyps; (* elim_type add an hyp *)
583 warn "t2'' and t2 are CONVERTIBLE";
587 try (* try to solve main goal *)
588 warn "trying reflexivity ....";
589 reflexivity_tac ~status:status'
590 with (Fail _) -> (* leave conclusion to the user *)
591 warn "reflexivity failed, solution's left as an ex :-)";
592 purge_hyps ~count:!new_hyps ~status:status')]
596 raise (Fail "Ring failure")
598 | _ -> (* impossible: we are applying ring exacty to 2 terms *)
601 (* wrap ring_tac catching GoalUnringable and raising Fail *)
602 let ring_tac ~status =
605 with GoalUnringable ->
606 raise (Fail "goal unringable")