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
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 \
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
--- /dev/null
+(* 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)
+;;
+
+
--- /dev/null
+
+(* 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
--- /dev/null
+(* 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
+;;
--- /dev/null
+(* 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
+
* 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
*)
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
projects / helm.git / commitdiff