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)
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"
57 let sym_eqt_uri = uri_of_string "cic:/Coq/Init/Logic_Type/sym_eqT.con"
58 let bool_uri = uri_of_string "cic:/Coq/Init/Datatypes/bool.ind"
59 let true_uri = (bool_uri, 0, 1)
60 let false_uri = (bool_uri, 0, 2)
62 let r_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/R.con"
63 let rplus_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/Rplus.con"
64 let rmult_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/Rmult.con"
65 let ropp_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/Ropp.con"
66 let r0_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/R0.con"
67 let r1_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/R1.con"
68 let rtheory_uri = uri_of_string "cic:/Coq/Reals/Rbase/RTheory.con"
71 uri_of_string "cic:/Coq/ring/Ring_abstract/apolynomial.ind"
72 let apvar_uri = (apolynomial_uri, 0, 1)
73 let ap0_uri = (apolynomial_uri, 0, 2)
74 let ap1_uri = (apolynomial_uri, 0, 3)
75 let applus_uri = (apolynomial_uri, 0, 4)
76 let apmult_uri = (apolynomial_uri, 0, 5)
77 let apopp_uri = (apolynomial_uri, 0, 6)
79 let quote_varmap_A_uri = uri_of_string "cic:/Coq/ring/Quote/variables_map/A.var"
80 let varmap_uri = uri_of_string "cic:/Coq/ring/Quote/varmap.ind"
81 let empty_vm_uri = (varmap_uri, 0, 1)
82 let node_vm_uri = (varmap_uri, 0, 2)
83 let varmap_find_uri = uri_of_string "cic:/Coq/ring/Quote/varmap_find.con"
84 let index_uri = uri_of_string "cic:/Coq/ring/Quote/index.ind"
85 let left_idx_uri = (index_uri, 0, 1)
86 let right_idx_uri = (index_uri, 0, 2)
87 let end_idx_uri = (index_uri, 0, 3)
89 let abstract_rings_A_uri =
90 uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/A.var"
91 let abstract_rings_Aplus_uri =
92 uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Aplus.var"
93 let abstract_rings_Amult_uri =
94 uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Amult.var"
95 let abstract_rings_Aone_uri =
96 uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Aone.var"
97 let abstract_rings_Azero_uri =
98 uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Azero.var"
99 let abstract_rings_Aopp_uri =
100 uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Aopp.var"
101 let abstract_rings_Aeq_uri =
102 uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Aeq.var"
103 let abstract_rings_vm_uri =
104 uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/vm.var"
105 let abstract_rings_T_uri =
106 uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/T.var"
107 let interp_ap_uri = uri_of_string "cic:/Coq/ring/Ring_abstract/interp_ap.con"
108 let interp_sacs_uri =
109 uri_of_string "cic:/Coq/ring/Ring_abstract/interp_sacs.con"
110 let apolynomial_normalize_uri =
111 uri_of_string "cic:/Coq/ring/Ring_abstract/apolynomial_normalize.con"
112 let apolynomial_normalize_ok_uri =
113 uri_of_string "cic:/Coq/ring/Ring_abstract/apolynomial_normalize_ok.con"
115 (** CIC PREDICATES *)
118 check whether a term is a constant or not, if argument "uri" is given and is
119 not "None" also check if the constant correspond to the given one or not
121 let cic_is_const ?(uri: uri option = None) term =
125 | Cic.Const _ -> true
129 | Cic.Const (u, _) when (eq u realuri) -> true
132 (** PROOF AND GOAL ACCESSORS *)
136 @return the uri of a given proof
138 let uri_of_proof ~proof:(uri, _, _, _) = uri
141 @param metano meta list index
142 @param metasenv meta list (environment)
143 @raise Failure if metano is not found in metasenv
144 @return conjecture corresponding to metano in metasenv
146 let conj_of_metano metano =
148 List.find (function (m, _, _) -> m = metano)
151 "Ring.conj_of_metano: " ^
152 (string_of_int metano) ^ " no such meta")
155 @param status current proof engine status
156 @raise Failure if proof is None
157 @return current goal's metasenv
159 let metasenv_of_status ~status:((_,m,_,_), _) = m
162 @param status a proof engine status
163 @raise Failure when proof or goal are None
164 @return context corresponding to current goal
166 let context_of_status ~status:(proof, goal as status) =
167 let metasenv = metasenv_of_status ~status:status in
168 let _, context, _ = List.find (function (m,_,_) -> m=goal) metasenv in
171 (** CIC TERM CONSTRUCTORS *)
174 Create a Cic term consisting of a constant
175 @param uri URI of the constant
177 @exp_named_subst explicit named substitution
179 let mkConst ~uri ~exp_named_subst =
180 Cic.Const (uri, exp_named_subst)
183 Create a Cic term consisting of a constructor
184 @param uri triple <uri, typeno, consno> where uri is the uri of an inductive
185 type, typeno is the type number in a mutind structure (0 based), consno is
186 the constructor number (1 based)
187 @exp_named_subst explicit named substitution
189 let mkCtor ~uri:(uri, typeno, consno) ~exp_named_subst =
190 Cic.MutConstruct (uri, typeno, consno, exp_named_subst)
193 Create a Cic term consisting of a type member of a mutual induction
194 @param uri pair <uri, typeno> where uri is the uri of a mutual inductive
195 type and typeno is the type number (0 based) in the mutual induction
196 @exp_named_subst explicit named substitution
198 let mkMutInd ~uri:(uri, typeno) ~exp_named_subst =
199 Cic.MutInd (uri, typeno, exp_named_subst)
204 raised when the current goal is not ringable; a goal is ringable when is an
205 equality on reals (@see r_uri)
207 exception GoalUnringable
209 (** RING's FUNCTIONS LIBRARY *)
212 Check whether the ring tactic can be applied on a given term (i.e. that is
213 an equality on reals)
214 @param term to be tested
215 @return true if the term is ringable, false otherwise
218 let is_equality = function
219 | Cic.MutInd uri 0 [] when (eq uri eqt_uri) -> true
222 let is_real = function
223 | Cic.Const (uri, _) when (eq uri r_uri) -> true
227 | Cic.Appl (app::set::_::_::[]) when (is_equality app && is_real set) ->
228 warn "Goal Ringable!";
231 warn "Goal Not Ringable :-((";
235 split an equality goal of the form "t1 = t2" in its two subterms t1 and t2
236 after checking that the goal is ringable
237 @param goal the current goal
238 @return a pair (t1,t2) that are two sides of the equality goal
239 @raise GoalUnringable if the goal isn't ringable
241 let split_eq = function
242 | (Cic.Appl (_::_::t1::t2::[])) as term when ringable term ->
243 warn ("<term1>" ^ (CicPp.ppterm t1) ^ "</term1>");
244 warn ("<term2>" ^ (CicPp.ppterm t2) ^ "</term2>");
246 | _ -> raise GoalUnringable
249 @param i an integer index representing a 1 based number of node in a binary
250 search tree counted in a fbs manner (i.e.: 1 is the root, 2 is the left
251 child of the root (if any), 3 is the right child of the root (if any), 4 is
252 the left child of the left child of the root (if any), ....)
253 @param proof the current proof
254 @return an index representing the same node in a varmap (@see varmap_uri),
255 the returned index is as defined in index (@see index_uri)
258 let rec digits_of_int n =
259 if n=1 then [] else (n mod 2 = 1)::(digits_of_int (n lsr 1))
264 mkCtor (if (digit = true) then right_idx_uri else left_idx_uri) [];
266 (List.rev (digits_of_int n)) (* remove leading true (i.e. digit 1) *)
267 (mkCtor end_idx_uri [])
270 Build a variable map (@see varmap_uri) from a variables array.
271 A variable map is almost a binary tree so this function receiving a var list
272 like [v;w;x;y;z] will build a varmap of shape: v
277 @param vars variables array
278 @return a cic term representing the variable map containing vars variables
280 let btree_of_array ~vars =
281 let r = mkConst r_uri [] in (* cic objects *)
282 let empty_vm_r = mkCtor empty_vm_uri [quote_varmap_A_uri,r] in
283 let node_vm_r = mkCtor node_vm_uri [quote_varmap_A_uri,r] in
284 let size = Array.length vars in
285 let halfsize = size lsr 1 in
286 let rec aux n = (* build the btree starting from position n *)
288 n is the position in the vars array _1_based_ in order to access
289 left and right child using (n*2, n*2+1) trick
293 else if n > halfsize then (* no more children *)
294 Cic.Appl [node_vm_r; vars.(n-1); empty_vm_r; empty_vm_r]
295 else (* still children *)
296 Cic.Appl [node_vm_r; vars.(n-1); aux (n*2); aux (n*2+1)]
301 abstraction function:
302 concrete polynoms -----> (abstract polynoms, varmap)
303 @param terms list of conrete polynoms
304 @return a pair <aterms, varmap> where aterms is a list of abstract polynoms
305 and varmap is the variable map needed to interpret them
307 let abstract_poly ~terms =
308 let varhash = Hashtbl.create 19 in (* vars hash, to speed up lookup *)
309 let varlist = ref [] in (* vars list in reverse order *)
310 let counter = ref 1 in (* index of next new variable *)
311 let rec aux = function (* TODO not tail recursive *)
312 (* "bop" -> binary operator | "uop" -> unary operator *)
313 | Cic.Appl (bop::t1::t2::[])
314 when (cic_is_const ~uri:(Some rplus_uri) bop) -> (* +. *)
315 Cic.Appl [mkCtor applus_uri []; aux t1; aux t2]
316 | Cic.Appl (bop::t1::t2::[])
317 when (cic_is_const ~uri:(Some rmult_uri) bop) -> (* *. *)
318 Cic.Appl [mkCtor apmult_uri []; aux t1; aux t2]
319 | Cic.Appl (uop::t::[])
320 when (cic_is_const ~uri:(Some ropp_uri) uop) -> (* ~-. *)
321 Cic.Appl [mkCtor apopp_uri []; aux t]
322 | t when (cic_is_const ~uri:(Some r0_uri) t) -> (* 0. *)
324 | t when (cic_is_const ~uri:(Some r1_uri) t) -> (* 1. *)
326 | t -> (* variable *)
328 Hashtbl.find varhash t (* use an old var *)
329 with Not_found -> begin (* create a new var *)
331 Cic.Appl [mkCtor apvar_uri []; path_of_int !counter]
334 varlist := t :: !varlist;
335 Hashtbl.add varhash t newvar;
339 let aterms = List.map aux terms in (* abstract vars *)
340 let varmap = (* build varmap *)
341 btree_of_array ~vars:(Array.of_list (List.rev !varlist))
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 =
354 let r = mkConst r_uri [] in (* cic objects *)
355 let rplus = mkConst rplus_uri [] in
356 let rmult = mkConst rmult_uri [] in
357 let ropp = mkConst ropp_uri [] in
358 let r1 = mkConst r1_uri [] in
359 let r0 = mkConst r0_uri [] in
360 let theory_args_subst varmap =
361 [abstract_rings_A_uri, r ;
362 abstract_rings_Aplus_uri, rplus ;
363 abstract_rings_Amult_uri, rmult ;
364 abstract_rings_Aone_uri, r1 ;
365 abstract_rings_Azero_uri, r0 ;
366 abstract_rings_Aopp_uri, ropp ;
367 abstract_rings_vm_uri, varmap] in
368 let theory_args_subst' eq varmap t =
369 [abstract_rings_A_uri, r ;
370 abstract_rings_Aplus_uri, rplus ;
371 abstract_rings_Amult_uri, rmult ;
372 abstract_rings_Aone_uri, r1 ;
373 abstract_rings_Azero_uri, r0 ;
374 abstract_rings_Aopp_uri, ropp ;
375 abstract_rings_Aeq_uri, eq ;
376 abstract_rings_vm_uri, varmap ;
377 abstract_rings_T_uri, t] in
378 let interp_ap varmap =
379 mkConst interp_ap_uri (theory_args_subst varmap) in
380 let interp_sacs varmap =
381 mkConst interp_sacs_uri (theory_args_subst varmap) in
382 let apolynomial_normalize = mkConst apolynomial_normalize_uri [] in
383 let apolynomial_normalize_ok eq varmap t =
384 mkConst apolynomial_normalize_ok_uri (theory_args_subst' eq varmap t) in
385 let rtheory = mkConst rtheory_uri [] in
386 let lxy_false = (** Cic funcion "fun (x,y):R -> false" *)
387 Cic.Lambda (Cic.Anonymous, r,
388 Cic.Lambda (Cic.Anonymous, r,
389 mkCtor false_uri []))
391 let (aterms, varmap) = abstract_poly ~terms in (* abstract polys *)
392 List.map (* build ring segments *)
394 Cic.Appl [interp_ap varmap ; t],
396 [interp_sacs varmap ; Cic.Appl [apolynomial_normalize; t]]),
397 Cic.Appl [apolynomial_normalize_ok lxy_false varmap rtheory ; t]
401 let status_of_single_goal_tactic_result =
403 proof,[goal] -> proof,goal
405 raise (Fail "status_of_single_goal_tactic_result: the tactic did not produce exactly a new goal")
408 auxiliary tactic "elim_type"
409 @param status current proof engine status
410 @param term term to cut
412 let elim_type_tac ~term ~status =
413 warn "in Ring.elim_type_tac";
414 Tacticals.thens ~start:(cut_tac ~term)
415 ~continuations:[elim_simpl_intros_tac ~term:(Cic.Rel 1) ; Tacticals.id_tac] ~status
418 auxiliary tactic, use elim_type and try to close 2nd subgoal using proof
419 @param status current proof engine status
420 @param term term to cut
421 @param proof term used to prove second subgoal generated by elim_type
423 let elim_type2_tac ~term ~proof ~status =
424 warn "in Ring.elim_type2";
425 Tacticals.thens ~start:(elim_type_tac ~term)
426 ~continuations:[Tacticals.id_tac ; exact_tac ~term:proof] ~status
428 (* spostata in variousTactics.ml
430 Reflexivity tactic, try to solve current goal using "refl_eqT"
431 Warning: this isn't equale to the coq's Reflexivity because this one tries
432 only refl_eqT, coq's one also try "refl_equal"
433 @param status current proof engine status
435 let reflexivity_tac ~status:(proof, goal) =
436 warn "in Ring.reflexivity_tac";
437 let refl_eqt = mkCtor ~uri:refl_eqt_uri ~exp_named_subst:[] in
439 apply_tac ~status:(proof, goal) ~term:refl_eqt
440 with (Fail _) as e ->
441 let e_str = Printexc.to_string e in
442 raise (Fail ("Reflexivity failed with exception: " ^ e_str))
445 (** lift an 8-uple of debrujins indexes of n *)
446 let lift ~n (a,b,c,d,e,f,g,h) =
447 match (List.map (CicSubstitution.lift n) [a;b;c;d;e;f;g;h]) with
448 | [a;b;c;d;e;f;g;h] -> (a,b,c,d,e,f,g,h)
452 remove hypothesis from a given status starting from the last one
453 @param count number of hypotheses to remove
454 @param status current proof engine status
456 let purge_hyps_tac ~count ~status:(proof, goal as status) =
457 let module S = ProofEngineStructuralRules in
458 let rec aux n context status =
460 match (n, context) with
464 (status_of_single_goal_tactic_result (S.clear ~hyp:hd ~status))
465 | (_, []) -> failwith "Ring.purge_hyps_tac: no hypotheses left"
467 let (_, metasenv, _, _) = proof in
468 let (_, context, _) = conj_of_metano goal metasenv in
469 let proof',goal' = aux count context status in
470 assert (goal = goal') ;
476 Ring tactic, does associative and commutative rewritings in Reals ring
477 @param status current proof engine status
479 let ring_tac ~status:((proof, goal) as status) =
480 warn "in Ring tactic";
481 let eqt = mkMutInd (eqt_uri, 0) [] in
482 let r = mkConst r_uri [] in
483 let metasenv = metasenv_of_status ~status in
484 let (metano, context, ty) = conj_of_metano goal metasenv in
485 let (t1, t2) = split_eq ty in (* goal like t1 = t2 *)
486 match (build_segments ~terms:[t1; t2]) with
487 | (t1', t1'', t1'_eq_t1'')::(t2', t2'', t2'_eq_t2'')::[] -> begin
488 List.iter (* debugging, feel free to remove *)
489 (fun (descr, term) ->
490 warn (descr ^ " " ^ (CicPp.ppterm term)))
492 ["t1"; "t1'"; "t1''"; "t1'_eq_t1''";
493 "t2"; "t2'"; "t2''"; "t2'_eq_t2''"]
494 [t1; t1'; t1''; t1'_eq_t1'';
495 t2; t2'; t2''; t2'_eq_t2'']);
497 let new_hyps = ref 0 in (* number of new hypotheses created *)
498 Tacticals.try_tactics
501 "reflexivity", VariousTactics.reflexivity_tac ;
502 "exact t1'_eq_t1''", exact_tac ~term:t1'_eq_t1'' ;
503 "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2'' ;
504 "exact sym_eqt su t1 ...", exact_tac
508 [equality_is_a_congruence_A, mkConst r_uri [] ;
509 equality_is_a_congruence_x, t1'' ;
510 equality_is_a_congruence_y, t1
514 "elim_type eqt su t1 ...", (fun ~status ->
515 let status' = (* status after 1st elim_type use *)
516 let context = context_of_status ~status in
517 if not (are_convertible context t1'' t1) then begin
518 warn "t1'' and t1 are NOT CONVERTIBLE";
520 elim_type2_tac (* 1st elim_type use *)
521 ~status ~proof:t1'_eq_t1''
522 ~term:(Cic.Appl [eqt; r; t1''; t1])
524 incr new_hyps; (* elim_type add an hyp *)
526 (proof,[goal]) -> proof,goal
529 warn "t1'' and t1 are CONVERTIBLE";
533 let (t1,t1',t1'',t1'_eq_t1'',t2,t2',t2'',t2'_eq_t2'') =
534 lift 1 (t1,t1',t1'',t1'_eq_t1'', t2,t2',t2'',t2'_eq_t2'')
537 Tacticals.try_tactics (* try to solve 1st subgoal *)
540 "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2'';
541 "exact sym_eqt su t2 ...",
546 [equality_is_a_congruence_A, mkConst r_uri [] ;
547 equality_is_a_congruence_x, t2'' ;
548 equality_is_a_congruence_y, t2
552 "elim_type eqt su t2 ...", (fun ~status ->
554 let context = context_of_status ~status in
555 if not (are_convertible context t2'' t2) then begin
556 warn "t2'' and t2 are NOT CONVERTIBLE";
558 elim_type2_tac (* 2nd elim_type use *)
559 ~status ~proof:t2'_eq_t2''
560 ~term:(Cic.Appl [eqt; r; t2''; t2])
562 incr new_hyps; (* elim_type add an hyp *)
564 (proof,[goal]) -> proof,goal
567 warn "t2'' and t2 are CONVERTIBLE";
571 try (* try to solve main goal *)
572 warn "trying reflexivity ....";
573 VariousTactics.reflexivity_tac ~status:status'
574 with (Fail _) -> (* leave conclusion to the user *)
575 warn "reflexivity failed, solution's left as an ex :-)";
576 purge_hyps_tac ~count:!new_hyps ~status:status')]
580 raise (Fail ("Ring failure: " ^ s))
582 | _ -> (* impossible: we are applying ring exacty to 2 terms *)
585 (* wrap ring_tac catching GoalUnringable and raising Fail *)
586 let ring_tac ~status =
589 with GoalUnringable ->
590 raise (Fail "goal unringable")