# HG changeset patch # User blanchet # Date 1303417108 -7200 # Node ID 494e4ac5b0f82d2209d8ddfa7b5d7dfbf9d4ef0c # Parent 95b2626c75a8e535d3fd77e6e42e9735031f81d0 detect some unsound proofs before showing them to the user diff -r 95b2626c75a8 -r 494e4ac5b0f8 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Apr 21 21:14:06 2011 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Apr 21 22:18:28 2011 +0200 @@ -378,7 +378,7 @@ val relevance_override = {add = [], del = [], only = false} val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i val no_dangerous_types = - Sledgehammer_ATP_Translate.types_dangerous_types type_sys + Sledgehammer_ATP_Translate.type_system_types_dangerous_types type_sys val time_limit = (case hard_timeout of NONE => I diff -r 95b2626c75a8 -r 494e4ac5b0f8 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Thu Apr 21 21:14:06 2011 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Thu Apr 21 22:18:28 2011 +0200 @@ -126,7 +126,7 @@ val subgoal = 1 val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal subgoal val no_dangerous_types = - Sledgehammer_ATP_Translate.types_dangerous_types type_sys + Sledgehammer_ATP_Translate.type_system_types_dangerous_types type_sys val facts = Sledgehammer_Filter.relevant_facts ctxt no_dangerous_types relevance_thresholds diff -r 95b2626c75a8 -r 494e4ac5b0f8 src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Thu Apr 21 21:14:06 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Thu Apr 21 22:18:28 2011 +0200 @@ -171,7 +171,6 @@ end in add 0 |> apsnd SOME end - fun nice_term (ATerm (name, ts)) = nice_name name ##>> pool_map nice_term ts #>> ATerm fun nice_formula (AQuant (q, xs, phi)) = diff -r 95b2626c75a8 -r 494e4ac5b0f8 src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Thu Apr 21 21:14:06 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_proof.ML Thu Apr 21 22:18:28 2011 +0200 @@ -12,10 +12,10 @@ type 'a uniform_formula = 'a ATP_Problem.uniform_formula datatype failure = - Unprovable | IncompleteUnprovable | ProofMissing | CantConnect | TimedOut | - OutOfResources | SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl | - NoRealZ3 | MalformedInput | MalformedOutput | Interrupted | Crashed | - InternalError | UnknownError of string + Unprovable | IncompleteUnprovable | ProofMissing | UnsoundProof | + CantConnect | TimedOut | OutOfResources | SpassTooOld | VampireTooOld | + NoPerl | NoLibwwwPerl | NoRealZ3 | MalformedInput | MalformedOutput | + Interrupted | Crashed | InternalError | UnknownError of string type step_name = string * string option @@ -35,7 +35,7 @@ bool -> bool -> bool -> int -> (string * string) list -> (failure * string) list -> string -> string * failure option val is_same_step : step_name * step_name -> bool - val atp_proof_from_tstplike_string : bool -> string -> string proof + val atp_proof_from_tstplike_proof : string -> string proof val map_term_names_in_atp_proof : (string -> string) -> string proof -> string proof val nasty_atp_proof : string Symtab.table -> string proof -> string proof @@ -47,10 +47,10 @@ open ATP_Problem datatype failure = - Unprovable | IncompleteUnprovable | ProofMissing | CantConnect | TimedOut | - OutOfResources | SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl | - NoRealZ3 | MalformedInput | MalformedOutput | Interrupted | Crashed | - InternalError | UnknownError of string + Unprovable | IncompleteUnprovable | ProofMissing | UnsoundProof | + CantConnect | TimedOut | OutOfResources | SpassTooOld | VampireTooOld | + NoPerl | NoLibwwwPerl | NoRealZ3 | MalformedInput | MalformedOutput | + Interrupted | Crashed | InternalError | UnknownError of string fun strip_spaces_in_list _ [] = [] | strip_spaces_in_list _ [c1] = if Char.isSpace c1 then [] else [str c1] @@ -95,6 +95,9 @@ "The prover gave up." | string_for_failure ProofMissing = "The prover claims the conjecture is a theorem but did not provide a proof." + | string_for_failure UnsoundProof = + "The prover found a type-incorrect proof. (Or, very unlikely, your axioms \ + \are inconsistent.)" | string_for_failure CantConnect = "Cannot connect to remote server." | string_for_failure TimedOut = "Timed out." | string_for_failure OutOfResources = "The prover ran out of resources." @@ -366,11 +369,12 @@ Inference (name, u, map_filter (clean_up_dependency seen) deps) :: clean_up_dependencies (name :: seen) steps -fun atp_proof_from_tstplike_string clean = - suffix "$" (* the $ sign acts as a sentinel (FIXME: needed?) *) - #> parse_proof - #> clean ? (sort (step_name_ord o pairself step_name) - #> clean_up_dependencies []) +fun atp_proof_from_tstplike_proof "" = [] + | atp_proof_from_tstplike_proof s = + s ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *) + |> parse_proof + |> sort (step_name_ord o pairself step_name) + |> clean_up_dependencies [] fun map_term_names_in_term f (ATerm (s, ts)) = ATerm (f s, map (map_term_names_in_term f) ts) diff -r 95b2626c75a8 -r 494e4ac5b0f8 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Thu Apr 21 21:14:06 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Thu Apr 21 22:18:28 2011 +0200 @@ -243,6 +243,7 @@ known_failures = [(Unprovable, "UNPROVABLE"), (IncompleteUnprovable, "CANNOT PROVE"), + (IncompleteUnprovable, "SZS status GaveUp"), (ProofMissing, "[predicate definition introduction]"), (ProofMissing, "predicate_definition_introduction,[]"), (* TSTP *) (TimedOut, "SZS status Timeout"), diff -r 95b2626c75a8 -r 494e4ac5b0f8 src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Thu Apr 21 21:14:06 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Thu Apr 21 22:18:28 2011 +0200 @@ -8,11 +8,12 @@ signature SLEDGEHAMMER_ATP_RECONSTRUCT = sig + type 'a proof = 'a ATP_Proof.proof type locality = Sledgehammer_Filter.locality type type_system = Sledgehammer_ATP_Translate.type_system type minimize_command = string list -> string type metis_params = - string * type_system * minimize_command * string + string * type_system * minimize_command * string proof * (string * locality) list vector * thm * int type isar_params = string Symtab.table * bool * int * Proof.context * int list list @@ -21,6 +22,8 @@ val repair_conjecture_shape_and_fact_names : string -> int list list -> (string * locality) list vector -> int list list * (string * locality) list vector + val is_unsound_proof : + int list list -> (string * locality) list vector -> string proof -> bool val apply_on_subgoal : string -> int -> int -> string val command_call : string -> string list -> string val try_command_line : string -> string -> string @@ -45,7 +48,7 @@ type minimize_command = string list -> string type metis_params = - string * type_system * minimize_command * string + string * type_system * minimize_command * string proof * (string * locality) list vector * thm * int type isar_params = string Symtab.table * bool * int * Proof.context * int list list @@ -115,39 +118,6 @@ else (conjecture_shape, fact_names) - -(** Soft-core proof reconstruction: Metis one-liner **) - -fun string_for_label (s, num) = s ^ string_of_int num - -fun set_settings "" = "" - | set_settings settings = "using [[" ^ settings ^ "]] " -fun apply_on_subgoal settings _ 1 = set_settings settings ^ "by " - | apply_on_subgoal settings 1 _ = set_settings settings ^ "apply " - | apply_on_subgoal settings i n = - "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal settings 1 n -fun command_call name [] = name - | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")" -fun try_command_line banner command = - banner ^ ": " ^ Markup.markup Markup.sendback command ^ "." -fun using_labels [] = "" - | using_labels ls = - "using " ^ space_implode " " (map string_for_label ls) ^ " " -fun metis_name type_sys = - if types_dangerous_types type_sys then "metisFT" else "metis" -fun metis_call type_sys ss = command_call (metis_name type_sys) ss -fun metis_command type_sys i n (ls, ss) = - using_labels ls ^ apply_on_subgoal "" i n ^ metis_call type_sys ss -fun metis_line banner type_sys i n ss = - try_command_line banner (metis_command type_sys i n ([], ss)) -fun minimize_line _ [] = "" - | minimize_line minimize_command ss = - case minimize_command ss of - "" => "" - | command => - "\nTo minimize the number of lemmas, try this: " ^ - Markup.markup Markup.sendback command ^ "." - val vampire_step_prefix = "f" (* grrr... *) fun resolve_fact fact_names ((_, SOME s)) = @@ -168,27 +138,77 @@ [] | NONE => [] +fun resolve_conjecture conjecture_shape (num, s_opt) = + let + val k = case try (unprefix conjecture_prefix) (the_default "" s_opt) of + SOME s => Int.fromString s |> the_default ~1 + | NONE => case Int.fromString num of + SOME j => find_index (exists (curry (op =) j)) + conjecture_shape + | NONE => ~1 + in if k >= 0 then [k] else [] end + +fun is_fact conjecture_shape = not o null o resolve_fact conjecture_shape +fun is_conjecture conjecture_shape = + not o null o resolve_conjecture conjecture_shape + fun add_fact fact_names (Inference (name, _, [])) = append (resolve_fact fact_names name) | add_fact _ _ = I -fun used_facts_in_tstplike_proof fact_names tstplike_proof = - if tstplike_proof = "" then - Vector.foldl (op @) [] fact_names - else - tstplike_proof - |> atp_proof_from_tstplike_string false - |> rpair [] |-> fold (add_fact fact_names) +fun used_facts_in_atp_proof fact_names atp_proof = + if null atp_proof then Vector.foldl (op @) [] fact_names + else fold (add_fact fact_names) atp_proof [] + +fun is_conjecture_referred_to_in_proof conjecture_shape = + exists (fn Inference (name, _, []) => is_conjecture conjecture_shape name + | _ => false) + +fun is_unsound_proof conjecture_shape fact_names = + (not o is_conjecture_referred_to_in_proof conjecture_shape) andf + forall (is_global_locality o snd) o used_facts_in_atp_proof fact_names + +(** Soft-core proof reconstruction: Metis one-liner **) + +fun string_for_label (s, num) = s ^ string_of_int num + +fun set_settings "" = "" + | set_settings settings = "using [[" ^ settings ^ "]] " +fun apply_on_subgoal settings _ 1 = set_settings settings ^ "by " + | apply_on_subgoal settings 1 _ = set_settings settings ^ "apply " + | apply_on_subgoal settings i n = + "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal settings 1 n +fun command_call name [] = name + | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")" +fun try_command_line banner command = + banner ^ ": " ^ Markup.markup Markup.sendback command ^ "." +fun using_labels [] = "" + | using_labels ls = + "using " ^ space_implode " " (map string_for_label ls) ^ " " +fun metis_name type_sys = + if type_system_types_dangerous_types type_sys then "metisFT" else "metis" +fun metis_call type_sys ss = command_call (metis_name type_sys) ss +fun metis_command type_sys i n (ls, ss) = + using_labels ls ^ apply_on_subgoal "" i n ^ metis_call type_sys ss +fun metis_line banner type_sys i n ss = + try_command_line banner (metis_command type_sys i n ([], ss)) +fun minimize_line _ [] = "" + | minimize_line minimize_command ss = + case minimize_command ss of + "" => "" + | command => + "\nTo minimize the number of lemmas, try this: " ^ + Markup.markup Markup.sendback command ^ "." val split_used_facts = List.partition (curry (op =) Chained o snd) #> pairself (sort_distinct (string_ord o pairself fst)) -fun metis_proof_text (banner, type_sys, minimize_command, tstplike_proof, - fact_names, goal, i) = +fun metis_proof_text (banner, type_sys, minimize_command, atp_proof, fact_names, + goal, i) = let val (chained_lemmas, other_lemmas) = - split_used_facts (used_facts_in_tstplike_proof fact_names tstplike_proof) + split_used_facts (used_facts_in_atp_proof fact_names atp_proof) val n = Logic.count_prems (prop_of goal) in (metis_line banner type_sys i n (map fst other_lemmas) ^ @@ -196,7 +216,6 @@ other_lemmas @ chained_lemmas) end - (** Hard-core proof reconstruction: structured Isar proofs **) (* Simple simplifications to ensure that sort annotations don't leave a trail of @@ -241,19 +260,6 @@ val assum_prefix = "A" val have_prefix = "F" -fun resolve_conjecture conjecture_shape (num, s_opt) = - let - val k = case try (unprefix conjecture_prefix) (the_default "" s_opt) of - SOME s => Int.fromString s |> the_default ~1 - | NONE => case Int.fromString num of - SOME j => find_index (exists (curry (op =) j)) - conjecture_shape - | NONE => ~1 - in if k >= 0 then [k] else [] end - -fun is_fact conjecture_shape = not o null o resolve_fact conjecture_shape -fun is_conjecture conjecture_shape = not o null o resolve_conjecture conjecture_shape - fun raw_label_for_name conjecture_shape name = case resolve_conjecture conjecture_shape name of [j] => (conjecture_prefix, j) @@ -621,12 +627,11 @@ else s -fun isar_proof_from_tstplike_proof pool ctxt type_sys tfrees isar_shrink_factor - tstplike_proof conjecture_shape fact_names params frees = +fun isar_proof_from_atp_proof pool ctxt type_sys tfrees isar_shrink_factor + atp_proof conjecture_shape fact_names params frees = let val lines = - tstplike_proof - |> atp_proof_from_tstplike_string true + atp_proof |> nasty_atp_proof pool |> map_term_names_in_atp_proof repair_name |> decode_lines ctxt type_sys tfrees @@ -929,8 +934,7 @@ in do_proof end fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape) - (metis_params as (_, type_sys, _, tstplike_proof, - fact_names, goal, i)) = + (metis_params as (_, type_sys, _, atp_proof, fact_names, goal, i)) = let val (params, hyp_ts, concl_t) = strip_subgoal goal i val frees = fold Term.add_frees (concl_t :: hyp_ts) [] @@ -938,9 +942,9 @@ val n = Logic.count_prems (prop_of goal) val (one_line_proof, lemma_names) = metis_proof_text metis_params fun isar_proof_for () = - case isar_proof_from_tstplike_proof pool ctxt type_sys tfrees - isar_shrink_factor tstplike_proof conjecture_shape fact_names - params frees + case isar_proof_from_atp_proof pool ctxt type_sys tfrees + isar_shrink_factor atp_proof conjecture_shape fact_names params + frees |> redirect_proof hyp_ts concl_t |> kill_duplicate_assumptions_in_proof |> then_chain_proof diff -r 95b2626c75a8 -r 494e4ac5b0f8 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Thu Apr 21 21:14:06 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Thu Apr 21 22:18:28 2011 +0200 @@ -21,7 +21,8 @@ val precise_overloaded_args : bool Unsynchronized.ref val fact_prefix : string val conjecture_prefix : string - val types_dangerous_types : type_system -> bool + val is_type_system_sound : type_system -> bool + val type_system_types_dangerous_types : type_system -> bool val num_atp_type_args : theory -> type_system -> string -> int val translate_atp_fact : Proof.context -> bool -> (string * 'a) * thm @@ -67,8 +68,11 @@ Mangled | No_Types -fun types_dangerous_types (Tags _) = true - | types_dangerous_types _ = false +fun is_type_system_sound (Tags true) = true + | is_type_system_sound _ = false + +fun type_system_types_dangerous_types (Tags _) = true + | type_system_types_dangerous_types _ = false (* This is an approximation. If it returns "true" for a constant that isn't overloaded (i.e., that has one uniform definition), needless clutter is @@ -289,7 +293,7 @@ fun get_helper_facts ctxt explicit_forall type_sys formulas = let - val no_dangerous_types = types_dangerous_types type_sys + val no_dangerous_types = type_system_types_dangerous_types type_sys val ct = init_counters |> fold count_formula formulas fun is_used s = the (Symtab.lookup ct s) > 0 fun dub c needs_full_types (th, j) = diff -r 95b2626c75a8 -r 494e4ac5b0f8 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu Apr 21 21:14:06 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu Apr 21 22:18:28 2011 +0200 @@ -36,6 +36,7 @@ only : bool} val trace : bool Unsynchronized.ref + val is_global_locality : locality -> bool val fact_from_ref : Proof.context -> unit Symtab.table -> thm list -> Facts.ref * Attrib.src list -> ((string * locality) * thm) list @@ -66,6 +67,12 @@ datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained +(* (quasi-)underapproximation of the truth *) +fun is_global_locality Local = false + | is_global_locality Assum = false + | is_global_locality Chained = false + | is_global_locality _ = true + type relevance_fudge = {allow_ext : bool, local_const_multiplier : real, diff -r 95b2626c75a8 -r 494e4ac5b0f8 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Apr 21 21:14:06 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Apr 21 22:18:28 2011 +0200 @@ -457,23 +457,37 @@ else I) |>> (if measure_run_time then split_time else rpair NONE) - val (tstplike_proof, outcome) = + val (atp_proof, outcome) = extract_tstplike_proof_and_outcome debug verbose complete res_code proof_delims known_failures output + |>> atp_proof_from_tstplike_proof + val (conjecture_shape, fact_names) = + if is_none outcome then + repair_conjecture_shape_and_fact_names output + conjecture_shape fact_names + else + (conjecture_shape, fact_names) (* don't bother repairing *) + val outcome = + if is_none outcome andalso + not (is_type_system_sound type_sys) andalso + is_unsound_proof conjecture_shape fact_names atp_proof then + SOME UnsoundProof + else + outcome in ((pool, conjecture_shape, fact_names), - (output, msecs, tstplike_proof, outcome)) + (output, msecs, atp_proof, outcome)) end val timer = Timer.startRealTimer () fun maybe_run_slice slice (_, (_, msecs0, _, SOME _)) = run_slice slice (Time.- (timeout, Timer.checkRealTimer timer)) - |> (fn (stuff, (output, msecs, tstplike_proof, outcome)) => - (stuff, (output, int_opt_add msecs0 msecs, - tstplike_proof, outcome))) + |> (fn (stuff, (output, msecs, atp_proof, outcome)) => + (stuff, (output, int_opt_add msecs0 msecs, atp_proof, + outcome))) | maybe_run_slice _ result = result in ((Symtab.empty, [], Vector.fromList []), - ("", SOME 0, "", SOME InternalError)) + ("", SOME 0, [], SOME InternalError)) |> fold maybe_run_slice actual_slices end else @@ -489,10 +503,8 @@ else File.write (Path.explode (Path.implode prob_file ^ "_proof")) output val ((pool, conjecture_shape, fact_names), - (output, msecs, tstplike_proof, outcome)) = + (output, msecs, atp_proof, outcome)) = with_path cleanup export run_on problem_path_name - val (conjecture_shape, fact_names) = - repair_conjecture_shape_and_fact_names output conjecture_shape fact_names val important_message = if not auto andalso random () <= atp_important_message_keep_factor then extract_important_message output @@ -511,8 +523,8 @@ "") val isar_params = (pool, debug, isar_shrink_factor, ctxt, conjecture_shape) val metis_params = - (proof_banner auto, type_sys, minimize_command, tstplike_proof, - fact_names, goal, subgoal) + (proof_banner auto, type_sys, minimize_command, atp_proof, fact_names, + goal, subgoal) val (outcome, (message, used_facts)) = case outcome of NONE => diff -r 95b2626c75a8 -r 494e4ac5b0f8 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Apr 21 21:14:06 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Apr 21 22:18:28 2011 +0200 @@ -183,7 +183,7 @@ val thy = Proof_Context.theory_of ctxt val {facts = chained_ths, goal, ...} = Proof.goal state val (_, hyp_ts, concl_t) = strip_subgoal goal i - val no_dangerous_types = types_dangerous_types type_sys + val no_dangerous_types = type_system_types_dangerous_types type_sys val _ = () |> not blocking ? kill_provers val _ = case find_first (not o is_prover_supported ctxt) provers of SOME name => error ("No such prover: " ^ name ^ ".") diff -r 95b2626c75a8 -r 494e4ac5b0f8 src/HOL/ex/sledgehammer_tactics.ML --- a/src/HOL/ex/sledgehammer_tactics.ML Thu Apr 21 21:14:06 2011 +0200 +++ b/src/HOL/ex/sledgehammer_tactics.ML Thu Apr 21 22:18:28 2011 +0200 @@ -33,7 +33,7 @@ val relevance_override = {add = [], del = [], only = false} val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i val no_dangerous_types = - Sledgehammer_ATP_Translate.types_dangerous_types type_sys + Sledgehammer_ATP_Translate.type_system_types_dangerous_types type_sys val facts = Sledgehammer_Filter.relevant_facts ctxt no_dangerous_types relevance_thresholds