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? *)
35 let debug_print = fun _ -> ()
37 (** debugging print *)
38 let warn s = debug_print (lazy ("RING WARNING: " ^ (Lazy.force s)))
43 Note: For constructors URIs aren't really URIs but rather triples of
44 the form (uri, typeno, consno). This discrepancy is to preserver an
45 uniformity of invocation of "mkXXX" functions.
48 let equality_is_a_congruence_A =
49 uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/A.var"
50 let equality_is_a_congruence_x =
51 uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/x.var"
52 let equality_is_a_congruence_y =
53 uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/y.var"
56 uri_of_string "cic:/Coq/ring/Ring_abstract/apolynomial.ind"
57 let apvar_uri = (apolynomial_uri, 0, 1)
58 let ap0_uri = (apolynomial_uri, 0, 2)
59 let ap1_uri = (apolynomial_uri, 0, 3)
60 let applus_uri = (apolynomial_uri, 0, 4)
61 let apmult_uri = (apolynomial_uri, 0, 5)
62 let apopp_uri = (apolynomial_uri, 0, 6)
64 let quote_varmap_A_uri = uri_of_string "cic:/Coq/ring/Quote/variables_map/A.var"
65 let varmap_uri = uri_of_string "cic:/Coq/ring/Quote/varmap.ind"
66 let empty_vm_uri = (varmap_uri, 0, 1)
67 let node_vm_uri = (varmap_uri, 0, 2)
68 let varmap_find_uri = uri_of_string "cic:/Coq/ring/Quote/varmap_find.con"
69 let index_uri = uri_of_string "cic:/Coq/ring/Quote/index.ind"
70 let left_idx_uri = (index_uri, 0, 1)
71 let right_idx_uri = (index_uri, 0, 2)
72 let end_idx_uri = (index_uri, 0, 3)
74 let abstract_rings_A_uri =
75 uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/A.var"
76 let abstract_rings_Aplus_uri =
77 uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Aplus.var"
78 let abstract_rings_Amult_uri =
79 uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Amult.var"
80 let abstract_rings_Aone_uri =
81 uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Aone.var"
82 let abstract_rings_Azero_uri =
83 uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Azero.var"
84 let abstract_rings_Aopp_uri =
85 uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Aopp.var"
86 let abstract_rings_Aeq_uri =
87 uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Aeq.var"
88 let abstract_rings_vm_uri =
89 uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/vm.var"
90 let abstract_rings_T_uri =
91 uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/T.var"
92 let interp_ap_uri = uri_of_string "cic:/Coq/ring/Ring_abstract/interp_ap.con"
94 uri_of_string "cic:/Coq/ring/Ring_abstract/interp_sacs.con"
95 let apolynomial_normalize_uri =
96 uri_of_string "cic:/Coq/ring/Ring_abstract/apolynomial_normalize.con"
97 let apolynomial_normalize_ok_uri =
98 uri_of_string "cic:/Coq/ring/Ring_abstract/apolynomial_normalize_ok.con"
100 (** CIC PREDICATES *)
103 check whether a term is a constant or not, if argument "uri" is given and is
104 not "None" also check if the constant correspond to the given one or not
106 let cic_is_const ?(uri: uri option = None) term =
110 | Cic.Const _ -> true
114 | Cic.Const (u, _) when (eq u realuri) -> true
117 (** PROOF AND GOAL ACCESSORS *)
121 @return the uri of a given proof
123 let uri_of_proof ~proof:(uri, _, _, _) = uri
126 @param status current proof engine status
127 @raise Failure if proof is None
128 @return current goal's metasenv
130 let metasenv_of_status ((_,m,_,_), _) = m
133 @param status a proof engine status
134 @raise Failure when proof or goal are None
135 @return context corresponding to current goal
137 let context_of_status status =
138 let (proof, goal) = status in
139 let metasenv = metasenv_of_status status in
140 let _, context, _ = CicUtil.lookup_meta goal metasenv in
143 (** CIC TERM CONSTRUCTORS *)
146 Create a Cic term consisting of a constant
147 @param uri URI of the constant
149 @exp_named_subst explicit named substitution
151 let mkConst ~uri ~exp_named_subst =
152 Cic.Const (uri, exp_named_subst)
155 Create a Cic term consisting of a constructor
156 @param uri triple <uri, typeno, consno> where uri is the uri of an inductive
157 type, typeno is the type number in a mutind structure (0 based), consno is
158 the constructor number (1 based)
159 @exp_named_subst explicit named substitution
161 let mkCtor ~uri:(uri, typeno, consno) ~exp_named_subst =
162 Cic.MutConstruct (uri, typeno, consno, exp_named_subst)
165 Create a Cic term consisting of a type member of a mutual induction
166 @param uri pair <uri, typeno> where uri is the uri of a mutual inductive
167 type and typeno is the type number (0 based) in the mutual induction
168 @exp_named_subst explicit named substitution
170 let mkMutInd ~uri:(uri, typeno) ~exp_named_subst =
171 Cic.MutInd (uri, typeno, exp_named_subst)
176 raised when the current goal is not ringable; a goal is ringable when is an
177 equality on reals (@see r_uri)
179 exception GoalUnringable
181 (** RING's FUNCTIONS LIBRARY *)
184 Check whether the ring tactic can be applied on a given term (i.e. that is
185 an equality on reals)
186 @param term to be tested
187 @return true if the term is ringable, false otherwise
190 let is_equality = function
191 | Cic.MutInd (uri, 0, []) when (eq uri HelmLibraryObjects.Logic.eq_URI) -> true
194 let is_real = function
195 | Cic.Const (uri, _) when (eq uri HelmLibraryObjects.Reals.r_URI) -> true
199 | Cic.Appl (app::set::_::_::[]) when (is_equality app && is_real set) ->
200 warn (lazy "Goal Ringable!");
203 warn (lazy "Goal Not Ringable :-((");
207 split an equality goal of the form "t1 = t2" in its two subterms t1 and t2
208 after checking that the goal is ringable
209 @param goal the current goal
210 @return a pair (t1,t2) that are two sides of the equality goal
211 @raise GoalUnringable if the goal isn't ringable
213 let split_eq = function
214 | (Cic.Appl (_::_::t1::t2::[])) as term when ringable term ->
215 warn (lazy ("<term1>" ^ (CicPp.ppterm t1) ^ "</term1>"));
216 warn (lazy ("<term2>" ^ (CicPp.ppterm t2) ^ "</term2>"));
218 | _ -> raise GoalUnringable
221 @param i an integer index representing a 1 based number of node in a binary
222 search tree counted in a fbs manner (i.e.: 1 is the root, 2 is the left
223 child of the root (if any), 3 is the right child of the root (if any), 4 is
224 the left child of the left child of the root (if any), ....)
225 @param proof the current proof
226 @return an index representing the same node in a varmap (@see varmap_uri),
227 the returned index is as defined in index (@see index_uri)
230 let rec digits_of_int n =
231 if n=1 then [] else (n mod 2 = 1)::(digits_of_int (n lsr 1))
236 mkCtor (if (digit = true) then right_idx_uri else left_idx_uri) [];
238 (List.rev (digits_of_int n)) (* remove leading true (i.e. digit 1) *)
239 (mkCtor end_idx_uri [])
242 Build a variable map (@see varmap_uri) from a variables array.
243 A variable map is almost a binary tree so this function receiving a var list
244 like [v;w;x;y;z] will build a varmap of shape: v
249 @param vars variables array
250 @return a cic term representing the variable map containing vars variables
252 let btree_of_array ~vars =
253 let r = HelmLibraryObjects.Reals.r in
254 let empty_vm_r = mkCtor empty_vm_uri [quote_varmap_A_uri,r] in
255 let node_vm_r = mkCtor node_vm_uri [quote_varmap_A_uri,r] in
256 let size = Array.length vars in
257 let halfsize = size lsr 1 in
258 let rec aux n = (* build the btree starting from position n *)
260 n is the position in the vars array _1_based_ in order to access
261 left and right child using (n*2, n*2+1) trick
265 else if n > halfsize then (* no more children *)
266 Cic.Appl [node_vm_r; vars.(n-1); empty_vm_r; empty_vm_r]
267 else (* still children *)
268 Cic.Appl [node_vm_r; vars.(n-1); aux (n*2); aux (n*2+1)]
273 abstraction function:
274 concrete polynoms -----> (abstract polynoms, varmap)
275 @param terms list of conrete polynoms
276 @return a pair <aterms, varmap> where aterms is a list of abstract polynoms
277 and varmap is the variable map needed to interpret them
279 let abstract_poly ~terms =
280 let varhash = Hashtbl.create 19 in (* vars hash, to speed up lookup *)
281 let varlist = ref [] in (* vars list in reverse order *)
282 let counter = ref 1 in (* index of next new variable *)
283 let rec aux = function (* TODO not tail recursive *)
284 (* "bop" -> binary operator | "uop" -> unary operator *)
285 | Cic.Appl (bop::t1::t2::[])
286 when (cic_is_const ~uri:(Some HelmLibraryObjects.Reals.rplus_URI) bop) -> (* +. *)
287 Cic.Appl [mkCtor applus_uri []; aux t1; aux t2]
288 | Cic.Appl (bop::t1::t2::[])
289 when (cic_is_const ~uri:(Some HelmLibraryObjects.Reals.rmult_URI) bop) -> (* *. *)
290 Cic.Appl [mkCtor apmult_uri []; aux t1; aux t2]
291 | Cic.Appl (uop::t::[])
292 when (cic_is_const ~uri:(Some HelmLibraryObjects.Reals.ropp_URI) uop) -> (* ~-. *)
293 Cic.Appl [mkCtor apopp_uri []; aux t]
294 | t when (cic_is_const ~uri:(Some HelmLibraryObjects.Reals.r0_URI) t) -> (* 0. *)
296 | t when (cic_is_const ~uri:(Some HelmLibraryObjects.Reals.r1_URI) t) -> (* 1. *)
298 | t -> (* variable *)
300 Hashtbl.find varhash t (* use an old var *)
301 with Not_found -> begin (* create a new var *)
303 Cic.Appl [mkCtor apvar_uri []; path_of_int !counter]
306 varlist := t :: !varlist;
307 Hashtbl.add varhash t newvar;
311 let aterms = List.map aux terms in (* abstract vars *)
312 let varmap = (* build varmap *)
313 btree_of_array ~vars:(Array.of_list (List.rev !varlist))
318 given a list of abstract terms (i.e. apolynomials) build the ring "segments"
319 that is triples like (t', t'', t''') where
320 t' = interp_ap(varmap, at)
321 t'' = interp_sacs(varmap, (apolynomial_normalize at))
322 t''' = apolynomial_normalize_ok(varmap, at)
323 at is the abstract term built from t, t is a single member of aterms
325 let build_segments ~terms =
326 let theory_args_subst varmap =
327 [abstract_rings_A_uri, HelmLibraryObjects.Reals.r ;
328 abstract_rings_Aplus_uri, HelmLibraryObjects.Reals.rplus ;
329 abstract_rings_Amult_uri, HelmLibraryObjects.Reals.rmult ;
330 abstract_rings_Aone_uri, HelmLibraryObjects.Reals.r1 ;
331 abstract_rings_Azero_uri, HelmLibraryObjects.Reals.r0 ;
332 abstract_rings_Aopp_uri, HelmLibraryObjects.Reals.ropp ;
333 abstract_rings_vm_uri, varmap] in
334 let theory_args_subst' eq varmap t =
335 [abstract_rings_A_uri, HelmLibraryObjects.Reals.r ;
336 abstract_rings_Aplus_uri, HelmLibraryObjects.Reals.rplus ;
337 abstract_rings_Amult_uri, HelmLibraryObjects.Reals.rmult ;
338 abstract_rings_Aone_uri, HelmLibraryObjects.Reals.r1 ;
339 abstract_rings_Azero_uri, HelmLibraryObjects.Reals.r0 ;
340 abstract_rings_Aopp_uri, HelmLibraryObjects.Reals.ropp ;
341 abstract_rings_Aeq_uri, eq ;
342 abstract_rings_vm_uri, varmap ;
343 abstract_rings_T_uri, t] in
344 let interp_ap varmap =
345 mkConst interp_ap_uri (theory_args_subst varmap) in
346 let interp_sacs varmap =
347 mkConst interp_sacs_uri (theory_args_subst varmap) in
348 let apolynomial_normalize = mkConst apolynomial_normalize_uri [] in
349 let apolynomial_normalize_ok eq varmap t =
350 mkConst apolynomial_normalize_ok_uri (theory_args_subst' eq varmap t) in
351 let lxy_false = (** Cic funcion "fun (x,y):R -> false" *)
352 Cic.Lambda (Cic.Anonymous, HelmLibraryObjects.Reals.r,
353 Cic.Lambda (Cic.Anonymous, HelmLibraryObjects.Reals.r, HelmLibraryObjects.Datatypes.falseb))
355 let (aterms, varmap) = abstract_poly ~terms in (* abstract polys *)
356 List.map (* build ring segments *)
358 Cic.Appl [interp_ap varmap ; t],
360 [interp_sacs varmap ; Cic.Appl [apolynomial_normalize; t]]),
361 Cic.Appl [apolynomial_normalize_ok lxy_false varmap HelmLibraryObjects.Reals.rtheory ; t]
365 let status_of_single_goal_tactic_result =
367 proof,[goal] -> proof,goal
369 raise (Fail (lazy "status_of_single_goal_tactic_result: the tactic did not produce exactly a new goal"))
371 (* Galla: spostata in variousTactics.ml
373 auxiliary tactic "elim_type"
374 @param status current proof engine status
375 @param term term to cut
377 let elim_type_tac ~term status =
378 warn (lazy "in Ring.elim_type_tac");
379 Tacticals.thens ~start:(cut_tac ~term)
380 ~continuations:[elim_simpl_intros_tac ~term:(Cic.Rel 1) ; Tacticals.id_tac] status
384 auxiliary tactic, use elim_type and try to close 2nd subgoal using proof
385 @param status current proof engine status
386 @param term term to cut
387 @param proof term used to prove second subgoal generated by elim_type
389 (* FG: METTERE I NOMI ANCHE QUI? *)
390 let elim_type2_tac ~term ~proof =
391 let elim_type2_tac ~term ~proof status =
392 let module E = EliminationTactics in
393 warn (lazy "in Ring.elim_type2");
394 ProofEngineTypes.apply_tactic
395 (Tacticals.thens ~start:(E.elim_type_tac term)
396 ~continuations:[Tacticals.id_tac ; exact_tac ~term:proof]) status
398 ProofEngineTypes.mk_tactic (elim_type2_tac ~term ~proof)
400 (* Galla: spostata in variousTactics.ml
402 Reflexivity tactic, try to solve current goal using "refl_eqT"
403 Warning: this isn't equale to the coq's Reflexivity because this one tries
404 only refl_eqT, coq's one also try "refl_equal"
405 @param status current proof engine status
407 let reflexivity_tac (proof, goal) =
408 warn (lazy "in Ring.reflexivity_tac");
409 let refl_eqt = mkCtor ~uri:refl_eqt_uri ~exp_named_subst:[] in
411 apply_tac (proof, goal) ~term:refl_eqt
412 with (Fail _) as e ->
413 let e_str = Printexc.to_string e in
414 raise (Fail ("Reflexivity failed with exception: " ^ e_str))
417 (** lift an 8-uple of debrujins indexes of n *)
418 let lift ~n (a,b,c,d,e,f,g,h) =
419 match (List.map (CicSubstitution.lift n) [a;b;c;d;e;f;g;h]) with
420 | [a;b;c;d;e;f;g;h] -> (a,b,c,d,e,f,g,h)
424 remove hypothesis from a given status starting from the last one
425 @param count number of hypotheses to remove
426 @param status current proof engine status
428 let purge_hyps_tac ~count =
429 let purge_hyps_tac ~count status =
430 let module S = ProofEngineStructuralRules in
431 let (proof, goal) = status in
432 let rec aux n context status =
434 match (n, context) with
440 | Some (Cic.Anonymous,_) -> assert false
441 | Some (Cic.Name name,_) -> name
444 (status_of_single_goal_tactic_result
445 (ProofEngineTypes.apply_tactic (S.clear ~hyp:name_of_hyp) status))
446 | (_, []) -> failwith "Ring.purge_hyps_tac: no hypotheses left"
448 let (_, metasenv, _, _) = proof in
449 let (_, context, _) = CicUtil.lookup_meta goal metasenv in
450 let proof',goal' = aux count context status in
451 assert (goal = goal') ;
454 ProofEngineTypes.mk_tactic (purge_hyps_tac ~count)
459 Ring tactic, does associative and commutative rewritings in Reals ring
460 @param status current proof engine status
463 let ring_tac status =
464 let (proof, goal) = status in
465 warn (lazy "in Ring tactic");
466 let eqt = mkMutInd (HelmLibraryObjects.Logic.eq_URI, 0) [] in
467 let r = HelmLibraryObjects.Reals.r in
468 let metasenv = metasenv_of_status status in
469 let (metano, context, ty) = CicUtil.lookup_meta goal metasenv in
470 let (t1, t2) = split_eq ty in (* goal like t1 = t2 *)
471 match (build_segments ~terms:[t1; t2]) with
472 | (t1', t1'', t1'_eq_t1'')::(t2', t2'', t2'_eq_t2'')::[] -> begin
474 List.iter (* debugging, feel free to remove *)
475 (fun (descr, term) ->
476 warn (lazy (descr ^ " " ^ (CicPp.ppterm term))))
478 ["t1"; "t1'"; "t1''"; "t1'_eq_t1''";
479 "t2"; "t2'"; "t2''"; "t2'_eq_t2''"]
480 [t1; t1'; t1''; t1'_eq_t1'';
481 t2; t2'; t2''; t2'_eq_t2'']);
483 let new_hyps = ref 0 in (* number of new hypotheses created *)
484 ProofEngineTypes.apply_tactic
487 "reflexivity", EqualityTactics.reflexivity_tac ;
488 "exact t1'_eq_t1''", exact_tac ~term:t1'_eq_t1'' ;
489 "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2'' ;
490 "exact sym_eqt su t1 ...", exact_tac
493 [mkConst HelmLibraryObjects.Logic.sym_eq_URI
494 [equality_is_a_congruence_A, HelmLibraryObjects.Reals.r;
495 equality_is_a_congruence_x, t1'' ;
496 equality_is_a_congruence_y, t1
500 "elim_type eqt su t1 ...", ProofEngineTypes.mk_tactic (fun status ->
501 let status' = (* status after 1st elim_type use *)
502 let context = context_of_status status in
503 let b,_ = (*TASSI : FIXME*)
504 are_convertible context t1'' t1 CicUniv.empty_ugraph in
506 warn (lazy "t1'' and t1 are NOT CONVERTIBLE");
508 ProofEngineTypes.apply_tactic
509 (elim_type2_tac (* 1st elim_type use *)
511 ~term:(Cic.Appl [eqt; r; t1''; t1]))
514 incr new_hyps; (* elim_type add an hyp *)
516 (proof,[goal]) -> proof,goal
519 warn (lazy "t1'' and t1 are CONVERTIBLE");
523 let (t1,t1',t1'',t1'_eq_t1'',t2,t2',t2'',t2'_eq_t2'') =
524 lift 1 (t1,t1',t1'',t1'_eq_t1'', t2,t2',t2'',t2'_eq_t2'')
527 ProofEngineTypes.apply_tactic
528 (Tacticals.first (* try to solve 1st subgoal *)
530 "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2'';
531 "exact sym_eqt su t2 ...",
535 [mkConst HelmLibraryObjects.Logic.sym_eq_URI
536 [equality_is_a_congruence_A, HelmLibraryObjects.Reals.r;
537 equality_is_a_congruence_x, t2'' ;
538 equality_is_a_congruence_y, t2
542 "elim_type eqt su t2 ...",
543 ProofEngineTypes.mk_tactic (fun status ->
545 let context = context_of_status status in
546 let b,_ = (* TASSI:FIXME *)
547 are_convertible context t2'' t2 CicUniv.empty_ugraph
550 warn (lazy "t2'' and t2 are NOT CONVERTIBLE");
552 ProofEngineTypes.apply_tactic
553 (elim_type2_tac (* 2nd elim_type use *)
555 ~term:(Cic.Appl [eqt; r; t2''; t2]))
558 incr new_hyps; (* elim_type add an hyp *)
560 (proof,[goal]) -> proof,goal
563 warn (lazy "t2'' and t2 are CONVERTIBLE");
567 try (* try to solve main goal *)
568 warn (lazy "trying reflexivity ....");
569 ProofEngineTypes.apply_tactic
570 EqualityTactics.reflexivity_tac status'
571 with (Fail _) -> (* leave conclusion to the user *)
572 warn (lazy "reflexivity failed, solution's left as an ex :-)");
573 ProofEngineTypes.apply_tactic
574 (purge_hyps_tac ~count:!new_hyps) status')])
580 raise (Fail (lazy ("Ring failure: " ^ Lazy.force s)))
582 | _ -> (* impossible: we are applying ring exacty to 2 terms *)
585 (* wrap ring_tac catching GoalUnringable and raising Fail *)
587 let ring_tac status =
590 with GoalUnringable ->
591 raise (Fail (lazy "goal unringable"))
593 let ring_tac = ProofEngineTypes.mk_tactic ring_tac