From: Enrico Tassi Date: Tue, 30 May 2006 10:44:55 +0000 (+0000) Subject: fixed proof generation again X-Git-Tag: make_still_working~7278 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fb99d31806e06e29bed90f08f132d6e8fb758bd8;p=helm.git fixed proof generation again --- diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml index aab75e941..52918d9af 100644 --- a/helm/software/components/tactics/paramodulation/equality.ml +++ b/helm/software/components/tactics/paramodulation/equality.ml @@ -678,7 +678,8 @@ let build_goal_proof l initial ty se = cic, p)) lets (letsno-1,initial) in - canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty)), se + canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty)), + se ;; let refl_proof ty term = diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml index da76559e8..e4dec6397 100644 --- a/helm/software/components/tactics/paramodulation/indexing.ml +++ b/helm/software/components/tactics/paramodulation/indexing.ml @@ -399,7 +399,7 @@ let subsumption_aux use_unification env table target = in (match Subst.merge_subst_if_possible subst subst' with | None -> ok what leftorright tl - | Some s -> Some (s, equation, leftorright)) + | Some s -> Some (s, equation, leftorright <> pos )) with | Inference.MatchingFailure | CicUnification.UnificationFailure _ -> ok what leftorright tl diff --git a/helm/software/components/tactics/paramodulation/indexing.mli b/helm/software/components/tactics/paramodulation/indexing.mli index 8fd618702..a446747e5 100644 --- a/helm/software/components/tactics/paramodulation/indexing.mli +++ b/helm/software/components/tactics/paramodulation/indexing.mli @@ -45,12 +45,12 @@ val unification : Cic.metasenv * Cic.context * CicUniv.universe_graph -> Index.t -> Equality.equality -> - (Subst.substitution * Equality.equality * Utils.pos) option + (Subst.substitution * Equality.equality * bool) option val subsumption : Cic.metasenv * Cic.context * CicUniv.universe_graph -> Index.t -> Equality.equality -> - (Subst.substitution * Equality.equality * Utils.pos) option + (Subst.substitution * Equality.equality * bool) option val superposition_left : Cic.conjecture list * Cic.context * CicUniv.universe_graph -> Index.t -> diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml index 02b080147..b3a53d929 100644 --- a/helm/software/components/tactics/paramodulation/saturation.ml +++ b/helm/software/components/tactics/paramodulation/saturation.ml @@ -896,14 +896,14 @@ let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) = in (* match Indexing.subsumption env table goal_equation with*) match Indexing.unification env table goal_equation with - | Some (subst, equality, pos ) -> + | Some (subst, equality, swapped ) -> prerr_endline ("GOAL SUBSUMED BY: " ^ Equality.string_of_equality equality); prerr_endline ("SUBST:" ^ Subst.ppsubst subst); let (_,p,(ty,l,r,_),m,id) = Equality.open_equality equality in let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in let p = - if pos = Utils.Left then + if swapped then Equality.symmetric eq_ty l id uri m else p diff --git a/helm/software/matita/tests/TPTP/elenco_problemi_veloci_per_test.txt b/helm/software/matita/tests/TPTP/elenco_problemi_veloci_per_test.txt new file mode 100644 index 000000000..d8503a4fc --- /dev/null +++ b/helm/software/matita/tests/TPTP/elenco_problemi_veloci_per_test.txt @@ -0,0 +1,255 @@ +Unsatisfiable/COL007-1.ma +Unsatisfiable/COL012-1.ma +Unsatisfiable/COL013-1.ma +Unsatisfiable/COL058-2.ma +Unsatisfiable/COL060-2.ma +Unsatisfiable/COL060-3.ma +Unsatisfiable/COL061-2.ma +Unsatisfiable/COL061-3.ma +Unsatisfiable/COL062-2.ma +Unsatisfiable/COL062-3.ma +Unsatisfiable/COL063-2.ma +Unsatisfiable/COL063-3.ma +Unsatisfiable/COL063-4.ma +Unsatisfiable/COL063-5.ma +Unsatisfiable/COL063-6.ma +Unsatisfiable/COL064-2.ma +Unsatisfiable/COL064-3.ma +Unsatisfiable/COL064-4.ma +Unsatisfiable/COL064-5.ma +Unsatisfiable/COL064-6.ma +Unsatisfiable/COL064-7.ma +Unsatisfiable/COL064-8.ma +Unsatisfiable/COL064-9.ma +Unsatisfiable/COL085-1.ma +Unsatisfiable/COL086-1.ma +Unsatisfiable/GRP023-2.ma +Unsatisfiable/GRP136-1.ma +Unsatisfiable/GRP137-1.ma +Unsatisfiable/GRP160-1.ma +Unsatisfiable/GRP161-1.ma +Unsatisfiable/GRP454-1.ma +Unsatisfiable/GRP457-1.ma +Unsatisfiable/GRP460-1.ma +Unsatisfiable/GRP463-1.ma +Unsatisfiable/GRP541-1.ma +Unsatisfiable/GRP545-1.ma +Unsatisfiable/GRP549-1.ma +Unsatisfiable/LAT033-1.ma +Unsatisfiable/LAT034-1.ma +Unsatisfiable/ROB030-1.ma +Unsatisfiable/SYN083-1.ma +Unsatisfiable/BOO006-4.ma +Unsatisfiable/BOO011-2.ma +Unsatisfiable/BOO011-4.ma +Unsatisfiable/COL004-3.ma +Unsatisfiable/COL008-1.ma +Unsatisfiable/COL016-1.ma +Unsatisfiable/COL022-1.ma +Unsatisfiable/COL045-1.ma +Unsatisfiable/COL048-1.ma +Unsatisfiable/COL050-1.ma +Unsatisfiable/COL058-3.ma +Unsatisfiable/COL083-1.ma +Unsatisfiable/COL084-1.ma +Unsatisfiable/GRP010-4.ma +Unsatisfiable/GRP022-2.ma +Unsatisfiable/GRP151-1.ma +Unsatisfiable/GRP496-1.ma +Unsatisfiable/GRP542-1.ma +Unsatisfiable/GRP546-1.ma +Unsatisfiable/RNG007-4.ma +Unsatisfiable/ROB010-1.ma +Unsatisfiable/ROB013-1.ma +Unsatisfiable/BOO018-4.ma +Unsatisfiable/COL015-1.ma +Unsatisfiable/COL017-1.ma +Unsatisfiable/COL025-1.ma +Unsatisfiable/GRP011-4.ma +Unsatisfiable/GRP012-4.ma +Unsatisfiable/GRP182-1.ma +Unsatisfiable/GRP481-1.ma +Unsatisfiable/GRP487-1.ma +Unsatisfiable/GRP493-1.ma +Unsatisfiable/GRP550-1.ma +Unsatisfiable/GRP552-1.ma +Unsatisfiable/BOO003-2.ma +Unsatisfiable/BOO006-2.ma +Unsatisfiable/COL018-1.ma +Unsatisfiable/COL024-1.ma +Unsatisfiable/GRP001-4.ma +Unsatisfiable/GRP115-1.ma +Unsatisfiable/GRP117-1.ma +Unsatisfiable/GRP182-3.ma +Unsatisfiable/GRP455-1.ma +Unsatisfiable/GRP458-1.ma +Unsatisfiable/GRP490-1.ma +Unsatisfiable/GRP494-1.ma +Unsatisfiable/GRP544-1.ma +Unsatisfiable/GRP573-1.ma +Unsatisfiable/GRP581-1.ma +Unsatisfiable/LCL132-1.ma +Unsatisfiable/ROB002-1.ma +Unsatisfiable/GRP001-2.ma +Unsatisfiable/GRP142-1.ma +Unsatisfiable/GRP144-1.ma +Unsatisfiable/GRP189-1.ma +Unsatisfiable/GRP206-1.ma +Unsatisfiable/GRP562-1.ma +Unsatisfiable/GRP566-1.ma +Unsatisfiable/GRP569-1.ma +Unsatisfiable/GRP570-1.ma +Unsatisfiable/LDA001-1.ma +Unsatisfiable/GRP173-1.ma +Unsatisfiable/GRP182-2.ma +Unsatisfiable/GRP188-2.ma +Unsatisfiable/GRP484-1.ma +Unsatisfiable/GRP491-1.ma +Unsatisfiable/GRP548-1.ma +Unsatisfiable/GRP558-1.ma +Unsatisfiable/GRP565-1.ma +Unsatisfiable/LCL133-1.ma +Unsatisfiable/LCL134-1.ma +Unsatisfiable/LCL135-1.ma +Unsatisfiable/BOO004-2.ma +Unsatisfiable/BOO009-2.ma +Unsatisfiable/GRP150-1.ma +Unsatisfiable/GRP153-1.ma +Unsatisfiable/GRP174-1.ma +Unsatisfiable/GRP182-4.ma +Unsatisfiable/GRP189-2.ma +Unsatisfiable/BOO010-2.ma +Unsatisfiable/BOO010-4.ma +Unsatisfiable/GRP118-1.ma +Unsatisfiable/GRP143-1.ma +Unsatisfiable/GRP145-1.ma +Unsatisfiable/GRP152-1.ma +Unsatisfiable/GRP188-1.ma +Unsatisfiable/GRP485-1.ma +Unsatisfiable/GRP510-1.ma +Unsatisfiable/GRP577-1.ma +Unsatisfiable/LCL161-1.ma +Unsatisfiable/GRP518-1.ma +Unsatisfiable/GRP520-1.ma +Unsatisfiable/BOO003-4.ma +Unsatisfiable/BOO004-4.ma +Unsatisfiable/GRP514-1.ma +Unsatisfiable/GRP516-1.ma +Unsatisfiable/GRP574-1.ma +Unsatisfiable/GRP586-1.ma +Unsatisfiable/LDA007-3.ma +Unsatisfiable/BOO005-4.ma +Unsatisfiable/COL014-1.ma +Unsatisfiable/GRP139-1.ma +Unsatisfiable/GRP141-1.ma +Unsatisfiable/BOO005-2.ma +Unsatisfiable/GRP497-1.ma +Unsatisfiable/GRP512-1.ma +Unsatisfiable/GRP561-1.ma +Unsatisfiable/GRP564-1.ma +Unsatisfiable/GRP582-1.ma +Unsatisfiable/LCL164-1.ma +Unsatisfiable/GRP590-1.ma +Unsatisfiable/GRP595-1.ma +Unsatisfiable/GRP146-1.ma +Unsatisfiable/GRP149-1.ma +Unsatisfiable/GRP162-1.ma +Unsatisfiable/GRP576-1.ma +Unsatisfiable/RNG024-6.ma +Unsatisfiable/GRP157-1.ma +Unsatisfiable/GRP163-1.ma +Unsatisfiable/GRP456-1.ma +Unsatisfiable/RNG008-4.ma +Unsatisfiable/RNG023-6.ma +Unsatisfiable/GRP459-1.ma +Unsatisfiable/GRP578-1.ma +Unsatisfiable/BOO017-2.ma +Unsatisfiable/GRP159-1.ma +Unsatisfiable/GRP186-3.ma +Unsatisfiable/GRP192-1.ma +Unsatisfiable/GRP560-1.ma +Unsatisfiable/GRP598-1.ma +Unsatisfiable/GRP543-1.ma +Unsatisfiable/BOO016-2.ma +Unsatisfiable/GRP158-1.ma +Unsatisfiable/GRP186-4.ma +Unsatisfiable/GRP572-1.ma +Unsatisfiable/GRP592-1.ma +Unsatisfiable/RNG011-5.ma +Unsatisfiable/GRP495-1.ma +Unsatisfiable/GRP596-1.ma +Unsatisfiable/GRP614-1.ma +Unsatisfiable/LCL156-1.ma +Unsatisfiable/LCL110-2.ma +Unsatisfiable/LCL154-1.ma +Unsatisfiable/LCL157-1.ma +Unsatisfiable/GRP154-1.ma +Unsatisfiable/GRP616-1.ma +Unsatisfiable/LCL112-2.ma +Unsatisfiable/LCL140-1.ma +Unsatisfiable/GRP168-1.ma +Unsatisfiable/GRP612-1.ma +Unsatisfiable/LCL113-2.ma +Unsatisfiable/BOO009-4.ma +Unsatisfiable/GRP116-1.ma +Unsatisfiable/LCL155-1.ma +Unsatisfiable/RNG023-7.ma +Unsatisfiable/RNG024-7.ma +Unsatisfiable/GRP600-1.ma +Unsatisfiable/LCL153-1.ma +Unsatisfiable/LCL158-1.ma +Unsatisfiable/GRP498-1.ma +Unsatisfiable/COL021-1.ma +Unsatisfiable/GRP155-1.ma +Unsatisfiable/GRP176-2.ma +Unsatisfiable/LCL139-1.ma +Unsatisfiable/GRP486-1.ma +Unsatisfiable/GRP606-1.ma +Unsatisfiable/LCL114-2.ma +Unsatisfiable/BOO013-2.ma +Unsatisfiable/GRP156-1.ma +Unsatisfiable/GRP176-1.ma +Unsatisfiable/LAT045-1.ma +Unsatisfiable/GRP168-2.ma +Unsatisfiable/GRP608-1.ma +Unsatisfiable/GRP551-1.ma +Unsatisfiable/GRP588-1.ma +Unsatisfiable/LAT039-1.ma +Unsatisfiable/LAT039-2.ma +Unsatisfiable/GRP584-1.ma +Unsatisfiable/BOO012-2.ma +Unsatisfiable/GRP568-1.ma +Unsatisfiable/GRP492-1.ma +Unsatisfiable/GRP602-1.ma +Unsatisfiable/GRP603-1.ma +Unsatisfiable/GRP467-1.ma +Unsatisfiable/GRP613-1.ma +Unsatisfiable/GRP547-1.ma +Unsatisfiable/BOO012-4.ma +Unsatisfiable/GRP580-1.ma +Unsatisfiable/GRP597-1.ma +Unsatisfiable/GRP517-1.ma +Unsatisfiable/BOO075-1.ma +Unsatisfiable/LCL115-2.ma +Unsatisfiable/LCL141-1.ma +Unsatisfiable/GRP605-1.ma +Unsatisfiable/GRP515-1.ma +Unsatisfiable/GRP509-1.ma +Unsatisfiable/GRP604-1.ma +Unsatisfiable/GRP513-1.ma +Unsatisfiable/GRP556-1.ma +Unsatisfiable/BOO013-4.ma +Unsatisfiable/GRP615-1.ma +Unsatisfiable/BOO001-1.ma +Unsatisfiable/GRP488-1.ma +Unsatisfiable/GRP583-1.ma +Unsatisfiable/GRP511-1.ma +Unsatisfiable/LAT008-1.ma +Unsatisfiable/BOO069-1.ma +Unsatisfiable/ROB009-1.ma +Unsatisfiable/BOO071-1.ma +Unsatisfiable/GRP567-1.ma +Unsatisfiable/BOO034-1.ma +Unsatisfiable/LAT040-1.ma +Unsatisfiable/GRP599-1.ma +Unsatisfiable/COL010-1.ma