# HG changeset patch # User blanchet # Date 1305206959 -7200 # Node ID d6db5a8154770e56ee991b31680b80a52626cedf # Parent e011f632227c16df633bbe308ea0ec7114de1793 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types diff -r e011f632227c -r d6db5a815477 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Thu May 12 15:29:19 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Thu May 12 15:29:19 2011 +0200 @@ -477,80 +477,6 @@ proofs. On the other hand, all HOL infinite types can be given the same models in first-order logic (via Löwenheim-Skolem). *) -fun datatype_constrs thy (T as Type (s, Ts)) = - (case Datatype.get_info thy s of - SOME {index, descr, ...} => - let val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the in - map (apsnd (fn Us => map (typ_of_dtyp descr (dtyps ~~ Ts)) Us ---> T)) - constrs - end - | NONE => []) - | datatype_constrs _ _ = [] - -(* Similar to "Nitpick_HOL.bounded_exact_card_of_type". - 0 means infinite type, 1 means singleton type (e.g., "unit"), and 2 means - cardinality 2 or more. The specified default cardinality is returned if the - cardinality of the type can't be determined. *) -fun tiny_card_of_type ctxt default_card T = - let - val max = 2 (* 1 would be too small for the "fun" case *) - fun aux slack avoid T = - (if member (op =) avoid T then - 0 - else case T of - Type (@{type_name fun}, [T1, T2]) => - (case (aux slack avoid T1, aux slack avoid T2) of - (k, 1) => if slack andalso k = 0 then 0 else 1 - | (0, _) => 0 - | (_, 0) => 0 - | (k1, k2) => - if k1 >= max orelse k2 >= max then max - else Int.min (max, Integer.pow k2 k1)) - | @{typ bool} => 2 (* optimization *) - | @{typ nat} => 0 (* optimization *) - | @{typ int} => 0 (* optimization *) - | Type (s, _) => - let val thy = Proof_Context.theory_of ctxt in - case datatype_constrs thy T of - constrs as _ :: _ => - let - val constr_cards = - map (Integer.prod o map (aux slack (T :: avoid)) o binder_types - o snd) constrs - in - if exists (curry (op =) 0) constr_cards then 0 - else Int.min (max, Integer.sum constr_cards) - end - | [] => - case Typedef.get_info ctxt s of - ({abs_type, rep_type, ...}, _) :: _ => - (* We cheat here by assuming that typedef types are infinite if - their underlying type is infinite. This is unsound in general - but it's hard to think of a realistic example where this would - not be the case. We are also slack with representation types: - If a representation type has the form "sigma => tau", we - consider it enough to check "sigma" for infiniteness. (Look - for "slack" in this function.) *) - (case varify_and_instantiate_type ctxt - (Logic.varifyT_global abs_type) T - (Logic.varifyT_global rep_type) - |> aux true avoid of - 0 => 0 - | 1 => 1 - | _ => default_card) - | [] => default_card - end - | TFree _ => - (* Very slightly unsound: Type variables are assumed not to be - constrained to cardinality 1. (In practice, the user would most - likely have used "unit" directly anyway.) *) - if default_card = 1 then 2 else default_card - | _ => default_card) - in Int.min (max, aux false [] T) end - -fun is_type_surely_finite ctxt T = tiny_card_of_type ctxt 0 T <> 0 -fun is_type_surely_infinite ctxt T = tiny_card_of_type ctxt 1 T = 0 - fun should_encode_type _ _ All_Types _ = true | should_encode_type ctxt _ Finite_Types T = is_type_surely_finite ctxt T | should_encode_type _ nonmono_Ts Nonmonotonic_Types T = diff -r e011f632227c -r d6db5a815477 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu May 12 15:29:19 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu May 12 15:29:19 2011 +0200 @@ -49,7 +49,6 @@ val const_names_in_fact : theory -> (string * typ -> term list -> bool * term list) -> term -> string list - val is_dangerous_term : term -> bool val relevant_facts : Proof.context -> real * real -> int -> (string * typ -> term list -> bool * term list) -> relevance_fudge @@ -737,62 +736,6 @@ (**** Predicates to detect unwanted facts (prolific or likely to cause unsoundness) ****) -(* Too general means, positive equality literal with a variable X as one - operand, when X does not occur properly in the other operand. This rules out - clearly inconsistent facts such as X = a | X = b, though it by no means - guarantees soundness. *) - -(* Unwanted equalities are those between a (bound or schematic) variable that - does not properly occur in the second operand. *) -val is_exhaustive_finite = - let - fun is_bad_equal (Var z) t = - not (exists_subterm (fn Var z' => z = z' | _ => false) t) - | is_bad_equal (Bound j) t = not (loose_bvar1 (t, j)) - | is_bad_equal _ _ = false - fun do_equals t1 t2 = is_bad_equal t1 t2 orelse is_bad_equal t2 t1 - fun do_formula pos t = - case (pos, t) of - (_, @{const Trueprop} $ t1) => do_formula pos t1 - | (true, Const (@{const_name all}, _) $ Abs (_, _, t')) => - do_formula pos t' - | (true, Const (@{const_name All}, _) $ Abs (_, _, t')) => - do_formula pos t' - | (false, Const (@{const_name Ex}, _) $ Abs (_, _, t')) => - do_formula pos t' - | (_, @{const "==>"} $ t1 $ t2) => - do_formula (not pos) t1 andalso - (t2 = @{prop False} orelse do_formula pos t2) - | (_, @{const HOL.implies} $ t1 $ t2) => - do_formula (not pos) t1 andalso - (t2 = @{const False} orelse do_formula pos t2) - | (_, @{const Not} $ t1) => do_formula (not pos) t1 - | (true, @{const HOL.disj} $ t1 $ t2) => forall (do_formula pos) [t1, t2] - | (false, @{const HOL.conj} $ t1 $ t2) => forall (do_formula pos) [t1, t2] - | (true, Const (@{const_name HOL.eq}, _) $ t1 $ t2) => do_equals t1 t2 - | (true, Const (@{const_name "=="}, _) $ t1 $ t2) => do_equals t1 t2 - | _ => false - in do_formula true end - -fun has_bound_or_var_of_type tycons = - exists_subterm (fn Var (_, Type (s, _)) => member (op =) tycons s - | Abs (_, Type (s, _), _) => member (op =) tycons s - | _ => false) - -(* Facts are forbidden to contain variables of these types. The typical reason - is that they lead to unsoundness. Note that "unit" satisfies numerous - equations like "?x = ()". The resulting clauses will have no type constraint, - yielding false proofs. Even "bool" leads to many unsound proofs, though only - for higher-order problems. *) -val dangerous_types = [@{type_name unit}, @{type_name bool}, @{type_name prop}] - -(* Facts containing variables of type "unit" or "bool" or of the form - "ALL x. x = A | x = B | x = C" are likely to lead to unsound proofs if types - are omitted. *) -val is_dangerous_term = - transform_elim_term - #> (has_bound_or_var_of_type dangerous_types orf is_exhaustive_finite) - fun is_theorem_bad_for_atps thm = let val t = prop_of thm in is_formula_too_complex t orelse exists_type type_has_top_sort t orelse diff -r e011f632227c -r d6db5a815477 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu May 12 15:29:19 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu May 12 15:29:19 2011 +0200 @@ -339,6 +339,62 @@ (* generic TPTP-based ATPs *) +(* Too general means, positive equality literal with a variable X as one + operand, when X does not occur properly in the other operand. This rules out + clearly inconsistent facts such as X = a | X = b, though it by no means + guarantees soundness. *) + +(* Unwanted equalities are those between a (bound or schematic) variable that + does not properly occur in the second operand. *) +val is_exhaustive_finite = + let + fun is_bad_equal (Var z) t = + not (exists_subterm (fn Var z' => z = z' | _ => false) t) + | is_bad_equal (Bound j) t = not (loose_bvar1 (t, j)) + | is_bad_equal _ _ = false + fun do_equals t1 t2 = is_bad_equal t1 t2 orelse is_bad_equal t2 t1 + fun do_formula pos t = + case (pos, t) of + (_, @{const Trueprop} $ t1) => do_formula pos t1 + | (true, Const (@{const_name all}, _) $ Abs (_, _, t')) => + do_formula pos t' + | (true, Const (@{const_name All}, _) $ Abs (_, _, t')) => + do_formula pos t' + | (false, Const (@{const_name Ex}, _) $ Abs (_, _, t')) => + do_formula pos t' + | (_, @{const "==>"} $ t1 $ t2) => + do_formula (not pos) t1 andalso + (t2 = @{prop False} orelse do_formula pos t2) + | (_, @{const HOL.implies} $ t1 $ t2) => + do_formula (not pos) t1 andalso + (t2 = @{const False} orelse do_formula pos t2) + | (_, @{const Not} $ t1) => do_formula (not pos) t1 + | (true, @{const HOL.disj} $ t1 $ t2) => forall (do_formula pos) [t1, t2] + | (false, @{const HOL.conj} $ t1 $ t2) => forall (do_formula pos) [t1, t2] + | (true, Const (@{const_name HOL.eq}, _) $ t1 $ t2) => do_equals t1 t2 + | (true, Const (@{const_name "=="}, _) $ t1 $ t2) => do_equals t1 t2 + | _ => false + in do_formula true end + +fun has_bound_or_var_of_type pred = + exists_subterm (fn Var (_, T as Type _) => pred T + | Abs (_, T as Type _, _) => pred T + | _ => false) + +(* Facts are forbidden to contain variables of these types. The typical reason + is that they lead to unsoundness. Note that "unit" satisfies numerous + equations like "?x = ()". The resulting clauses will have no type constraint, + yielding false proofs. Even "bool" leads to many unsound proofs, though only + for higher-order problems. *) + +(* Facts containing variables of type "unit" or "bool" or of the form + "ALL x. x = A | x = B | x = C" are likely to lead to unsound proofs if types + are omitted. *) +fun is_dangerous_term ctxt = + transform_elim_term + #> (has_bound_or_var_of_type (is_type_surely_finite ctxt) orf + is_exhaustive_finite) + fun int_opt_add (SOME m) (SOME n) = SOME (m + n) | int_opt_add _ _ = NONE @@ -448,7 +504,7 @@ val fairly_sound = is_type_sys_fairly_sound type_sys val facts = facts |> not fairly_sound - ? filter_out (is_dangerous_term o prop_of o snd + ? filter_out (is_dangerous_term ctxt o prop_of o snd o untranslated_fact) |> take num_facts |> not (null blacklist) diff -r e011f632227c -r d6db5a815477 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu May 12 15:29:19 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu May 12 15:29:19 2011 +0200 @@ -21,6 +21,8 @@ val varify_type : Proof.context -> typ -> typ val instantiate_type : theory -> typ -> typ -> typ -> typ val varify_and_instantiate_type : Proof.context -> typ -> typ -> typ -> typ + val is_type_surely_finite : Proof.context -> typ -> bool + val is_type_surely_infinite : Proof.context -> typ -> bool val monomorphic_term : Type.tyenv -> term -> term val eta_expand : typ list -> term -> int -> term val transform_elim_term : term -> term @@ -110,6 +112,81 @@ instantiate_type thy (varify_type ctxt T1) T1' (varify_type ctxt T2) end +fun datatype_constrs thy (T as Type (s, Ts)) = + (case Datatype.get_info thy s of + SOME {index, descr, ...} => + let val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the in + map (apsnd (fn Us => map (typ_of_dtyp descr (dtyps ~~ Ts)) Us ---> T)) + constrs + end + | NONE => []) + | datatype_constrs _ _ = [] + +(* Similar to "Nitpick_HOL.bounded_exact_card_of_type". + 0 means infinite type, 1 means singleton type (e.g., "unit"), and 2 means + cardinality 2 or more. The specified default cardinality is returned if the + cardinality of the type can't be determined. *) +fun tiny_card_of_type ctxt default_card T = + let + val max = 2 (* 1 would be too small for the "fun" case *) + fun aux slack avoid T = + (if member (op =) avoid T then + 0 + else case T of + Type (@{type_name fun}, [T1, T2]) => + (case (aux slack avoid T1, aux slack avoid T2) of + (k, 1) => if slack andalso k = 0 then 0 else 1 + | (0, _) => 0 + | (_, 0) => 0 + | (k1, k2) => + if k1 >= max orelse k2 >= max then max + else Int.min (max, Integer.pow k2 k1)) + | @{typ prop} => 2 + | @{typ bool} => 2 (* optimization *) + | @{typ nat} => 0 (* optimization *) + | @{typ int} => 0 (* optimization *) + | Type (s, _) => + let val thy = Proof_Context.theory_of ctxt in + case datatype_constrs thy T of + constrs as _ :: _ => + let + val constr_cards = + map (Integer.prod o map (aux slack (T :: avoid)) o binder_types + o snd) constrs + in + if exists (curry (op =) 0) constr_cards then 0 + else Int.min (max, Integer.sum constr_cards) + end + | [] => + case Typedef.get_info ctxt s of + ({abs_type, rep_type, ...}, _) :: _ => + (* We cheat here by assuming that typedef types are infinite if + their underlying type is infinite. This is unsound in general + but it's hard to think of a realistic example where this would + not be the case. We are also slack with representation types: + If a representation type has the form "sigma => tau", we + consider it enough to check "sigma" for infiniteness. (Look + for "slack" in this function.) *) + (case varify_and_instantiate_type ctxt + (Logic.varifyT_global abs_type) T + (Logic.varifyT_global rep_type) + |> aux true avoid of + 0 => 0 + | 1 => 1 + | _ => default_card) + | [] => default_card + end + | TFree _ => + (* Very slightly unsound: Type variables are assumed not to be + constrained to cardinality 1. (In practice, the user would most + likely have used "unit" directly anyway.) *) + if default_card = 1 then 2 else default_card + | _ => default_card) + in Int.min (max, aux false [] T) end + +fun is_type_surely_finite ctxt T = tiny_card_of_type ctxt 0 T <> 0 +fun is_type_surely_infinite ctxt T = tiny_card_of_type ctxt 1 T = 0 + fun monomorphic_term subst t = map_types (map_type_tvar (fn v => case Type.lookup subst v of