(* 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 ;;