helm/ocaml/tactics/hashtbl_equiv.ml

   1 (* Copyright (C) 2000-2002, HELM Team.
   2  *
   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.
   6  *
   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.
  11  *
  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.
  16  *
  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,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (*********************************************************************)
  27 (*                                                                   *)
  28 (*                           PROJECT HELM                            *)
  29 (*                                                                   *)
  30 (*                          Andrea Asperti                           *)
  31 (*                            8/09/2004                              *)
  32 (*                                                                   *)
  33 (*                                                                   *)
  34 (*********************************************************************)
  35
  36
  37 (* the file contains an hash table of objects of the library
  38    equivalent to some object in the standard subset; it is
  39    mostly used to filter useless cases in auto *)
  40
  41
  42 let equivalent_objects =
  43 (* finte costanti; i.e. costanti senza corpo *)
  44 [("cic:/Rocq/DEMOS/Demo_AutoRewrite/Ack0.con","finte costanti");
  45  ("cic:/Rocq/DEMOS/Demo_AutoRewrite/Ac10.con","finte costanti");
  46  ("cic:/Rocq/DEMOS/Demo_AutoRewrite/Ack2.con","finte costanti")
  47  ]@
  48 (* inutili mostri *)
  49 [("cic:/Rocq/DEMOS/Demo_AutoRewrite/Resg0.con","useless monster");
  50  ("cic:/Rocq/DEMOS/Demo_AutoRewrite/Resg1.con","useless monster");
  51  ("cic:/Rocq/DEMOS/Demo_AutoRewrite/ResAck0.con","useless monster")
  52  ]@
  53 (* istanze *)
  54    ("cic:/Coq/Init/Peano/eq_S.con","cic:/Coq/Init/Logic/f_equal.con")::
  55 [
  56 "cic:/Paris/ZF/src/useful/lem_iff_sym.con","cic:/Coq/Init/Logic/iff_sym.con";
  57 "cic:/Lyon/AUTOMATA/Ensf_types/False_imp_P.con","cic:/Coq/Init/Logic/False_ind.con";
  58 "cic:/Rocq/TreeAutomata/bases/plus_O_r.con","cic:/Coq/Arith/Plus/plus_0_r.con";
  59 "cic:/Coq/Reals/Rfunctions/sum_f_R0_triangle.con","cic:/Coq/Reals/PartSum/Rabs_triang_gen.con";
  60 "cic:/Sophia-Antipolis/Bertrand/Misc/eq_plus.con","cic:/Coq/Arith/Plus/plus_reg_l.con";
  61 "cic:/Suresnes/BDD/rauzy/algorithme1/Prelude_BDT/deMorgan_not_and.con","cic:/Coq/Logic/Classical_Prop/or_not_and.con";
  62 "cic:/Rocq/DEMOS/Sorting/diff_true_false.con","cic:/Coq/Bool/Bool/diff_true_false.con";
  63 "cic:/CoRN/metrics/CMetricSpaces/nz.con","cic:/Coq/Arith/Max/le_max_l.con";
  64 "cic:/Coq/Logic/Decidable/not_or.con","cic:/Coq/Logic/Classical_Prop/not_or_and.con";
  65 "cic:/Coq/Init/Logic/sym_not_equal.con","cic:/Coq/Init/Logic/sym_not_eq.con";
  66 "cic:/Coq/Reals/R_sqrt/sqrt_sqrt.con","cic:/Coq/Reals/R_sqrt/sqrt_def.con";
  67 "cic:/Coq/Reals/Rlimit/eps2_Rgt_R0_subproof.con","cic:/Coq/Reals/Rlimit/eps2_Rgt_R0.con";
  68 "cic:/Coq/Logic/Eqdep_dec/eqT2eq.con","cic:/Coq/Logic/Eqdep_dec/eq2eqT.con";
  69 "cic:/Coq/Reals/R_sqr/Rsqr_eq_0.con","cic:/Coq/Reals/RIneq/Rsqr_0_uniq.con";
  70 "cic:/Rocq/THREE_GAP/Nat_compl/en_plus.con","cic:/Coq/Arith/Plus/plus_0_r.con";
  71 "cic:/Nijmegen/QArith/Zaux/Zabs_10.con","cic:/Coq/ZArith/Zabs/Zabs_pos.con";
  72 "cic:/Coq/Reals/Rlimit/Rlt_eps4_eps_subproof0.con","cic:/Coq/Reals/Rlimit/Rlt_eps2_eps_subproof.con";
  73 "cic:/Coq/Arith/Le/le_refl.con","cic:/Coq/Init/Peano/le.ind#xpointer(1/1/1)";
  74 "cic:/Rocq/TreeAutomata/bases/le_n_n.con","cic:/Coq/Arith/Le/le_refl.con";
  75 "cic:/Coq/ZArith/auxiliary/Zred_factor1.con","cic:/Coq/ZArith/BinInt/Zplus_diag_eq_mult_2.con";
  76 "cic:/Coq/Relations/Newman/caseRxy.con","cic:/Coq/Relations/Newman/Ind_proof.con";
  77 "cic:/Rocq/TreeAutomata/bases/S_plus_r.con","cic:/Coq/Init/Peano/plus_n_Sm.con";
  78 "cic:/Eindhoven/POCKLINGTON/lemmas/Zmult_ab0a0b0.con","cic:/Coq/ZArith/BinInt/Zmult_integral.con";
  79 "cic:/Sophia-Antipolis/Algebra/Z_group/ax8.con","cic:/Coq/NArith/BinPos/ZC2.con";
  80 "cic:/Sophia-Antipolis/Algebra/Z_group/Zlt_reg_l.con","cic:/Coq/ZArith/Zorder/Zplus_lt_compat_l.con";
  81 "cic:/Sophia-Antipolis/MATHS/Z/Nat_complements/mult_neutr.con","cic:/Coq/Arith/Mult/mult_1_l.con";
  82 "cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con","cic:/Coq/Reals/RIneq/Rlt_0_1.con";
  83 "cic:/Suresnes/BDD/rauzy/algorithme1/Prelude_BDT/Classic.con","cic:/Coq/Logic/Classical_Prop/NNPP.con";
  84 "cic:/Coq/Reals/R_sqr/Rsqr_pos_lt.con","cic:/Coq/Reals/RIneq/Rlt_0_sqr.con";
  85 "cic:/Rocq/THREE_GAP/Nat_compl/lt_minus2.con","cic:/Coq/Reals/ArithProp/lt_minus_O_lt.con";
  86 "cic:/Coq/Reals/Rtrigo_def/sin_antisym.con","cic:/Coq/Reals/Rtrigo/sin_neg.con";
  87 "cic:/Sophia-Antipolis/Functions_in_ZFC/Functions_in_ZFC/false_implies_everything.con","cic:/Coq/Init/Logic/False_ind.con";
  88 "cic:/Coq/ring/Setoid_ring_normalize/index_eq_prop.con","cic:/Coq/ring/Ring_normalize/index_eq_prop.con";
  89 "cic:/CoRN/algebra/Basics/le_pred.con","cic:/Coq/Arith/Le/le_pred.con";
  90 "cic:/Lannion/continuations/FOUnify_cps/nat_complements/le_S_eqP.con","cic:/Coq/Arith/Compare/le_le_S_eq.con";
  91 "cic:/Coq/Sorting/Permutation/permut_right.con","cic:/Coq/Sorting/Permutation/permut_cons.con";
  92 "cic:/Eindhoven/POCKLINGTON/lemmas/Zlt_mult_l.con","cic:/Coq/ZArith/Zorder/Zmult_lt_compat_l.con";
  93 "cic:/Coq/Reals/RIneq/Rplus_lt_0_compat.con","cic:/Coq/Reals/DiscrR/Rplus_lt_pos.con";
  94 "cic:/Nijmegen/QArith/Zaux/Zpower_1_subproof.con","cic:/Coq/ZArith/BinInt/Zmult_1_r.con";
  95 "cic:/CoRN/fta/KeyLemma/lem_1c.con","cic:/Coq/Arith/Minus/le_minus.con";
  96 "cic:/Coq/omega/OmegaLemmas/OMEGA20.con","cic:/Coq/omega/OmegaLemmas/OMEGA17.con";
  97 "cic:/Nijmegen/QArith/Zaux/pair_2.con","cic:/Coq/Init/Datatypes/injective_projections.con";
  98 "cic:/Coq/Reals/Rlimit/Rlt_eps4_eps_subproof.con","cic:/Coq/Reals/Rlimit/Rlt_eps2_eps_subproof.con";
  99 "cic:/CoRN/algebra/Basics/le_mult_right.con","cic:/Coq/Arith/Mult/mult_le_compat_r.con";
 100 "cic:/Nijmegen/QArith/Zaux/Zle_lt_plus_plus.con","cic:/Coq/ZArith/Zorder/Zplus_le_lt_compat.con";
 101 "cic:/Rocq/ARITH/Chinese/Nat_complements/lt_minus2.con","cic:/Coq/Reals/ArithProp/lt_minus_O_lt.con";
 102 "cic:/Rocq/THREE_GAP/Nat_compl/not_gt_le.con","cic:/Coq/Arith/Compare_dec/not_gt.con";
 103 "cic:/Rocq/ARITH/Chinese/Nat_complements/mult_commut.con","cic:/Coq/Arith/Mult/mult_comm.con";
 104 "cic:/CoRN/algebra/Basics/lt_mult_right.con","cic:/Coq/Arith/Mult/mult_lt_compat_r.con";
 105 "cic:/Rocq/ARITH/Chinese/Nat_complements/mult_neutr.con","cic:/Coq/Arith/Mult/mult_1_l.con";
 106 "cic:/Nijmegen/QArith/Zaux/Zabs_neg.con","cic:/Coq/ZArith/Zabs/Zabs_non_eq.con";
 107 "cic:/Lyon/FIRING-SQUAD/bib/plus_S.con","cic:/Coq/Init/Peano/plus_Sn_m.con";
 108 "cic:/Nijmegen/QArith/Qhomographic_Qpositive_to_Qpositive/one_non_negative.con","cic:/Coq/ZArith/Zorder/Zle_0_1.con";
 109 "cic:/Coq/fourier/Fourier_util/Rle_zero_1.con","cic:/Coq/Reals/RIneq/Rle_0_1.con";
 110 "cic:/Coq/Logic/Diaconescu/proof_irrel.con","cic:/Coq/Logic/Classical_Prop/proof_irrelevance.con";
 111 "cic:/Coq/Init/Logic/sym_equal.con","cic:/Coq/Init/Logic/sym_eq.con";
 112 "cic:/Coq/IntMap/Mapiter/pair_sp.con","cic:/Coq/Init/Datatypes/surjective_pairing.con";
 113 "cic:/Coq/Logic/ProofIrrelevance/proof_irrelevance_cci.con","cic:/Coq/Logic/Classical_Prop/proof_irrelevance.con";
 114 "cic:/Suresnes/BDD/rauzy/algorithme1/Prelude_BDT/deMorgan_or_not.con","cic:/Coq/Logic/Classical_Prop/not_and_or.con";
 115 "cic:/CoRN/model/structures/Zsec/Zplus_wd0.con","cic:/Coq/ZArith/BinInt/Zplus_eq_compat.con";
 116 "cic:/Coq/ZArith/auxiliary/Zred_factor6.con","cic:/Coq/ZArith/BinInt/Zplus_0_r_reverse.con";
 117 "cic:/Eindhoven/POCKLINGTON/lemmas/S_inj.con","cic:/Coq/Init/Peano/eq_add_S.con";
 118 "cic:/Coq/ZArith/Wf_Z/Z_of_nat_complete.con","cic:/Coq/Reals/RIneq/IZN.con";
 119 "cic:/Suresnes/BDD/rauzy/algorithme1/Prelude_BDT/Commutative_orb.con","cic:/Coq/Bool/Bool/orb_comm.con";
 120 "cic:/Coq/Reals/PartSum/plus_sum.con","cic:/Coq/Reals/Cauchy_prod/sum_plus.con";
 121 "cic:/Nijmegen/QArith/Qpositive/minus_le.con","cic:/Coq/Arith/Minus/le_minus.con";
 122 "cic:/Lyon/FIRING-SQUAD/bib/plus_zero.con","cic:/Coq/Arith/Plus/plus_0_r.con";
 123 "cic:/Sophia-Antipolis/Cours-de-Coq/ex1_auto/not_not_converse.con","cic:/Coq/Logic/Classical_Prop/NNPP.con";
 124 "cic:/Suresnes/BDD/rauzy/algorithme1/Prelude_BDT/deMorgan_and_not.con","cic:/Coq/Logic/Classical_Prop/not_or_and.con";
 125 "cic:/Suresnes/BDD/rauzy/algorithme1/Prelude_BDT/Commutative_andb.con","cic:/Coq/Bool/Bool/andb_comm.con";
 126 "cic:/Sophia-Antipolis/MATHS/Z/Nat_complements/lt_minus2.con","cic:/Coq/Reals/ArithProp/lt_minus_O_lt.con";
 127 "cic:/Suresnes/BDD/canonicite/Prelude0/Morgan_and_not.con","cic:/Coq/Logic/Classical_Prop/not_or_and.con";
 128 "cic:/Coq/Logic/ClassicalFacts/TrueP.con","cic:/Coq/Logic/ClassicalFacts/FalseP.con";
 129 "cic:/Nijmegen/QArith/Zaux/Zminus_eq.con","cic:/Coq/ZArith/BinInt/Zminus_eq.con";
 130 "cic:/Sophia-Antipolis/Cours-de-Coq/ex1/not_not_converse.con","cic:/Coq/Logic/Classical_Prop/NNPP.con";
 131 "cic:/Nijmegen/QArith/Zaux/pair_1.con","cic:/Coq/Init/Datatypes/surjective_pairing.con";
 132 "cic:/Orsay/Maths/divide/Zabs_ind.con","cic:/Coq/ZArith/Zabs/Zabs_ind.con";
 133 "cic:/CoRN/algebra/Basics/Zmult_minus_distr_r.con","cic:/Coq/ZArith/BinInt/Zmult_minus_distr_l.con";
 134 "cic:/Coq/fourier/Fourier_util/Rfourier_eqLR_to_le.con","cic:/Coq/Reals/RIneq/Req_le.con";
 135 "cic:/Rocq/TreeAutomata/bases/Sn_eq_Sm_n_eq_m.con","cic:/Coq/Init/Peano/eq_add_S.con";
 136 "cic:/Coq/Init/Logic/trans_equal.con","cic:/Coq/Init/Logic/trans_eq.con";
 137 "cic:/Coq/omega/OmegaLemmas/OMEGA2.con","cic:/Coq/ZArith/Zorder/Zplus_le_0_compat.con";
 138 "cic:/Sophia-Antipolis/Bertrand/Raux/P_Rmin.con","cic:/Coq/Reals/Rpower/P_Rmin.con";
 139 "cic:/Sophia-Antipolis/MATHS/Z/Nat_complements/mult_commut.con","cic:/Coq/Arith/Mult/mult_comm.con";
 140 "cic:/Sophia-Antipolis/Huffman/Aux/le_minus.con","cic:/Coq/Arith/Minus/le_minus.con";
 141 "cic:/Coq/Init/Peano/plus_O_n.con","cic:/Coq/Arith/Plus/plus_0_l.con";
 142 "cic:/Coq/Logic/Berardi/inv2.con","cic:/Coq/Logic/Berardi/AC.con";
 143 "cic:/Coq/Reals/SeqProp/not_Rlt.con","cic:/Coq/Reals/RIneq/Rnot_lt_ge.con";
 144 "cic:/Nancy/FOUnify/nat_complements/le_S_eqP.con","cic:/Coq/Arith/Compare/le_le_S_eq.con";
 145 "cic:/Rocq/TreeAutomata/bases/le_mult_l.con","cic:/Coq/Arith/Mult/mult_le_compat_r.con";
 146 "cic:/Eindhoven/POCKLINGTON/natZ/isnat_mult.con","cic:/Coq/ZArith/Zorder/Zmult_le_0_compat.con";
 147 "cic:/Coq/fourier/Fourier_util/Rfourier_eqRL_to_le.con","cic:/Coq/Reals/RIneq/Req_le_sym.con";
 148 "cic:/Nijmegen/QArith/Zaux/Zabs_mult.con","cic:/Coq/ZArith/Zabs/Zabs_Zmult.con";
 149 "cic:/Rocq/TreeAutomata/bases/plus_n_O.con","cic:/Coq/Arith/Plus/plus_0_r.con";
 150 "cic:/Suresnes/BDD/rauzy/algorithme1/Prelude_BDT/excluded_middle.con","cic:/Coq/Logic/Classical_Prop/classic.con";
 151 "cic:/Rocq/TreeAutomata/bases/le_mult_mult.con","cic:/Coq/Arith/Mult/mult_le_compat.con";
 152 "cic:/Coq/Bool/Bool/Is_true_eq_true2.con","cic:/Coq/Bool/Bool/Is_true_eq_left.con";
 153 "cic:/Eindhoven/POCKLINGTON/natZ/isnat_plus.con","cic:/Coq/ZArith/Zorder/Zplus_le_0_compat.con";
 154 "cic:/Eindhoven/POCKLINGTON/lemmas/lt_plus_plus.con","cic:/Coq/Arith/Plus/plus_lt_compat.con";
 155 "cic:/Rocq/TreeAutomata/bases/le_mult_r.con","cic:/Coq/Arith/Mult/mult_le_compat_l.con";
 156 "cic:/Sophia-Antipolis/Functions_in_ZFC/Functions_in_ZFC/excluded_middle.con","cic:/Coq/Logic/Classical_Prop/NNPP.con";
 157 "cic:/Sophia-Antipolis/Algebra/Z_group/ax3.con","cic:/Coq/ZArith/Zorder/Zgt_pos_0.con";
 158 "cic:/Nijmegen/QArith/Zaux/Zabs_plus.con","cic:/Coq/ZArith/Zabs/Zabs_triangle.con";
 159 "cic:/Sophia-Antipolis/Buchberger/Buch/Sdep.con","cic:/Coq/Init/Datatypes/prod_ind.con";
 160 "cic:/Coq/Reals/PartSum/Rsum_abs.con","cic:/Coq/Reals/PartSum/Rabs_triang_gen.con";
 161 "cic:/Cachan/SMC/mu/minus_n_m_le_n.con","cic:/Coq/Arith/Minus/le_minus.con";
 162 "cic:/Marseille/GC/lib_arith/lib_S_pred/eqnm_eqSnSm.con","cic:/Coq/Init/Peano/eq_S.con";
 163 "cic:/Nijmegen/QArith/Zaux/Zpower_1_subproof_subproof.con","cic:/Coq/ZArith/BinInt/Zmult_1_r.con";
 164 "cic:/Eindhoven/POCKLINGTON/lemmas/predminus1.con","cic:/Coq/Arith/Minus/pred_of_minus.con";
 165 "cic:/Sophia-Antipolis/Bertrand/Raux/Rpower_pow.con","cic:/Coq/Reals/Rpower/Rpower_pow.con";
 166 "cic:/Lyon/FIRING-SQUAD/bib/lt_plus_plus.con","cic:/Coq/Arith/Plus/plus_lt_compat.con";
 167 "cic:/Eindhoven/POCKLINGTON/lemmas/Zlt_neq.con","cic:/Coq/ZArith/Zorder/Zlt_not_eq.con";
 168 "cic:/Coq/Arith/Lt/nat_total_order.con","cic:/Coq/Arith/Compare_dec/not_eq.con";
 169 "cic:/Rocq/TreeAutomata/bases/plus_O_l.con","cic:/Coq/Arith/Plus/plus_0_r.con";
 170 "cic:/Coq/Logic/ClassicalFacts/boolP.ind#xpointer(1/1/2)","cic:/Coq/Logic/ClassicalFacts/boolP.ind#xpointer(1/1/1)";
 171 "cic:/Nijmegen/QArith/Zaux/Zmult_pos_pos.con","cic:/Coq/ZArith/Zorder/Zmult_lt_O_compat.con";
 172 "cic:/Nijmegen/QArith/Zaux/Zlt_plus_plus.con","cic:/Coq/ZArith/Zorder/Zplus_lt_compat.con";
 173 "cic:/Coq/Logic/Diaconescu/pred_ext_and_rel_choice_imp_EM.con","cic:/Coq/Logic/Classical_Prop/classic.con";
 174 "cic:/Sophia-Antipolis/Rsa/MiscRsa/eq_plus.con","cic:/Coq/Arith/Plus/plus_reg_l.con"
 175 ]
 176 ;;
 177
 178 let equiv_table = Hashtbl.create 503
 179 ;;
 180
 181 let _ = List.iter (fun (a,b) -> Hashtbl.add equiv_table a b) equivalent_objects
 182 ;;
 183
 184 let not_a_duplicate u =
 185   try
 186     ignore(Hashtbl.find equiv_table u); false
 187   with
 188     Not_found -> true
 189 ;;