From: Andrea Asperti Date: Thu, 4 Nov 2004 10:24:59 +0000 (+0000) Subject: Auto moved to a new file autoTactic.ml X-Git-Tag: v_0_6_4_1~26 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=59a077151336a0e73804572b52fb757a0e7f6a97;p=helm.git Auto moved to a new file autoTactic.ml Added a hastbl of duplicates in the library (currently filtered by hint). --- diff --git a/helm/ocaml/tactics/.depend b/helm/ocaml/tactics/.depend index 6cd18ba9f..1f98e15f4 100644 --- a/helm/ocaml/tactics/.depend +++ b/helm/ocaml/tactics/.depend @@ -5,6 +5,7 @@ proofEngineStructuralRules.cmi: proofEngineTypes.cmi primitiveTactics.cmi: proofEngineTypes.cmi metadataQuery.cmi: proofEngineTypes.cmi variousTactics.cmi: proofEngineTypes.cmi +autoTactic.cmi: proofEngineTypes.cmi introductionTactics.cmi: proofEngineTypes.cmi eliminationTactics.cmi: proofEngineTypes.cmi negationTactics.cmi: proofEngineTypes.cmi @@ -35,16 +36,20 @@ primitiveTactics.cmo: proofEngineHelpers.cmi proofEngineReduction.cmi \ primitiveTactics.cmx: proofEngineHelpers.cmx proofEngineReduction.cmx \ proofEngineTypes.cmx reductionTactics.cmx tacticals.cmx \ primitiveTactics.cmi -metadataQuery.cmo: primitiveTactics.cmi proofEngineTypes.cmi \ - metadataQuery.cmi -metadataQuery.cmx: primitiveTactics.cmx proofEngineTypes.cmx \ - metadataQuery.cmi -variousTactics.cmo: metadataQuery.cmi primitiveTactics.cmi \ - proofEngineReduction.cmi proofEngineTypes.cmi tacticals.cmi \ - variousTactics.cmi -variousTactics.cmx: metadataQuery.cmx primitiveTactics.cmx \ - proofEngineReduction.cmx proofEngineTypes.cmx tacticals.cmx \ - variousTactics.cmi +metadataQuery.cmo: hashtbl_equiv.cmi primitiveTactics.cmi \ + proofEngineTypes.cmi metadataQuery.cmi +metadataQuery.cmx: hashtbl_equiv.cmx primitiveTactics.cmx \ + proofEngineTypes.cmx metadataQuery.cmi +variousTactics.cmo: primitiveTactics.cmi proofEngineReduction.cmi \ + proofEngineTypes.cmi tacticals.cmi variousTactics.cmi +variousTactics.cmx: primitiveTactics.cmx proofEngineReduction.cmx \ + proofEngineTypes.cmx tacticals.cmx variousTactics.cmi +hashtbl_equiv.cmo: hashtbl_equiv.cmi +hashtbl_equiv.cmx: hashtbl_equiv.cmi +autoTactic.cmo: metadataQuery.cmi primitiveTactics.cmi proofEngineHelpers.cmi \ + proofEngineTypes.cmi autoTactic.cmi +autoTactic.cmx: metadataQuery.cmx primitiveTactics.cmx proofEngineHelpers.cmx \ + proofEngineTypes.cmx autoTactic.cmi introductionTactics.cmo: primitiveTactics.cmi proofEngineTypes.cmi \ introductionTactics.cmi introductionTactics.cmx: primitiveTactics.cmx proofEngineTypes.cmx \ diff --git a/helm/ocaml/tactics/Makefile b/helm/ocaml/tactics/Makefile index 439478865..33391a5e4 100644 --- a/helm/ocaml/tactics/Makefile +++ b/helm/ocaml/tactics/Makefile @@ -8,8 +8,8 @@ INTERFACE_FILES = \ proofEngineTypes.mli \ proofEngineReduction.mli proofEngineHelpers.mli \ tacticals.mli reductionTactics.mli proofEngineStructuralRules.mli \ - primitiveTactics.mli metadataQuery.mli \ - variousTactics.mli \ + primitiveTactics.mli hashtbl_equiv.mli metadataQuery.mli \ + variousTactics.mli autoTactic.mli \ introductionTactics.mli eliminationTactics.mli negationTactics.mli \ equalityTactics.mli discriminationTactics.mli ring.mli fourier.mli \ fourierR.mli history.mli statefulProofEngine.mli diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml new file mode 100644 index 000000000..bc9991664 --- /dev/null +++ b/helm/ocaml/tactics/autoTactic.ml @@ -0,0 +1,339 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(* Da rimuovere, solo per debug*) +let print_context ctx = + let print_name = + function + Cic.Name n -> n + | Cic.Anonymous -> "_" + in + List.fold_right + (fun i (output,context) -> + let (newoutput,context') = + match i with + Some (n,Cic.Decl t) -> + print_name n ^ ":" ^ CicPp.pp t context ^ "\n", (Some n)::context + | Some (n,Cic.Def (t,None)) -> + print_name n ^ ":=" ^ CicPp.pp t context ^ "\n", (Some n)::context + | None -> + "_ ?= _\n", None::context + | Some (_,Cic.Def (_,Some _)) -> assert false + in + output^newoutput,context' + ) ctx ("",[]) + ;; + + +let search_theorems_in_context status = + let (proof, goal) = status in + let module C = Cic in + let module R = CicReduction in + let module S = CicSubstitution in + let module PET = ProofEngineTypes in + let module PT = PrimitiveTactics in + prerr_endline "Entro in search_context"; + let _,metasenv,_,_ = proof in + let _,context,ty = CicUtil.lookup_meta goal metasenv in + let rec find n = function + [] -> [] + | hd::tl -> + let res = + try + Some (PET.apply_tactic + (PT.apply_tac ~term:(C.Rel n)) status ) + with + PET.Fail _ -> None in + (match res with + Some res -> res::(find (n+1) tl) + | None -> find (n+1) tl) + in + try + find 1 context + with Failure s -> + [] +;; + +let depth = 4;; + +let new_search_theorems f proof goal depth gtl sign = + let choices = f (proof,goal) + in + List.map + (function (proof, goallist) -> + (proof,(List.map (function g -> (g,depth)) goallist)@gtl, sign)) + choices +;; + +exception NoOtherChoices;; +let rec auto dbd = function + [] -> [] + | (proof, [], sign)::tl -> (proof, [], sign)::tl + | (proof, (goal,0)::_, _)::tl -> auto dbd tl + | (proof, (((goal,depth)::gtl) as allg), sign)::tl -> + (* first we check if the metavariable has not been already + closed as a side effect by some other application *) + let facts = (depth = 1) in + let name,metasenv,p,statement = proof in + let meta_inf = + (try + let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in + Some (ey, ty) + with _ -> None) in + match meta_inf with + Some (ey, ty) -> + (* the goal is still there *) + prerr_endline ("CURRENT GOAL = " ^ (CicPp.ppterm ty)); + prerr_endline ("CURRENT PROOF = " ^ (CicPp.ppterm p)); + prerr_endline ("CURRENT HYP = " ^ (fst (print_context ey))); + (* if the goal contains metavariables we use the input + signature for at_most constraints *) + let is_meta_closed = CicUtil.is_meta_closed ty in + let sign, new_sign = + if is_meta_closed then + None, Some (MetadataConstraints.signature_of ty) + else sign,sign in (* maybe the union ? *) + let local_choices = + new_search_theorems + search_theorems_in_context + proof goal (depth-1) [] new_sign in + let global_choices = + new_search_theorems + (fun status -> + List.map snd + (MetadataQuery.hint + ~dbd ~facts:facts ?signature:sign status)) + proof goal (depth-1) [] new_sign in + (* we proceed depth-first on the current goal. This is + a MAJOR optimization, since in case of success, and + if the goal is meta_closed, we may just drop the alternatives + tl1, avoiding useless backtracking. *) + let all_choices = + local_choices@global_choices in + (match (auto dbd all_choices) + with + [] -> auto dbd tl + | (proof,[],_)::tl1 -> + let all_choices = + let gtl' = List.map fst gtl in + if (gtl = [] || is_meta_closed) then + (proof,gtl,sign)::tl + else + let tl2 = + (List.map + (function (p,l,s) -> (p,l@gtl,s)) tl1) + in + (proof,gtl,sign)::tl2@tl in + auto dbd all_choices + | _ -> assert false) + | None -> auto dbd ((proof,gtl,sign)::tl) +;; + + +let auto_tac ~(dbd:Mysql.dbd) = + let auto_tac dbh (proof,goal) = + prerr_endline "Entro in Auto"; + match (auto dbd [(proof, [(goal,depth)],None)]) with + [] -> prerr_endline("Auto failed"); + raise (ProofEngineTypes.Fail "No Applicable theorem") + | (proof,[],_)::_ -> + prerr_endline "AUTO_TAC HA FINITO"; + (proof,[]) + | _ -> assert false + in + ProofEngineTypes.mk_tactic (auto_tac dbd) +;; + + +(************************** EXPERIMENTAL VERSION ****************************) + +(* In this versions of auto_tac we maintain an hash table of all inspected + goals. We assume that the context is invariant for application. + To this aim, it is essential to sall hint_verbose, that in turns calls + apply_verbose. *) + + +type exitus = + No of int + | Yes of Cic.term * int + | NotYetInspected + +let inspected_goals = Hashtbl.create 503;; + +let search_theorems_in_context status = + let (proof, goal) = status in + let module C = Cic in + let module R = CicReduction in + let module S = CicSubstitution in + let module PET = ProofEngineTypes in + let module PT = PrimitiveTactics in + prerr_endline "Entro in search_context"; + let _,metasenv,_,_ = proof in + let _,context,ty = CicUtil.lookup_meta goal metasenv in + let rec find n = function + [] -> [] + | hd::tl -> + let res = + try + Some (PT.apply_tac_verbose ~term:(C.Rel n) status ) + with + PET.Fail _ -> None in + (match res with + Some res -> res::(find (n+1) tl) + | None -> find (n+1) tl) + in + try + find 1 context + with Failure s -> + [] +;; + +let new_search_theorems f proof goal depth gtl sign = + let choices = f (proof,goal) + in + List.map + (function (subst,(proof, goallist)) -> + (subst,(proof,(List.map (function g -> (g,depth)) goallist)@gtl, sign))) + choices +;; + +exception NoOtherChoices;; +let rec auto_new dbd = function + [] -> [] + | (subst,(proof, [], sign))::tl -> (subst,(proof, [], sign))::tl + | (subst,(proof, (goal,0)::_, _))::tl -> auto_new dbd tl + | (subst,(proof, (((goal,depth)::gtl) as allg), sign))::tl -> + let facts = (depth = 1) in + let name,metasenv,p,statement = proof in + let meta_inf = + (try + let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in + Some (ey, ty) + with _ -> None) in + match meta_inf with + Some (ey, ty) -> + (* first of all we check if the goal has been already + inspected *) + let exitus = + try Hashtbl.find inspected_goals ty + with Not_found -> NotYetInspected in + let is_meta_closed = CicUtil.is_meta_closed ty in + begin + match exitus with + Yes (bo,_) -> + prerr_endline "ALREADY PROVED!!!!!!!!!!!!!!!!!!!!!!!!!!!!"; + prerr_endline (CicPp.ppterm ty); + let subst_in = + (* if we just apply the subtitution, the type + is irrelevant: we may use Implicit, since it will + be dropped *) + CicMetaSubst.apply_subst + [(goal,(ey, bo, Cic.Implicit None))] in + let (proof,_) = + ProofEngineHelpers.subst_meta_and_metasenv_in_proof + proof goal subst_in metasenv in + let new_subst t = (subst_in (subst t)) in + auto_new dbd ((new_subst,(proof,gtl,sign))::tl) + | No d when (d >= depth) -> + prerr_endline "PRUNED!!!!!!!!!!!!!!!!!!!!!!!!!!!!"; + auto_new dbd tl + | No _ + | NotYetInspected -> + prerr_endline ("CURRENT GOAL = " ^ (CicPp.ppterm ty)); + prerr_endline ("CURRENT PROOF = " ^ (CicPp.ppterm p)); + prerr_endline ("CURRENT HYP = " ^ (fst (print_context ey))); + let sign, new_sign = + if is_meta_closed then + None, Some (MetadataConstraints.signature_of ty) + else sign,sign in (* maybe the union ? *) + let local_choices = + new_search_theorems + search_theorems_in_context + proof goal (depth-1) [] new_sign in + let global_choices = + new_search_theorems + (fun status -> + List.map snd + (MetadataQuery.experimental_hint + ~dbd ~facts:facts ?signature:sign status)) + proof goal (depth-1) [] new_sign in + let all_choices = + local_choices@global_choices in + (match (auto_new dbd all_choices) + with + [] -> + (* no proof has been found; we update the + hastable *) + Hashtbl.add inspected_goals ty (No depth); + auto_new dbd tl + | (local_subst,(proof,[],_))::tl1 -> + (* a proof for goal has been found: + in order to get the proof we apply subst to + Meta[goal] *) + if is_meta_closed then + begin + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable ey in + let meta_proof = + local_subst (Cic.Meta(goal,irl)) in + Hashtbl.add inspected_goals + ty (Yes (meta_proof,depth)); + end; + let new_subst t = (local_subst (subst t)) in + let all_choices = + let gtl' = List.map fst gtl in + if (gtl = [] || is_meta_closed) then + (new_subst,(proof,gtl,sign))::tl + else + let tl2 = + (List.map + (function (f,(p,l,s)) + -> (f,(p,l@gtl,s))) tl1) + in + (new_subst,(proof,gtl,sign))::tl2@tl in + auto_new dbd all_choices + | _ -> assert false) + end + | None -> auto_new dbd ((subst,(proof,gtl,sign))::tl) +;; + + +let auto_tac_new ~(dbd:Mysql.dbd) = + let auto_tac dbd (proof,goal) = + Hashtbl.clear inspected_goals; + prerr_endline "Entro in Auto"; + let id t = t in + match (auto_new dbd [id,(proof, [(goal,depth)],None)]) with + [] -> prerr_endline("Auto failed"); + raise (ProofEngineTypes.Fail "No Applicable theorem") + | (_,(proof,[],_))::_ -> + prerr_endline "AUTO_TAC HA FINITO"; + (proof,[]) + | _ -> assert false + in + ProofEngineTypes.mk_tactic (auto_tac dbd) +;; + + diff --git a/helm/ocaml/tactics/autoTactic.mli b/helm/ocaml/tactics/autoTactic.mli new file mode 100644 index 000000000..15ed54d1d --- /dev/null +++ b/helm/ocaml/tactics/autoTactic.mli @@ -0,0 +1,28 @@ + +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +val auto_tac : dbd:Mysql.dbd -> ProofEngineTypes.tactic +val auto_tac_new : dbd:Mysql.dbd -> ProofEngineTypes.tactic diff --git a/helm/ocaml/tactics/hashtbl_equiv.ml b/helm/ocaml/tactics/hashtbl_equiv.ml new file mode 100644 index 000000000..b489e089a --- /dev/null +++ b/helm/ocaml/tactics/hashtbl_equiv.ml @@ -0,0 +1,189 @@ +(* Copyright (C) 2000-2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(*********************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Andrea Asperti *) +(* 8/09/2004 *) +(* *) +(* *) +(*********************************************************************) + + +(* the file contains an hash table of objects of the library + equivalent to some object in the standard subset; it is + mostly used to filter useless cases in auto *) + + +let equivalent_objects = +(* finte costanti; i.e. costanti senza corpo *) +[("cic:/Rocq/DEMOS/Demo_AutoRewrite/Ack0.con","finte costanti"); + ("cic:/Rocq/DEMOS/Demo_AutoRewrite/Ac10.con","finte costanti"); + ("cic:/Rocq/DEMOS/Demo_AutoRewrite/Ack2.con","finte costanti") + ]@ +(* inutili mostri *) +[("cic:/Rocq/DEMOS/Demo_AutoRewrite/Resg0.con","useless monster"); + ("cic:/Rocq/DEMOS/Demo_AutoRewrite/Resg1.con","useless monster"); + ("cic:/Rocq/DEMOS/Demo_AutoRewrite/ResAck0.con","useless monster") + ]@ +(* istanze *) + ("cic:/Coq/Init/Peano/eq_S.con","cic:/Coq/Init/Logic/f_equal.con"):: +[ +"cic:/Paris/ZF/src/useful/lem_iff_sym.con","cic:/Coq/Init/Logic/iff_sym.con"; +"cic:/Lyon/AUTOMATA/Ensf_types/False_imp_P.con","cic:/Coq/Init/Logic/False_ind.con"; +"cic:/Rocq/TreeAutomata/bases/plus_O_r.con","cic:/Coq/Arith/Plus/plus_0_r.con"; +"cic:/Coq/Reals/Rfunctions/sum_f_R0_triangle.con","cic:/Coq/Reals/PartSum/Rabs_triang_gen.con"; +"cic:/Sophia-Antipolis/Bertrand/Misc/eq_plus.con","cic:/Coq/Arith/Plus/plus_reg_l.con"; +"cic:/Suresnes/BDD/rauzy/algorithme1/Prelude_BDT/deMorgan_not_and.con","cic:/Coq/Logic/Classical_Prop/or_not_and.con"; +"cic:/Rocq/DEMOS/Sorting/diff_true_false.con","cic:/Coq/Bool/Bool/diff_true_false.con"; +"cic:/CoRN/metrics/CMetricSpaces/nz.con","cic:/Coq/Arith/Max/le_max_l.con"; +"cic:/Coq/Logic/Decidable/not_or.con","cic:/Coq/Logic/Classical_Prop/not_or_and.con"; +"cic:/Coq/Init/Logic/sym_not_equal.con","cic:/Coq/Init/Logic/sym_not_eq.con"; +"cic:/Coq/Reals/R_sqrt/sqrt_sqrt.con","cic:/Coq/Reals/R_sqrt/sqrt_def.con"; +"cic:/Coq/Reals/Rlimit/eps2_Rgt_R0_subproof.con","cic:/Coq/Reals/Rlimit/eps2_Rgt_R0.con"; +"cic:/Coq/Logic/Eqdep_dec/eqT2eq.con","cic:/Coq/Logic/Eqdep_dec/eq2eqT.con"; +"cic:/Coq/Reals/R_sqr/Rsqr_eq_0.con","cic:/Coq/Reals/RIneq/Rsqr_0_uniq.con"; +"cic:/Rocq/THREE_GAP/Nat_compl/en_plus.con","cic:/Coq/Arith/Plus/plus_0_r.con"; +"cic:/Nijmegen/QArith/Zaux/Zabs_10.con","cic:/Coq/ZArith/Zabs/Zabs_pos.con"; +"cic:/Coq/Reals/Rlimit/Rlt_eps4_eps_subproof0.con","cic:/Coq/Reals/Rlimit/Rlt_eps2_eps_subproof.con"; +"cic:/Coq/Arith/Le/le_refl.con","cic:/Coq/Init/Peano/le.ind#xpointer(1/1/1)"; +"cic:/Rocq/TreeAutomata/bases/le_n_n.con","cic:/Coq/Arith/Le/le_refl.con"; +"cic:/Coq/ZArith/auxiliary/Zred_factor1.con","cic:/Coq/ZArith/BinInt/Zplus_diag_eq_mult_2.con"; +"cic:/Coq/Relations/Newman/caseRxy.con","cic:/Coq/Relations/Newman/Ind_proof.con"; +"cic:/Rocq/TreeAutomata/bases/S_plus_r.con","cic:/Coq/Init/Peano/plus_n_Sm.con"; +"cic:/Eindhoven/POCKLINGTON/lemmas/Zmult_ab0a0b0.con","cic:/Coq/ZArith/BinInt/Zmult_integral.con"; +"cic:/Sophia-Antipolis/Algebra/Z_group/ax8.con","cic:/Coq/NArith/BinPos/ZC2.con"; +"cic:/Sophia-Antipolis/Algebra/Z_group/Zlt_reg_l.con","cic:/Coq/ZArith/Zorder/Zplus_lt_compat_l.con"; +"cic:/Sophia-Antipolis/MATHS/Z/Nat_complements/mult_neutr.con","cic:/Coq/Arith/Mult/mult_1_l.con"; +"cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con","cic:/Coq/Reals/RIneq/Rlt_0_1.con"; +"cic:/Suresnes/BDD/rauzy/algorithme1/Prelude_BDT/Classic.con","cic:/Coq/Logic/Classical_Prop/NNPP.con"; +"cic:/Coq/Reals/R_sqr/Rsqr_pos_lt.con","cic:/Coq/Reals/RIneq/Rlt_0_sqr.con"; +"cic:/Rocq/THREE_GAP/Nat_compl/lt_minus2.con","cic:/Coq/Reals/ArithProp/lt_minus_O_lt.con"; +"cic:/Coq/Reals/Rtrigo_def/sin_antisym.con","cic:/Coq/Reals/Rtrigo/sin_neg.con"; +"cic:/Sophia-Antipolis/Functions_in_ZFC/Functions_in_ZFC/false_implies_everything.con","cic:/Coq/Init/Logic/False_ind.con"; +"cic:/Coq/ring/Setoid_ring_normalize/index_eq_prop.con","cic:/Coq/ring/Ring_normalize/index_eq_prop.con"; +"cic:/CoRN/algebra/Basics/le_pred.con","cic:/Coq/Arith/Le/le_pred.con"; +"cic:/Lannion/continuations/FOUnify_cps/nat_complements/le_S_eqP.con","cic:/Coq/Arith/Compare/le_le_S_eq.con"; +"cic:/Coq/Sorting/Permutation/permut_right.con","cic:/Coq/Sorting/Permutation/permut_cons.con"; +"cic:/Eindhoven/POCKLINGTON/lemmas/Zlt_mult_l.con","cic:/Coq/ZArith/Zorder/Zmult_lt_compat_l.con"; +"cic:/Coq/Reals/RIneq/Rplus_lt_0_compat.con","cic:/Coq/Reals/DiscrR/Rplus_lt_pos.con"; +"cic:/Nijmegen/QArith/Zaux/Zpower_1_subproof.con","cic:/Coq/ZArith/BinInt/Zmult_1_r.con"; +"cic:/CoRN/fta/KeyLemma/lem_1c.con","cic:/Coq/Arith/Minus/le_minus.con"; +"cic:/Coq/omega/OmegaLemmas/OMEGA20.con","cic:/Coq/omega/OmegaLemmas/OMEGA17.con"; +"cic:/Nijmegen/QArith/Zaux/pair_2.con","cic:/Coq/Init/Datatypes/injective_projections.con"; +"cic:/Coq/Reals/Rlimit/Rlt_eps4_eps_subproof.con","cic:/Coq/Reals/Rlimit/Rlt_eps2_eps_subproof.con"; +"cic:/CoRN/algebra/Basics/le_mult_right.con","cic:/Coq/Arith/Mult/mult_le_compat_r.con"; +"cic:/Nijmegen/QArith/Zaux/Zle_lt_plus_plus.con","cic:/Coq/ZArith/Zorder/Zplus_le_lt_compat.con"; +"cic:/Rocq/ARITH/Chinese/Nat_complements/lt_minus2.con","cic:/Coq/Reals/ArithProp/lt_minus_O_lt.con"; +"cic:/Rocq/THREE_GAP/Nat_compl/not_gt_le.con","cic:/Coq/Arith/Compare_dec/not_gt.con"; +"cic:/Rocq/ARITH/Chinese/Nat_complements/mult_commut.con","cic:/Coq/Arith/Mult/mult_comm.con"; +"cic:/CoRN/algebra/Basics/lt_mult_right.con","cic:/Coq/Arith/Mult/mult_lt_compat_r.con"; +"cic:/Rocq/ARITH/Chinese/Nat_complements/mult_neutr.con","cic:/Coq/Arith/Mult/mult_1_l.con"; +"cic:/Nijmegen/QArith/Zaux/Zabs_neg.con","cic:/Coq/ZArith/Zabs/Zabs_non_eq.con"; +"cic:/Lyon/FIRING-SQUAD/bib/plus_S.con","cic:/Coq/Init/Peano/plus_Sn_m.con"; +"cic:/Nijmegen/QArith/Qhomographic_Qpositive_to_Qpositive/one_non_negative.con","cic:/Coq/ZArith/Zorder/Zle_0_1.con"; +"cic:/Coq/fourier/Fourier_util/Rle_zero_1.con","cic:/Coq/Reals/RIneq/Rle_0_1.con"; +"cic:/Coq/Logic/Diaconescu/proof_irrel.con","cic:/Coq/Logic/Classical_Prop/proof_irrelevance.con"; +"cic:/Coq/Init/Logic/sym_equal.con","cic:/Coq/Init/Logic/sym_eq.con"; +"cic:/Coq/IntMap/Mapiter/pair_sp.con","cic:/Coq/Init/Datatypes/surjective_pairing.con"; +"cic:/Coq/Logic/ProofIrrelevance/proof_irrelevance_cci.con","cic:/Coq/Logic/Classical_Prop/proof_irrelevance.con"; +"cic:/Suresnes/BDD/rauzy/algorithme1/Prelude_BDT/deMorgan_or_not.con","cic:/Coq/Logic/Classical_Prop/not_and_or.con"; +"cic:/CoRN/model/structures/Zsec/Zplus_wd0.con","cic:/Coq/ZArith/BinInt/Zplus_eq_compat.con"; +"cic:/Coq/ZArith/auxiliary/Zred_factor6.con","cic:/Coq/ZArith/BinInt/Zplus_0_r_reverse.con"; +"cic:/Eindhoven/POCKLINGTON/lemmas/S_inj.con","cic:/Coq/Init/Peano/eq_add_S.con"; +"cic:/Coq/ZArith/Wf_Z/Z_of_nat_complete.con","cic:/Coq/Reals/RIneq/IZN.con"; +"cic:/Suresnes/BDD/rauzy/algorithme1/Prelude_BDT/Commutative_orb.con","cic:/Coq/Bool/Bool/orb_comm.con"; +"cic:/Coq/Reals/PartSum/plus_sum.con","cic:/Coq/Reals/Cauchy_prod/sum_plus.con"; +"cic:/Nijmegen/QArith/Qpositive/minus_le.con","cic:/Coq/Arith/Minus/le_minus.con"; +"cic:/Lyon/FIRING-SQUAD/bib/plus_zero.con","cic:/Coq/Arith/Plus/plus_0_r.con"; +"cic:/Sophia-Antipolis/Cours-de-Coq/ex1_auto/not_not_converse.con","cic:/Coq/Logic/Classical_Prop/NNPP.con"; +"cic:/Suresnes/BDD/rauzy/algorithme1/Prelude_BDT/deMorgan_and_not.con","cic:/Coq/Logic/Classical_Prop/not_or_and.con"; +"cic:/Suresnes/BDD/rauzy/algorithme1/Prelude_BDT/Commutative_andb.con","cic:/Coq/Bool/Bool/andb_comm.con"; +"cic:/Sophia-Antipolis/MATHS/Z/Nat_complements/lt_minus2.con","cic:/Coq/Reals/ArithProp/lt_minus_O_lt.con"; +"cic:/Suresnes/BDD/canonicite/Prelude0/Morgan_and_not.con","cic:/Coq/Logic/Classical_Prop/not_or_and.con"; +"cic:/Coq/Logic/ClassicalFacts/TrueP.con","cic:/Coq/Logic/ClassicalFacts/FalseP.con"; +"cic:/Nijmegen/QArith/Zaux/Zminus_eq.con","cic:/Coq/ZArith/BinInt/Zminus_eq.con"; +"cic:/Sophia-Antipolis/Cours-de-Coq/ex1/not_not_converse.con","cic:/Coq/Logic/Classical_Prop/NNPP.con"; +"cic:/Nijmegen/QArith/Zaux/pair_1.con","cic:/Coq/Init/Datatypes/surjective_pairing.con"; +"cic:/Orsay/Maths/divide/Zabs_ind.con","cic:/Coq/ZArith/Zabs/Zabs_ind.con"; +"cic:/CoRN/algebra/Basics/Zmult_minus_distr_r.con","cic:/Coq/ZArith/BinInt/Zmult_minus_distr_l.con"; +"cic:/Coq/fourier/Fourier_util/Rfourier_eqLR_to_le.con","cic:/Coq/Reals/RIneq/Req_le.con"; +"cic:/Rocq/TreeAutomata/bases/Sn_eq_Sm_n_eq_m.con","cic:/Coq/Init/Peano/eq_add_S.con"; +"cic:/Coq/Init/Logic/trans_equal.con","cic:/Coq/Init/Logic/trans_eq.con"; +"cic:/Coq/omega/OmegaLemmas/OMEGA2.con","cic:/Coq/ZArith/Zorder/Zplus_le_0_compat.con"; +"cic:/Sophia-Antipolis/Bertrand/Raux/P_Rmin.con","cic:/Coq/Reals/Rpower/P_Rmin.con"; +"cic:/Sophia-Antipolis/MATHS/Z/Nat_complements/mult_commut.con","cic:/Coq/Arith/Mult/mult_comm.con"; +"cic:/Sophia-Antipolis/Huffman/Aux/le_minus.con","cic:/Coq/Arith/Minus/le_minus.con"; +"cic:/Coq/Init/Peano/plus_O_n.con","cic:/Coq/Arith/Plus/plus_0_l.con"; +"cic:/Coq/Logic/Berardi/inv2.con","cic:/Coq/Logic/Berardi/AC.con"; +"cic:/Coq/Reals/SeqProp/not_Rlt.con","cic:/Coq/Reals/RIneq/Rnot_lt_ge.con"; +"cic:/Nancy/FOUnify/nat_complements/le_S_eqP.con","cic:/Coq/Arith/Compare/le_le_S_eq.con"; +"cic:/Rocq/TreeAutomata/bases/le_mult_l.con","cic:/Coq/Arith/Mult/mult_le_compat_r.con"; +"cic:/Eindhoven/POCKLINGTON/natZ/isnat_mult.con","cic:/Coq/ZArith/Zorder/Zmult_le_0_compat.con"; +"cic:/Coq/fourier/Fourier_util/Rfourier_eqRL_to_le.con","cic:/Coq/Reals/RIneq/Req_le_sym.con"; +"cic:/Nijmegen/QArith/Zaux/Zabs_mult.con","cic:/Coq/ZArith/Zabs/Zabs_Zmult.con"; +"cic:/Rocq/TreeAutomata/bases/plus_n_O.con","cic:/Coq/Arith/Plus/plus_0_r.con"; +"cic:/Suresnes/BDD/rauzy/algorithme1/Prelude_BDT/excluded_middle.con","cic:/Coq/Logic/Classical_Prop/classic.con"; +"cic:/Rocq/TreeAutomata/bases/le_mult_mult.con","cic:/Coq/Arith/Mult/mult_le_compat.con"; +"cic:/Coq/Bool/Bool/Is_true_eq_true2.con","cic:/Coq/Bool/Bool/Is_true_eq_left.con"; +"cic:/Eindhoven/POCKLINGTON/natZ/isnat_plus.con","cic:/Coq/ZArith/Zorder/Zplus_le_0_compat.con"; +"cic:/Eindhoven/POCKLINGTON/lemmas/lt_plus_plus.con","cic:/Coq/Arith/Plus/plus_lt_compat.con"; +"cic:/Rocq/TreeAutomata/bases/le_mult_r.con","cic:/Coq/Arith/Mult/mult_le_compat_l.con"; +"cic:/Sophia-Antipolis/Functions_in_ZFC/Functions_in_ZFC/excluded_middle.con","cic:/Coq/Logic/Classical_Prop/NNPP.con"; +"cic:/Sophia-Antipolis/Algebra/Z_group/ax3.con","cic:/Coq/ZArith/Zorder/Zgt_pos_0.con"; +"cic:/Nijmegen/QArith/Zaux/Zabs_plus.con","cic:/Coq/ZArith/Zabs/Zabs_triangle.con"; +"cic:/Sophia-Antipolis/Buchberger/Buch/Sdep.con","cic:/Coq/Init/Datatypes/prod_ind.con"; +"cic:/Coq/Reals/PartSum/Rsum_abs.con","cic:/Coq/Reals/PartSum/Rabs_triang_gen.con"; +"cic:/Cachan/SMC/mu/minus_n_m_le_n.con","cic:/Coq/Arith/Minus/le_minus.con"; +"cic:/Marseille/GC/lib_arith/lib_S_pred/eqnm_eqSnSm.con","cic:/Coq/Init/Peano/eq_S.con"; +"cic:/Nijmegen/QArith/Zaux/Zpower_1_subproof_subproof.con","cic:/Coq/ZArith/BinInt/Zmult_1_r.con"; +"cic:/Eindhoven/POCKLINGTON/lemmas/predminus1.con","cic:/Coq/Arith/Minus/pred_of_minus.con"; +"cic:/Sophia-Antipolis/Bertrand/Raux/Rpower_pow.con","cic:/Coq/Reals/Rpower/Rpower_pow.con"; +"cic:/Lyon/FIRING-SQUAD/bib/lt_plus_plus.con","cic:/Coq/Arith/Plus/plus_lt_compat.con"; +"cic:/Eindhoven/POCKLINGTON/lemmas/Zlt_neq.con","cic:/Coq/ZArith/Zorder/Zlt_not_eq.con"; +"cic:/Coq/Arith/Lt/nat_total_order.con","cic:/Coq/Arith/Compare_dec/not_eq.con"; +"cic:/Rocq/TreeAutomata/bases/plus_O_l.con","cic:/Coq/Arith/Plus/plus_0_r.con"; +"cic:/Coq/Logic/ClassicalFacts/boolP.ind#xpointer(1/1/2)","cic:/Coq/Logic/ClassicalFacts/boolP.ind#xpointer(1/1/1)"; +"cic:/Nijmegen/QArith/Zaux/Zmult_pos_pos.con","cic:/Coq/ZArith/Zorder/Zmult_lt_O_compat.con"; +"cic:/Nijmegen/QArith/Zaux/Zlt_plus_plus.con","cic:/Coq/ZArith/Zorder/Zplus_lt_compat.con"; +"cic:/Coq/Logic/Diaconescu/pred_ext_and_rel_choice_imp_EM.con","cic:/Coq/Logic/Classical_Prop/classic.con"; +"cic:/Sophia-Antipolis/Rsa/MiscRsa/eq_plus.con","cic:/Coq/Arith/Plus/plus_reg_l.con" +] +;; + +let equiv_table = Hashtbl.create 503 +;; + +let _ = List.iter (fun (a,b) -> Hashtbl.add equiv_table a b) equivalent_objects +;; + +let not_a_duplicate u = + try + ignore(Hashtbl.find equiv_table u); false + with + Not_found -> true +;; diff --git a/helm/ocaml/tactics/hashtbl_equiv.mli b/helm/ocaml/tactics/hashtbl_equiv.mli new file mode 100644 index 000000000..723e6831b --- /dev/null +++ b/helm/ocaml/tactics/hashtbl_equiv.mli @@ -0,0 +1,38 @@ +(* Copyright (C) 2000-2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(*********************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Andrea Asperti *) +(* 8/09/2004 *) +(* *) +(* *) +(*********************************************************************) + + +val not_a_duplicate : string -> bool + diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml index 0a7544ef8..5be94e7df 100644 --- a/helm/ocaml/tactics/variousTactics.ml +++ b/helm/ocaml/tactics/variousTactics.ml @@ -23,222 +23,6 @@ * http://cs.unibo.it/helm/. *) - -(* Da rimuovere, solo per debug*) -let print_context ctx = - let print_name = - function - Cic.Name n -> n - | Cic.Anonymous -> "_" - in - List.fold_right - (fun i (output,context) -> - let (newoutput,context') = - match i with - Some (n,Cic.Decl t) -> - print_name n ^ ":" ^ CicPp.pp t context ^ "\n", (Some n)::context - | Some (n,Cic.Def (t,None)) -> - print_name n ^ ":=" ^ CicPp.pp t context ^ "\n", (Some n)::context - | None -> - "_ ?= _\n", None::context - | Some (_,Cic.Def (_,Some _)) -> assert false - in - output^newoutput,context' - ) ctx ("",[]) - ;; - - - - - -let search_theorems_in_context status = - let (proof, goal) = status in - let module C = Cic in - let module R = CicReduction in - let module S = CicSubstitution in - let module PET = ProofEngineTypes in - let module PT = PrimitiveTactics in - prerr_endline "Entro in search_context"; - let _,metasenv,_,_ = proof in - let _,context,ty = CicUtil.lookup_meta goal metasenv in - let rec find n = function - [] -> [] - | hd::tl -> - let res = - try - Some (PET.apply_tactic (PT.apply_tac ~term:(C.Rel n)) status ) - with - PET.Fail _ -> None in - (match res with - Some res -> res::(find (n+1) tl) - | None -> find (n+1) tl) - in - try - let res = find 1 context in - prerr_endline "Ho finito context"; - res - with Failure s -> - prerr_endline ("SIAM QUI = " ^ s); [] -;; - -exception NotAProposition;; -exception NotApplicableTheorem;; -exception MaxDepth;; - -let depth = 3;; - -(* -let rec auto_tac_aux mqi_handle level proof goal = -prerr_endline ("Entro in Auto_rec; level = " ^ (string_of_int level)); -if level = 0 then - (* (proof, [goal]) *) - (prerr_endline ("MaxDepth"); - raise MaxDepth) -else - (* let us verify that the metavariable is still an open goal -- - it could have been closed by closing other goals -- and that - it is of sort Prop *) - let _,metasenv,_,_ = proof in - let meta_inf = - (try - let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in - Some (ey, ty) - with _ -> None) in - match meta_inf with - Some (ey, ty) -> - prerr_endline ("CURRENT GOAL = " ^ (CicPp.ppterm ty)); - prerr_endline ("CURRENT HYP = " ^ (fst (print_context ey))); - (* if the goal does not have a sort Prop we return the - current proof and a list containing the goal *) - let ty_sort = CicTypeChecker.type_of_aux' metasenv ey ty in - if CicReduction.are_convertible - ey (Cic.Sort Cic.Prop) ty_sort then - (* sort Prop *) - (* choices is a list of pairs proof and goallist *) - let choices = - (search_theorems_in_context (proof,goal))@ - (TacticChaser.searchTheorems mqi_handle (proof,goal)) - in - let rec try_choices = function - [] -> raise NotApplicableTheorem - | (proof,goallist)::tl -> -prerr_endline ("GOALLIST = " ^ string_of_int (List.length goallist)); - (try - List.fold_left - (fun proof goal -> - auto_tac_aux mqi_handle (level-1) proof goal) - proof goallist - with - | MaxDepth - | NotApplicableTheorem - | NotAProposition -> - try_choices tl) in - try_choices choices - else - (* CUT AND PASTE DI PROVA !! *) - let choices = - (search_theorems_in_context (proof,goal))@ - (TacticChaser.searchTheorems mqi_handle (proof,goal)) - in - let rec try_choices = function - [] -> raise NotApplicableTheorem - | (proof,[])::tl -> proof - | _::tl -> try_choices tl in - try_choices choices - (* raise NotAProposition *) - | None -> proof -;; - -let auto_tac mqi_handle = - let module PET = ProofEngineTypes in - let auto_tac mqi_handle (proof,goal) = - prerr_endline "Entro in Auto"; - try - let proof = auto_tac_aux mqi_handle depth proof goal in - prerr_endline "AUTO_TAC HA FINITO"; - (proof,[]) - with - | MaxDepth -> assert false (* this should happens only if depth is 0 above *) - | NotApplicableTheorem -> - prerr_endline("No applicable theorem"); - raise (ProofEngineTypes.Fail "No Applicable theorem") - in - PET.mk_tactic (auto_tac mqi_handle) -;; - -*) - -(**** ESPERIMENTO ************************) - -let new_search_theorems f proof goal depth gtl = - let local_choices = f (proof,goal) - in - List.map - (function (proof, goallist) -> - (proof, (List.map (function g -> (g,depth)) goallist)@gtl)) - local_choices -;; - -exception NoOtherChoices;; - -let rec auto_new dbd = function - [] -> raise NoOtherChoices - | (proof, [])::tl -> (proof, [])::tl - | (proof, (goal,0)::gtl)::tl -> auto_new dbd tl - | (proof, (goal,depth)::gtl)::tl -> - let _,metasenv,proof_obj,_ = proof in - let meta_inf = - (try - let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in - Some (ey, ty) - with _ -> None) in - match meta_inf with - Some (ey, ty) -> - prerr_endline ("CURRENT GOAL = " ^ (CicPp.ppterm ty)); - prerr_endline ("CURRENT HYP = " ^ (fst (print_context ey))); - prerr_endline ("CURRENT PROOF = " ^ (CicPp.ppterm proof_obj)); - let local_choices = - new_search_theorems - search_theorems_in_context proof goal (depth-1) gtl in - let global_choices = - new_search_theorems - (fun status -> List.map snd (MetadataQuery.hint ~dbd status)) -(* (TacticChaser.searchTheorems mqi_handle) *) - proof goal (depth-1) gtl in - let all_choices = - local_choices@global_choices@tl in - let sorting_list (_,g1) (_,g2) = - let l1 = List.length g1 in - let l2 = List.length g2 in - if (l1 = l2 && not(l1 = 0)) then - (snd(List.nth g2 0)) - (snd(List.nth g1 0)) - else l1 - l2 in - let reorder = - List.stable_sort sorting_list all_choices - in - auto_new dbd reorder - | None -> auto_new dbd ((proof,gtl)::tl) -;; - - -let auto_tac ~(dbd:Mysql.dbd) = -(* CicMetaSubst.reset_counters (); *) - let auto_tac dbd (proof,goal) = - prerr_endline "Entro in Auto"; - try - (match auto_new dbd [(proof, [(goal,depth)])] with - | (proof,_)::_ -> - prerr_endline "AUTO_TAC HA FINITO"; - (* CicMetaSubst.print_counters (); *) - (proof,[]) - | _ -> assert false) - with - | NoOtherChoices -> - prerr_endline("Auto failed"); - raise (ProofEngineTypes.Fail "No Applicable theorem") - in - ProofEngineTypes.mk_tactic (auto_tac dbd) -;; (* TODO se ce n'e' piu' di una, prende la prima che trova... sarebbe meglio chiedere: find dovrebbe restituire una lista di hyp (?) da passare all'utonto con una diff --git a/helm/ocaml/tactics/variousTactics.mli b/helm/ocaml/tactics/variousTactics.mli index 5c7c9a0a9..d1da2fe98 100644 --- a/helm/ocaml/tactics/variousTactics.mli +++ b/helm/ocaml/tactics/variousTactics.mli @@ -25,13 +25,10 @@ *) exception AllSelectedTermsMustBeConvertible;; -exception NotApplicableTheorem;; val assumption_tac: ProofEngineTypes.tactic val generalize_tac: ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> Cic.term list -> ProofEngineTypes.tactic -(* val auto_tac : MQIConn.handle -> ProofEngineTypes.tactic *) -val auto_tac : dbd:Mysql.dbd -> ProofEngineTypes.tactic