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/.
31 open HelmLibraryObjects
35 (** perform debugging output? *)
38 (** debugging print *)
41 prerr_endline ("RING WARNING: " ^ s)
46 Note: For constructors URIs aren't really URIs but rather triples of
47 the form (uri, typeno, consno). This discrepancy is to preserver an
48 uniformity of invocation of "mkXXX" functions.
51 let equality_is_a_congruence_A =
52 uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/A.var"
53 let equality_is_a_congruence_x =
54 uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/x.var"
55 let equality_is_a_congruence_y =
56 uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/y.var"
59 uri_of_string "cic:/Coq/ring/Ring_abstract/apolynomial.ind"
60 let apvar_uri = (apolynomial_uri, 0, 1)
61 let ap0_uri = (apolynomial_uri, 0, 2)
62 let ap1_uri = (apolynomial_uri, 0, 3)
63 let applus_uri = (apolynomial_uri, 0, 4)
64 let apmult_uri = (apolynomial_uri, 0, 5)
65 let apopp_uri = (apolynomial_uri, 0, 6)
67 let quote_varmap_A_uri = uri_of_string "cic:/Coq/ring/Quote/variables_map/A.var"
68 let varmap_uri = uri_of_string "cic:/Coq/ring/Quote/varmap.ind"
69 let empty_vm_uri = (varmap_uri, 0, 1)
70 let node_vm_uri = (varmap_uri, 0, 2)
71 let varmap_find_uri = uri_of_string "cic:/Coq/ring/Quote/varmap_find.con"
72 let index_uri = uri_of_string "cic:/Coq/ring/Quote/index.ind"
73 let left_idx_uri = (index_uri, 0, 1)
74 let right_idx_uri = (index_uri, 0, 2)
75 let end_idx_uri = (index_uri, 0, 3)
77 let abstract_rings_A_uri =
78 uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/A.var"
79 let abstract_rings_Aplus_uri =
80 uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Aplus.var"
81 let abstract_rings_Amult_uri =
82 uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Amult.var"
83 let abstract_rings_Aone_uri =
84 uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Aone.var"
85 let abstract_rings_Azero_uri =
86 uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Azero.var"
87 let abstract_rings_Aopp_uri =
88 uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Aopp.var"
89 let abstract_rings_Aeq_uri =
90 uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Aeq.var"
91 let abstract_rings_vm_uri =
92 uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/vm.var"
93 let abstract_rings_T_uri =
94 uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/T.var"
95 let interp_ap_uri = uri_of_string "cic:/Coq/ring/Ring_abstract/interp_ap.con"
97 uri_of_string "cic:/Coq/ring/Ring_abstract/interp_sacs.con"
98 let apolynomial_normalize_uri =
99 uri_of_string "cic:/Coq/ring/Ring_abstract/apolynomial_normalize.con"
100 let apolynomial_normalize_ok_uri =
101 uri_of_string "cic:/Coq/ring/Ring_abstract/apolynomial_normalize_ok.con"
103 (** CIC PREDICATES *)
106 check whether a term is a constant or not, if argument "uri" is given and is
107 not "None" also check if the constant correspond to the given one or not
109 let cic_is_const ?(uri: uri option = None) term =
113 | Cic.Const _ -> true
117 | Cic.Const (u, _) when (eq u realuri) -> true
120 (** PROOF AND GOAL ACCESSORS *)
124 @return the uri of a given proof
126 let uri_of_proof ~proof:(uri, _, _, _) = uri
129 @param metano meta list index
130 @param metasenv meta list (environment)
131 @raise Failure if metano is not found in metasenv
132 @return conjecture corresponding to metano in metasenv
134 let conj_of_metano metano =
136 List.find (function (m, _, _) -> m = metano)
139 "Ring.conj_of_metano: " ^
140 (string_of_int metano) ^ " no such meta")
143 @param status current proof engine status
144 @raise Failure if proof is None
145 @return current goal's metasenv
147 let metasenv_of_status ~status:((_,m,_,_), _) = m
150 @param status a proof engine status
151 @raise Failure when proof or goal are None
152 @return context corresponding to current goal
154 let context_of_status ~status:(proof, goal as status) =
155 let metasenv = metasenv_of_status ~status:status in
156 let _, context, _ = List.find (function (m,_,_) -> m=goal) metasenv in
159 (** CIC TERM CONSTRUCTORS *)
162 Create a Cic term consisting of a constant
163 @param uri URI of the constant
165 @exp_named_subst explicit named substitution
167 let mkConst ~uri ~exp_named_subst =
168 Cic.Const (uri, exp_named_subst)
171 Create a Cic term consisting of a constructor
172 @param uri triple <uri, typeno, consno> where uri is the uri of an inductive
173 type, typeno is the type number in a mutind structure (0 based), consno is
174 the constructor number (1 based)
175 @exp_named_subst explicit named substitution
177 let mkCtor ~uri:(uri, typeno, consno) ~exp_named_subst =
178 Cic.MutConstruct (uri, typeno, consno, exp_named_subst)
181 Create a Cic term consisting of a type member of a mutual induction
182 @param uri pair <uri, typeno> where uri is the uri of a mutual inductive
183 type and typeno is the type number (0 based) in the mutual induction
184 @exp_named_subst explicit named substitution
186 let mkMutInd ~uri:(uri, typeno) ~exp_named_subst =
187 Cic.MutInd (uri, typeno, exp_named_subst)
192 raised when the current goal is not ringable; a goal is ringable when is an
193 equality on reals (@see r_uri)
195 exception GoalUnringable
197 (** RING's FUNCTIONS LIBRARY *)
200 Check whether the ring tactic can be applied on a given term (i.e. that is
201 an equality on reals)
202 @param term to be tested
203 @return true if the term is ringable, false otherwise
206 let is_equality = function
207 | Cic.MutInd (uri, 0, []) when (eq uri Logic_Type.eqt_URI) -> true
210 let is_real = function
211 | Cic.Const (uri, _) when (eq uri Reals.r_URI) -> true
215 | Cic.Appl (app::set::_::_::[]) when (is_equality app && is_real set) ->
216 warn "Goal Ringable!";
219 warn "Goal Not Ringable :-((";
223 split an equality goal of the form "t1 = t2" in its two subterms t1 and t2
224 after checking that the goal is ringable
225 @param goal the current goal
226 @return a pair (t1,t2) that are two sides of the equality goal
227 @raise GoalUnringable if the goal isn't ringable
229 let split_eq = function
230 | (Cic.Appl (_::_::t1::t2::[])) as term when ringable term ->
231 warn ("<term1>" ^ (CicPp.ppterm t1) ^ "</term1>");
232 warn ("<term2>" ^ (CicPp.ppterm t2) ^ "</term2>");
234 | _ -> raise GoalUnringable
237 @param i an integer index representing a 1 based number of node in a binary
238 search tree counted in a fbs manner (i.e.: 1 is the root, 2 is the left
239 child of the root (if any), 3 is the right child of the root (if any), 4 is
240 the left child of the left child of the root (if any), ....)
241 @param proof the current proof
242 @return an index representing the same node in a varmap (@see varmap_uri),
243 the returned index is as defined in index (@see index_uri)
246 let rec digits_of_int n =
247 if n=1 then [] else (n mod 2 = 1)::(digits_of_int (n lsr 1))
252 mkCtor (if (digit = true) then right_idx_uri else left_idx_uri) [];
254 (List.rev (digits_of_int n)) (* remove leading true (i.e. digit 1) *)
255 (mkCtor end_idx_uri [])
258 Build a variable map (@see varmap_uri) from a variables array.
259 A variable map is almost a binary tree so this function receiving a var list
260 like [v;w;x;y;z] will build a varmap of shape: v
265 @param vars variables array
266 @return a cic term representing the variable map containing vars variables
268 let btree_of_array ~vars =
270 let empty_vm_r = mkCtor empty_vm_uri [quote_varmap_A_uri,r] in
271 let node_vm_r = mkCtor node_vm_uri [quote_varmap_A_uri,r] in
272 let size = Array.length vars in
273 let halfsize = size lsr 1 in
274 let rec aux n = (* build the btree starting from position n *)
276 n is the position in the vars array _1_based_ in order to access
277 left and right child using (n*2, n*2+1) trick
281 else if n > halfsize then (* no more children *)
282 Cic.Appl [node_vm_r; vars.(n-1); empty_vm_r; empty_vm_r]
283 else (* still children *)
284 Cic.Appl [node_vm_r; vars.(n-1); aux (n*2); aux (n*2+1)]
289 abstraction function:
290 concrete polynoms -----> (abstract polynoms, varmap)
291 @param terms list of conrete polynoms
292 @return a pair <aterms, varmap> where aterms is a list of abstract polynoms
293 and varmap is the variable map needed to interpret them
295 let abstract_poly ~terms =
296 let varhash = Hashtbl.create 19 in (* vars hash, to speed up lookup *)
297 let varlist = ref [] in (* vars list in reverse order *)
298 let counter = ref 1 in (* index of next new variable *)
299 let rec aux = function (* TODO not tail recursive *)
300 (* "bop" -> binary operator | "uop" -> unary operator *)
301 | Cic.Appl (bop::t1::t2::[])
302 when (cic_is_const ~uri:(Some Reals.rplus_URI) bop) -> (* +. *)
303 Cic.Appl [mkCtor applus_uri []; aux t1; aux t2]
304 | Cic.Appl (bop::t1::t2::[])
305 when (cic_is_const ~uri:(Some Reals.rmult_URI) bop) -> (* *. *)
306 Cic.Appl [mkCtor apmult_uri []; aux t1; aux t2]
307 | Cic.Appl (uop::t::[])
308 when (cic_is_const ~uri:(Some Reals.ropp_URI) uop) -> (* ~-. *)
309 Cic.Appl [mkCtor apopp_uri []; aux t]
310 | t when (cic_is_const ~uri:(Some Reals.r0_URI) t) -> (* 0. *)
312 | t when (cic_is_const ~uri:(Some Reals.r1_URI) t) -> (* 1. *)
314 | t -> (* variable *)
316 Hashtbl.find varhash t (* use an old var *)
317 with Not_found -> begin (* create a new var *)
319 Cic.Appl [mkCtor apvar_uri []; path_of_int !counter]
322 varlist := t :: !varlist;
323 Hashtbl.add varhash t newvar;
327 let aterms = List.map aux terms in (* abstract vars *)
328 let varmap = (* build varmap *)
329 btree_of_array ~vars:(Array.of_list (List.rev !varlist))
334 given a list of abstract terms (i.e. apolynomials) build the ring "segments"
335 that is triples like (t', t'', t''') where
336 t' = interp_ap(varmap, at)
337 t'' = interp_sacs(varmap, (apolynomial_normalize at))
338 t''' = apolynomial_normalize_ok(varmap, at)
339 at is the abstract term built from t, t is a single member of aterms
341 let build_segments ~terms =
342 let theory_args_subst varmap =
343 [abstract_rings_A_uri, Reals.r ;
344 abstract_rings_Aplus_uri, Reals.rplus ;
345 abstract_rings_Amult_uri, Reals.rmult ;
346 abstract_rings_Aone_uri, Reals.r1 ;
347 abstract_rings_Azero_uri, Reals.r0 ;
348 abstract_rings_Aopp_uri, Reals.ropp ;
349 abstract_rings_vm_uri, varmap] in
350 let theory_args_subst' eq varmap t =
351 [abstract_rings_A_uri, Reals.r ;
352 abstract_rings_Aplus_uri, Reals.rplus ;
353 abstract_rings_Amult_uri, Reals.rmult ;
354 abstract_rings_Aone_uri, Reals.r1 ;
355 abstract_rings_Azero_uri, Reals.r0 ;
356 abstract_rings_Aopp_uri, Reals.ropp ;
357 abstract_rings_Aeq_uri, eq ;
358 abstract_rings_vm_uri, varmap ;
359 abstract_rings_T_uri, t] in
360 let interp_ap varmap =
361 mkConst interp_ap_uri (theory_args_subst varmap) in
362 let interp_sacs varmap =
363 mkConst interp_sacs_uri (theory_args_subst varmap) in
364 let apolynomial_normalize = mkConst apolynomial_normalize_uri [] in
365 let apolynomial_normalize_ok eq varmap t =
366 mkConst apolynomial_normalize_ok_uri (theory_args_subst' eq varmap t) in
367 let lxy_false = (** Cic funcion "fun (x,y):R -> false" *)
368 Cic.Lambda (Cic.Anonymous, Reals.r,
369 Cic.Lambda (Cic.Anonymous, Reals.r, Datatypes.falseb))
371 let (aterms, varmap) = abstract_poly ~terms in (* abstract polys *)
372 List.map (* build ring segments *)
374 Cic.Appl [interp_ap varmap ; t],
376 [interp_sacs varmap ; Cic.Appl [apolynomial_normalize; t]]),
377 Cic.Appl [apolynomial_normalize_ok lxy_false varmap Reals.rtheory ; t]
381 let status_of_single_goal_tactic_result =
383 proof,[goal] -> proof,goal
385 raise (Fail "status_of_single_goal_tactic_result: the tactic did not produce exactly a new goal")
387 (* Galla: spostata in variousTactics.ml
389 auxiliary tactic "elim_type"
390 @param status current proof engine status
391 @param term term to cut
393 let elim_type_tac ~term ~status =
394 warn "in Ring.elim_type_tac";
395 Tacticals.thens ~start:(cut_tac ~term)
396 ~continuations:[elim_simpl_intros_tac ~term:(Cic.Rel 1) ; Tacticals.id_tac] ~status
400 auxiliary tactic, use elim_type and try to close 2nd subgoal using proof
401 @param status current proof engine status
402 @param term term to cut
403 @param proof term used to prove second subgoal generated by elim_type
405 let elim_type2_tac ~term ~proof ~status =
406 let module E = EliminationTactics in
407 warn "in Ring.elim_type2";
408 Tacticals.thens ~start:(E.elim_type_tac ~term)
409 ~continuations:[Tacticals.id_tac ; exact_tac ~term:proof] ~status
411 (* Galla: spostata in variousTactics.ml
413 Reflexivity tactic, try to solve current goal using "refl_eqT"
414 Warning: this isn't equale to the coq's Reflexivity because this one tries
415 only refl_eqT, coq's one also try "refl_equal"
416 @param status current proof engine status
418 let reflexivity_tac ~status:(proof, goal) =
419 warn "in Ring.reflexivity_tac";
420 let refl_eqt = mkCtor ~uri:refl_eqt_uri ~exp_named_subst:[] in
422 apply_tac ~status:(proof, goal) ~term:refl_eqt
423 with (Fail _) as e ->
424 let e_str = Printexc.to_string e in
425 raise (Fail ("Reflexivity failed with exception: " ^ e_str))
428 (** lift an 8-uple of debrujins indexes of n *)
429 let lift ~n (a,b,c,d,e,f,g,h) =
430 match (List.map (CicSubstitution.lift n) [a;b;c;d;e;f;g;h]) with
431 | [a;b;c;d;e;f;g;h] -> (a,b,c,d,e,f,g,h)
435 remove hypothesis from a given status starting from the last one
436 @param count number of hypotheses to remove
437 @param status current proof engine status
439 let purge_hyps_tac ~count ~status:(proof, goal as status) =
440 let module S = ProofEngineStructuralRules in
441 let rec aux n context status =
443 match (n, context) with
447 (status_of_single_goal_tactic_result (S.clear ~hyp:hd ~status))
448 | (_, []) -> failwith "Ring.purge_hyps_tac: no hypotheses left"
450 let (_, metasenv, _, _) = proof in
451 let (_, context, _) = conj_of_metano goal metasenv in
452 let proof',goal' = aux count context status in
453 assert (goal = goal') ;
459 Ring tactic, does associative and commutative rewritings in Reals ring
460 @param status current proof engine status
462 let ring_tac ~status:((proof, goal) as status) =
463 warn "in Ring tactic";
464 let eqt = mkMutInd (Logic_Type.eqt_URI, 0) [] in
466 let metasenv = metasenv_of_status ~status in
467 let (metano, context, ty) = conj_of_metano goal metasenv in
468 let (t1, t2) = split_eq ty in (* goal like t1 = t2 *)
469 match (build_segments ~terms:[t1; t2]) with
470 | (t1', t1'', t1'_eq_t1'')::(t2', t2'', t2'_eq_t2'')::[] -> begin
471 List.iter (* debugging, feel free to remove *)
472 (fun (descr, term) ->
473 warn (descr ^ " " ^ (CicPp.ppterm term)))
475 ["t1"; "t1'"; "t1''"; "t1'_eq_t1''";
476 "t2"; "t2'"; "t2''"; "t2'_eq_t2''"]
477 [t1; t1'; t1''; t1'_eq_t1'';
478 t2; t2'; t2''; t2'_eq_t2'']);
480 let new_hyps = ref 0 in (* number of new hypotheses created *)
481 Tacticals.try_tactics
484 "reflexivity", EqualityTactics.reflexivity_tac ;
485 "exact t1'_eq_t1''", exact_tac ~term:t1'_eq_t1'' ;
486 "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2'' ;
487 "exact sym_eqt su t1 ...", exact_tac
490 [mkConst Logic_Type.sym_eqt_URI
491 [equality_is_a_congruence_A, Reals.r;
492 equality_is_a_congruence_x, t1'' ;
493 equality_is_a_congruence_y, t1
497 "elim_type eqt su t1 ...", (fun ~status ->
498 let status' = (* status after 1st elim_type use *)
499 let context = context_of_status ~status in
500 if not (are_convertible context t1'' t1) then begin
501 warn "t1'' and t1 are NOT CONVERTIBLE";
503 elim_type2_tac (* 1st elim_type use *)
504 ~status ~proof:t1'_eq_t1''
505 ~term:(Cic.Appl [eqt; r; t1''; t1])
507 incr new_hyps; (* elim_type add an hyp *)
509 (proof,[goal]) -> proof,goal
512 warn "t1'' and t1 are CONVERTIBLE";
516 let (t1,t1',t1'',t1'_eq_t1'',t2,t2',t2'',t2'_eq_t2'') =
517 lift 1 (t1,t1',t1'',t1'_eq_t1'', t2,t2',t2'',t2'_eq_t2'')
520 Tacticals.try_tactics (* try to solve 1st subgoal *)
523 "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2'';
524 "exact sym_eqt su t2 ...",
528 [mkConst Logic_Type.sym_eqt_URI
529 [equality_is_a_congruence_A, Reals.r;
530 equality_is_a_congruence_x, t2'' ;
531 equality_is_a_congruence_y, t2
535 "elim_type eqt su t2 ...", (fun ~status ->
537 let context = context_of_status ~status in
538 if not (are_convertible context t2'' t2) then begin
539 warn "t2'' and t2 are NOT CONVERTIBLE";
541 elim_type2_tac (* 2nd elim_type use *)
542 ~status ~proof:t2'_eq_t2''
543 ~term:(Cic.Appl [eqt; r; t2''; t2])
545 incr new_hyps; (* elim_type add an hyp *)
547 (proof,[goal]) -> proof,goal
550 warn "t2'' and t2 are CONVERTIBLE";
554 try (* try to solve main goal *)
555 warn "trying reflexivity ....";
556 EqualityTactics.reflexivity_tac ~status:status'
557 with (Fail _) -> (* leave conclusion to the user *)
558 warn "reflexivity failed, solution's left as an ex :-)";
559 purge_hyps_tac ~count:!new_hyps ~status:status')]
563 raise (Fail ("Ring failure: " ^ s))
565 | _ -> (* impossible: we are applying ring exacty to 2 terms *)
568 (* wrap ring_tac catching GoalUnringable and raising Fail *)
569 let ring_tac ~status =
572 with GoalUnringable ->
573 raise (Fail "goal unringable")