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 check whether a term is a constant or not, if argument "uri" is given and is
102 not "None" also check if the constant correspond to the given one or not
104 let cic_is_const ?(uri: uri option = None) term =
108 | Cic.Const _ -> true
112 | Cic.Const (u, _) when (eq u realuri) -> true
115 (** PROOF AND GOAL ACCESSORS *)
119 @return the uri of a given proof
121 let uri_of_proof ~proof:(uri, _, _, _) = uri
124 @param metano meta list index
125 @param metasenv meta list (environment)
126 @raise Failure if metano is not found in metasenv
127 @return conjecture corresponding to metano in metasenv
129 let conj_of_metano metano =
131 List.find (function (m, _, _) -> m = metano)
134 "Ring.conj_of_metano: " ^
135 (string_of_int metano) ^ " no such meta")
138 @param status current proof engine status
139 @raise Failure if proof is None
140 @return current goal's metasenv
142 let metasenv_of_status ~status:((_,m,_,_), _) = m
145 @param status a proof engine status
146 @raise Failure when proof or goal are None
147 @return context corresponding to current goal
149 let context_of_status ~status:(proof, goal as status) =
150 let metasenv = metasenv_of_status ~status:status in
151 let _, context, _ = List.find (function (m,_,_) -> m=goal) metasenv in
154 (** CIC TERM CONSTRUCTORS *)
157 Create a Cic term consisting of a constant
158 @param uri URI of the constant
161 let mkConst ~uri ~proof =
162 let cookingsno = relative_depth (uri_of_proof ~proof) uri 0 in
163 Cic.Const (uri, cookingsno)
166 Create a Cic term consisting of a constructor
167 @param uri triple <uri, typeno, consno> where uri is the uri of an inductive
168 type, typeno is the type number in a mutind structure (0 based), consno is
169 the constructor number (1 based)
170 @param proof current proof
172 let mkCtor ~uri:(uri, typeno, consno) ~proof =
173 let cookingsno = relative_depth (uri_of_proof ~proof) uri 0 in
174 Cic.MutConstruct (uri, cookingsno, typeno, consno)
177 Create a Cic term consisting of a type member of a mutual induction
178 @param uri pair <uri, typeno> where uri is the uri of a mutual inductive
179 type and typeno is the type number (0 based) in the mutual induction
181 let mkMutInd ~uri:(uri, typeno) ~proof =
182 let cookingsno = relative_depth (uri_of_proof ~proof) uri 0 in
183 Cic.MutInd (uri, cookingsno, typeno)
188 raised when the current goal is not ringable; a goal is ringable when is an
189 equality on reals (@see r_uri)
191 exception GoalUnringable
193 (** RING's FUNCTIONS LIBRARY *)
196 Check whether the ring tactic can be applied on a given term (i.e. that is
197 an equality on reals)
198 @param term term to be tested
199 @return true if the term is ringable, false otherwise
202 let is_equality = function
203 | Cic.MutInd uri _ 0 when (eq uri eqt_uri) -> true
206 let is_real = function
207 | Cic.Const (uri, _) when (eq uri r_uri) -> true
211 | Cic.Appl (app::set::_::_::[]) when (is_equality app && is_real set) ->
212 warn "Goal Ringable!";
215 warn "Goal Not Ringable :-((";
219 split an equality goal of the form "t1 = t2" in its two subterms t1 and t2
220 after checking that the goal is ringable
221 @param goal the current goal
222 @return a pair (t1,t2) that are two sides of the equality goal
223 @raise GoalUnringable if the goal isn't ringable
225 let split_eq = function
226 | (Cic.Appl (_::_::t1::t2::[])) as term when ringable term ->
227 warn ("<term1>" ^ (CicPp.ppterm t1) ^ "</term1>");
228 warn ("<term2>" ^ (CicPp.ppterm t2) ^ "</term2>");
230 | _ -> raise GoalUnringable
233 @param i an integer index representing a 1 based number of node in a binary
234 search tree counted in a fbs manner (i.e.: 1 is the root, 2 is the left
235 child of the root (if any), 3 is the right child of the root (if any), 4 is
236 the left child of the left child of the root (if any), ....)
237 @param proof the current proof
238 @return an index representing the same node in a varmap (@see varmap_uri),
239 the returned index is as defined in index (@see index_uri)
241 let path_of_int n proof =
242 let rec digits_of_int n =
243 if n=1 then [] else (n mod 2 = 1)::(digits_of_int (n lsr 1))
248 mkCtor (if (digit = true) then right_idx_uri else left_idx_uri) proof;
250 (List.rev (digits_of_int n)) (* remove leading true (i.e. digit 1) *)
251 (mkCtor end_idx_uri proof)
254 Build a variable map (@see varmap_uri) from a variables array.
255 A variable map is almost a binary tree so this function receiving a var list
256 like [v;w;x;y;z] will build a varmap of shape: v
261 @param vars variables array
262 @param proof current proof
263 @return a cic term representing the variable map containing vars variables
265 let btree_of_array ~vars ~proof =
266 let r = mkConst r_uri proof in (* cic objects *)
267 let empty_vm = mkCtor empty_vm_uri proof in
268 let empty_vm_r = Cic.Appl [empty_vm; r] in
269 let node_vm = mkCtor node_vm_uri proof in
270 let node_vm_r = Cic.Appl [node_vm; r] in
271 let size = Array.length vars in
272 let halfsize = size lsr 1 in
273 let rec aux n = (* build the btree starting from position n *)
275 n is the position in the vars array _1_based_ in order to access
276 left and right child using (n*2, n*2+1) trick
280 else if n > halfsize then (* no more children *)
281 Cic.Appl [node_vm; r; vars.(n-1); empty_vm_r; empty_vm_r]
282 else (* still children *)
283 Cic.Appl [node_vm; r; vars.(n-1); aux (n*2); aux (n*2+1)]
288 abstraction function:
289 concrete polynoms -----> (abstract polynoms, varmap)
290 @param terms list of conrete polynoms
291 @param proof current proof
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 ~proof =
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 rplus_uri) bop) -> (* +. *)
303 Cic.Appl [mkCtor applus_uri proof; aux t1; aux t2]
304 | Cic.Appl (bop::t1::t2::[])
305 when (cic_is_const ~uri:(Some rmult_uri) bop) -> (* *. *)
306 Cic.Appl [mkCtor apmult_uri proof; aux t1; aux t2]
307 | Cic.Appl (uop::t::[])
308 when (cic_is_const ~uri:(Some ropp_uri) uop) -> (* ~-. *)
309 Cic.Appl [mkCtor apopp_uri proof; aux t]
310 | t when (cic_is_const ~uri:(Some r0_uri) t) -> (* 0. *)
312 | t when (cic_is_const ~uri:(Some 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 proof; path_of_int !counter proof]
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)) ~proof
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 ~proof =
342 let r = mkConst r_uri proof in (* cic objects *)
343 let rplus = mkConst rplus_uri proof in
344 let rmult = mkConst rmult_uri proof in
345 let ropp = mkConst ropp_uri proof in
346 let r0 = mkConst r0_uri proof in
347 let r1 = mkConst r1_uri proof in
348 let interp_ap = mkConst interp_ap_uri proof in
349 let interp_sacs = mkConst interp_sacs_uri proof in
350 let apolynomial_normalize = mkConst apolynomial_normalize_uri proof in
351 let apolynomial_normalize_ok = mkConst apolynomial_normalize_ok_uri proof in
352 let rtheory = mkConst rtheory_uri proof in
353 let lxy_false = (** Cic funcion "fun (x,y):R -> false" *)
354 Cic.Lambda (Cic.Anonimous, r,
355 Cic.Lambda (Cic.Anonimous, r,
356 mkCtor false_uri proof))
358 let theory_args = [r; rplus; rmult; r1; r0; ropp] in
359 let (aterms, varmap) = abstract_poly ~terms ~proof in (* abstract polys *)
360 List.map (* build ring segments *)
362 Cic.Appl ((interp_ap :: theory_args) @ [varmap; t]),
366 [varmap; Cic.Appl [apolynomial_normalize; t]])),
368 (apolynomial_normalize_ok :: theory_args) @
369 [lxy_false; varmap; rtheory; t]))
372 let id_tac ~status:(proof,goal) =
375 let status_of_single_goal_tactic_result =
377 proof,[goal] -> proof,goal
379 raise (Fail "status_of_single_goal_tactic_result: the tactic did not produce exactly a new goal")
382 auxiliary tactic "elim_type"
383 @param status current proof engine status
384 @param term term to cut
386 let elim_type_tac ~term ~status =
387 warn "in Ring.elim_type_tac";
388 Tacticals.thens ~start:(cut_tac ~term)
389 ~continuations:[elim_intros_simpl_tac ~term:(Cic.Rel 1) ; id_tac] ~status
392 auxiliary tactic, use elim_type and try to close 2nd subgoal using proof
393 @param status current proof engine status
394 @param term term to cut
395 @param proof term used to prove second subgoal generated by elim_type
397 let elim_type2_tac ~term ~proof ~status =
398 warn "in Ring.elim_type2";
399 Tacticals.thens ~start:(elim_type_tac ~term)
400 ~continuations:[id_tac ; exact_tac ~term:proof] ~status
403 Reflexivity tactic, try to solve current goal using "refl_eqT"
404 Warning: this isn't equale to the coq's Reflexivity because this one tries
405 only refl_eqT, coq's one also try "refl_equal"
406 @param status current proof engine status
408 let reflexivity_tac ~status:(proof, goal) =
409 warn "in Ring.reflexivity_tac";
410 let refl_eqt = mkCtor ~uri:refl_eqt_uri ~proof:proof in
412 apply_tac ~status:(proof, goal) ~term:refl_eqt
413 with (Fail _) as e ->
414 let e_str = Printexc.to_string e in
415 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 ~status:(proof, goal as status) =
429 let module S = ProofEngineStructuralRules in
430 let rec aux n context status =
432 match (n, context) with
436 (status_of_single_goal_tactic_result (S.clear ~hyp:hd ~status))
437 | (_, []) -> failwith "Ring.purge_hyps_tac: no hypotheses left"
439 let (_, metasenv, _, _) = proof in
440 let (_, context, _) = conj_of_metano goal metasenv in
441 let proof',goal' = aux count context status in
442 assert (goal = goal') ;
448 Ring tactic, does associative and commutative rewritings in Reals ring
449 @param status current proof engine status
451 let ring_tac ~status:(proof, goal) =
452 warn "in Ring tactic";
453 let status = (proof, goal) in
454 let eqt = mkMutInd (eqt_uri, 0) proof in
455 let r = mkConst r_uri proof in
456 let metasenv = metasenv_of_status ~status in
457 let (metano, context, ty) = conj_of_metano goal metasenv in
458 let (t1, t2) = split_eq ty in (* goal like t1 = t2 *)
459 match (build_segments ~terms:[t1; t2] ~proof) with
460 | (t1', t1'', t1'_eq_t1'')::(t2', t2'', t2'_eq_t2'')::[] -> begin
461 List.iter (* debugging, feel free to remove *)
462 (fun (descr, term) ->
463 warn (descr ^ " " ^ (CicPp.ppterm term)))
465 ["t1"; "t1'"; "t1''"; "t1'_eq_t1''";
466 "t2"; "t2'"; "t2''"; "t2'_eq_t2''"]
467 [t1; t1'; t1''; t1'_eq_t1'';
468 t2; t2'; t2''; t2'_eq_t2'']);
470 let new_hyps = ref 0 in (* number of new hypotheses created *)
471 Tacticals.try_tactics
474 "reflexivity", reflexivity_tac;
475 "exact t1'_eq_t1''", exact_tac ~term:t1'_eq_t1'';
476 "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2'';
477 "exact sym_eqt su t1 ...", exact_tac ~term:(
479 mkConst sym_eqt_uri proof; mkConst r_uri proof;
480 t1''; t1; t1'_eq_t1'']);
481 "elim_type eqt su t1 ...", (fun ~status ->
482 let status' = (* status after 1st elim_type use *)
483 let context = context_of_status ~status in
484 if not (are_convertible context t1'' t1) then begin
485 warn "t1'' and t1 are NOT CONVERTIBLE";
487 elim_type2_tac (* 1st elim_type use *)
488 ~status ~proof:t1'_eq_t1''
489 ~term:(Cic.Appl [eqt; r; t1''; t1])
491 incr new_hyps; (* elim_type add an hyp *)
493 (proof,[goal]) -> proof,goal
496 warn "t1'' and t1 are CONVERTIBLE";
500 let (t1,t1',t1'',t1'_eq_t1'',t2,t2',t2'',t2'_eq_t2'') =
501 lift 1 (t1,t1',t1'',t1'_eq_t1'', t2,t2',t2'',t2'_eq_t2'')
504 Tacticals.try_tactics (* try to solve 1st subgoal *)
507 "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2'';
508 "exact sym_eqt su t2 ...",
511 mkConst sym_eqt_uri proof;
513 t2''; t2; t2'_eq_t2'']);
514 "elim_type eqt su t2 ...", (fun ~status ->
516 let context = context_of_status ~status in
517 if not (are_convertible context t2'' t2) then begin
518 warn "t2'' and t2 are NOT CONVERTIBLE";
520 elim_type2_tac (* 2nd elim_type use *)
521 ~status ~proof:t2'_eq_t2''
522 ~term:(Cic.Appl [eqt; r; t2''; t2])
524 incr new_hyps; (* elim_type add an hyp *)
526 (proof,[goal]) -> proof,goal
529 warn "t2'' and t2 are CONVERTIBLE";
533 try (* try to solve main goal *)
534 warn "trying reflexivity ....";
535 reflexivity_tac ~status:status'
536 with (Fail _) -> (* leave conclusion to the user *)
537 warn "reflexivity failed, solution's left as an ex :-)";
538 purge_hyps_tac ~count:!new_hyps ~status:status')]
542 raise (Fail ("Ring failure: " ^ s))
544 | _ -> (* impossible: we are applying ring exacty to 2 terms *)
547 (* wrap ring_tac catching GoalUnringable and raising Fail *)
548 let ring_tac ~status =
551 with GoalUnringable ->
552 raise (Fail "goal unringable")