src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
author blanchet
Mon Jun 02 17:34:26 2014 +0200 (2014-06-02 ago)
changeset 57158 f028d93798e6
parent 57154 f0eff6393a32
child 57286 4868ec62f533
permissions -rw-r--r--
simplified counterexample handling
     1 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Author:     Steffen Juilf Smolka, TU Muenchen
     4 
     5 Basic data structures for representing and basic methods
     6 for dealing with Isar proof texts.
     7 *)
     8 
     9 signature SLEDGEHAMMER_ISAR_PROOF =
    10 sig
    11   type proof_method = Sledgehammer_Proof_Methods.proof_method
    12 
    13   type label = string * int
    14   type facts = label list * string list (* local and global facts *)
    15 
    16   datatype isar_qualifier = Show | Then
    17 
    18   datatype isar_proof =
    19     Proof of (string * typ) list * (label * term) list * isar_step list
    20   and isar_step =
    21     Let of term * term |
    22     Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list
    23       * facts * proof_method list * string
    24 
    25   val no_label : label
    26 
    27   val label_ord : label * label -> order
    28   val string_of_label : label -> string
    29 
    30   val steps_of_isar_proof : isar_proof -> isar_step list
    31 
    32   val label_of_isar_step : isar_step -> label option
    33   val facts_of_isar_step : isar_step -> facts
    34   val proof_methods_of_isar_step : isar_step -> proof_method list
    35 
    36   val fold_isar_steps : (isar_step -> 'a -> 'a) -> isar_step list -> 'a -> 'a
    37   val map_isar_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof
    38   val add_isar_steps : isar_step list -> int -> int
    39 
    40   structure Canonical_Label_Tab : TABLE
    41 
    42   val canonical_label_ord : (label * label) -> order
    43 
    44   val comment_isar_proof : (label -> proof_method list -> string) -> isar_proof -> isar_proof
    45   val chain_isar_proof : isar_proof -> isar_proof
    46   val kill_useless_labels_in_isar_proof : isar_proof -> isar_proof
    47   val relabel_isar_proof_canonically : isar_proof -> isar_proof
    48   val relabel_isar_proof_nicely : isar_proof -> isar_proof
    49 
    50   val string_of_isar_proof : Proof.context -> int -> int -> isar_proof -> string
    51 end;
    52 
    53 structure Sledgehammer_Isar_Proof : SLEDGEHAMMER_ISAR_PROOF =
    54 struct
    55 
    56 open ATP_Util
    57 open ATP_Proof
    58 open ATP_Problem_Generate
    59 open ATP_Proof_Reconstruct
    60 open Sledgehammer_Util
    61 open Sledgehammer_Proof_Methods
    62 open Sledgehammer_Isar_Annotate
    63 
    64 type label = string * int
    65 type facts = label list * string list (* local and global facts *)
    66 
    67 datatype isar_qualifier = Show | Then
    68 
    69 datatype isar_proof =
    70   Proof of (string * typ) list * (label * term) list * isar_step list
    71 and isar_step =
    72   Let of term * term |
    73   Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list
    74     * facts * proof_method list * string
    75 
    76 val no_label = ("", ~1)
    77 
    78 val label_ord = pairself swap #> prod_ord int_ord fast_string_ord
    79 
    80 fun string_of_label (s, num) = s ^ string_of_int num
    81 
    82 fun steps_of_isar_proof (Proof (_, _, steps)) = steps
    83 
    84 fun label_of_isar_step (Prove (_, _, l, _, _, _, _, _)) = SOME l
    85   | label_of_isar_step _ = NONE
    86 
    87 fun subproofs_of_isar_step (Prove (_, _, _, _, subs, _, _, _)) = subs
    88   | subproofs_of_isar_step _ = []
    89 
    90 fun facts_of_isar_step (Prove (_, _, _, _, _, facts, _, _)) = facts
    91   | facts_of_isar_step _ = ([], [])
    92 
    93 fun proof_methods_of_isar_step (Prove (_, _, _, _, _, _, meths, _)) = meths
    94   | proof_methods_of_isar_step _ = []
    95 
    96 fun fold_isar_step f step =
    97   fold (steps_of_isar_proof #> fold_isar_steps f) (subproofs_of_isar_step step) #> f step
    98 and fold_isar_steps f = fold (fold_isar_step f)
    99 
   100 fun map_isar_steps f =
   101   let
   102     fun map_proof (Proof (fix, assms, steps)) = Proof (fix, assms, map map_step steps)
   103     and map_step (step as Let _) = f step
   104       | map_step (Prove (qs, xs, l, t, subs, facts, meths, comment)) =
   105         f (Prove (qs, xs, l, t, map map_proof subs, facts, meths, comment))
   106   in map_proof end
   107 
   108 val add_isar_steps = fold_isar_steps (fn Prove _ => Integer.add 1 | _ => I)
   109 
   110 (* canonical proof labels: 1, 2, 3, ... in post traversal order *)
   111 fun canonical_label_ord (((_, i1), (_, i2)) : label * label) = int_ord (i1, i2)
   112 
   113 structure Canonical_Label_Tab = Table(
   114   type key = label
   115   val ord = canonical_label_ord)
   116 
   117 fun comment_isar_step comment_of (Prove (qs, xs, l, t, subs, facts, meths, _)) =
   118     Prove (qs, xs, l, t, subs, facts, meths, comment_of l meths)
   119   | comment_isar_step _ step = step
   120 fun comment_isar_proof comment_of = map_isar_steps (comment_isar_step comment_of)
   121 
   122 fun chain_qs_lfs NONE lfs = ([], lfs)
   123   | chain_qs_lfs (SOME l0) lfs =
   124     if member (op =) lfs l0 then ([Then], lfs |> remove (op =) l0) else ([], lfs)
   125 fun chain_isar_step lbl (x as Prove (qs, xs, l, t, subs, (lfs, gfs), meths, comment)) =
   126     let val (qs', lfs) = chain_qs_lfs lbl lfs in
   127       Prove (qs' @ qs, xs, l, t, map chain_isar_proof subs, (lfs, gfs), meths, comment)
   128     end
   129   | chain_isar_step _ step = step
   130 and chain_isar_steps _ [] = []
   131   | chain_isar_steps (prev as SOME _) (i :: is) =
   132     chain_isar_step prev i :: chain_isar_steps (label_of_isar_step i) is
   133   | chain_isar_steps _ (i :: is) = i :: chain_isar_steps (label_of_isar_step i) is
   134 and chain_isar_proof (Proof (fix, assms, steps)) =
   135   Proof (fix, assms, chain_isar_steps (try (List.last #> fst) assms) steps)
   136 
   137 fun kill_useless_labels_in_isar_proof proof =
   138   let
   139     val used_ls =
   140       fold_isar_steps (facts_of_isar_step #> fst #> union (op =)) (steps_of_isar_proof proof) []
   141 
   142     fun kill_label l = if member (op =) used_ls l then l else no_label
   143 
   144     fun kill_step (Prove (qs, xs, l, t, subs, facts, meths, comment)) =
   145         Prove (qs, xs, kill_label l, t, map kill_proof subs, facts, meths, comment)
   146       | kill_step step = step
   147     and kill_proof (Proof (fix, assms, steps)) =
   148       Proof (fix, map (apfst kill_label) assms, map kill_step steps)
   149   in
   150     kill_proof proof
   151   end
   152 
   153 fun relabel_isar_proof_canonically proof =
   154   let
   155     fun next_label l (next, subst) =
   156       let val l' = ("", next) in (l', (next + 1, (l, l') :: subst)) end
   157 
   158     fun relabel_step (Prove (qs, fix, l, t, subs, (lfs, gfs), meths, comment))
   159           (accum as (_, subst)) =
   160         let
   161           val lfs' = maps (the_list o AList.lookup (op =) subst) lfs
   162           val ((subs', l'), accum') = accum
   163             |> fold_map relabel_proof subs
   164             ||>> next_label l
   165         in
   166           (Prove (qs, fix, l', t, subs', (lfs', gfs), meths, comment), accum')
   167         end
   168       | relabel_step step accum = (step, accum)
   169     and relabel_proof (Proof (fix, assms, steps)) =
   170       fold_map (fn (l, t) => next_label l #> apfst (rpair t)) assms
   171       ##>> fold_map relabel_step steps
   172       #>> (fn (assms, steps) => Proof (fix, assms, steps))
   173   in
   174     fst (relabel_proof proof (0, []))
   175   end
   176 
   177 val assume_prefix = "a"
   178 val have_prefix = "f"
   179 
   180 val relabel_isar_proof_nicely =
   181   let
   182     fun next_label depth prefix l (accum as (next, subst)) =
   183       if l = no_label then
   184         (l, accum)
   185       else
   186         let val l' = (replicate_string (depth + 1) prefix, next) in
   187           (l', (next + 1, (l, l') :: subst))
   188         end
   189 
   190     fun relabel_step depth (Prove (qs, xs, l, t, subs, (lfs, gfs), meths, comment))
   191           (accum as (_, subst)) =
   192         let
   193           val lfs' = maps (the_list o AList.lookup (op =) subst) lfs
   194           val (l', accum' as (_, subst')) = next_label depth have_prefix l accum
   195           val subs' = map (relabel_proof subst' (depth + 1)) subs
   196         in
   197           (Prove (qs, xs, l', t, subs', (lfs', gfs), meths, comment), accum')
   198         end
   199       | relabel_step _ step accum = (step, accum)
   200     and relabel_proof subst depth (Proof (fix, assms, steps)) =
   201       (1, subst)
   202       |> fold_map (fn (l, t) => next_label depth assume_prefix l #> apfst (rpair t)) assms
   203       ||>> fold_map (relabel_step depth) steps
   204       |> (fn ((assms, steps), _) => Proof (fix, assms, steps))
   205   in
   206     relabel_proof [] 0
   207   end
   208 
   209 val indent_size = 2
   210 
   211 fun string_of_isar_proof ctxt0 i n proof =
   212   let
   213     (* Make sure only type constraints inserted by the type annotation code are printed. *)
   214     val ctxt = ctxt0
   215       |> Config.put show_markup false
   216       |> Config.put Printer.show_type_emphasis false
   217       |> Config.put show_types false
   218       |> Config.put show_sorts false
   219       |> Config.put show_consts false
   220 
   221     val register_fixes = map Free #> fold Variable.auto_fixes
   222 
   223     fun add_str s' = apfst (suffix s')
   224 
   225     fun of_indent ind = replicate_string (ind * indent_size) " "
   226     fun of_moreover ind = of_indent ind ^ "moreover\n"
   227     fun of_label l = if l = no_label then "" else string_of_label l ^ ": "
   228 
   229     fun of_obtain qs nr =
   230       (if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then "ultimately "
   231        else if nr = 1 orelse member (op =) qs Then then "then "
   232        else "") ^ "obtain"
   233 
   234     fun of_show_have qs = if member (op =) qs Show then "show" else "have"
   235     fun of_thus_hence qs = if member (op =) qs Show then "thus" else "hence"
   236 
   237     fun of_have qs nr =
   238       if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then "ultimately " ^ of_show_have qs
   239       else if nr = 1 orelse member (op =) qs Then then of_thus_hence qs
   240       else of_show_have qs
   241 
   242     fun add_term term (s, ctxt) =
   243       (s ^ (term
   244             |> singleton (Syntax.uncheck_terms ctxt)
   245             |> annotate_types_in_term ctxt
   246             |> with_vanilla_print_mode (Syntax.unparse_term ctxt #> Pretty.string_of)
   247             |> simplify_spaces
   248             |> maybe_quote),
   249        ctxt |> Variable.auto_fixes term)
   250 
   251     fun using_facts [] [] = ""
   252       | using_facts ls ss = enclose "using " " " (space_implode " " (map string_of_label ls @ ss))
   253 
   254     fun is_direct_method (Metis_Method _) = true
   255       | is_direct_method Meson_Method = true
   256       | is_direct_method SMT2_Method = true
   257       | is_direct_method Simp_Method = true
   258       | is_direct_method _ = false
   259 
   260     (* Local facts are always passed via "using", which affects "meson" and "metis". This is
   261        arguably stylistically superior, because it emphasises the structure of the proof. It is also
   262        more robust w.r.t. preplay: Preplay is performed before chaining of local facts with "hence"
   263        and "thus" is introduced. See also "tac_of_method" in "Sledgehammer_Isar_Preplay". *)
   264     fun of_method ls ss meth =
   265       let val direct = is_direct_method meth in
   266         using_facts ls (if direct then [] else ss) ^
   267         "by " ^ string_of_proof_method ctxt (if direct then ss else []) meth
   268       end
   269 
   270     fun of_free (s, T) =
   271       maybe_quote s ^ " :: " ^
   272       maybe_quote (simplify_spaces (with_vanilla_print_mode (Syntax.string_of_typ ctxt) T))
   273 
   274     fun add_frees xs (s, ctxt) =
   275       (s ^ space_implode " and " (map of_free xs), ctxt |> register_fixes xs)
   276 
   277     fun add_fix _ [] = I
   278       | add_fix ind xs = add_str (of_indent ind ^ "fix ") #> add_frees xs #> add_str "\n"
   279 
   280     fun add_assm ind (l, t) =
   281       add_str (of_indent ind ^ "assume " ^ of_label l) #> add_term t #> add_str "\n"
   282 
   283     fun of_subproof ind ctxt proof =
   284       let
   285         val ind = ind + 1
   286         val s = of_proof ind ctxt proof
   287         val prefix = "{ "
   288         val suffix = " }"
   289       in
   290         replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
   291         String.extract (s, ind * indent_size, SOME (size s - ind * indent_size - 1)) ^
   292         suffix ^ "\n"
   293       end
   294     and of_subproofs _ _ _ [] = ""
   295       | of_subproofs ind ctxt qs subs =
   296         (if member (op =) qs Then then of_moreover ind else "") ^
   297         space_implode (of_moreover ind) (map (of_subproof ind ctxt) subs)
   298     and add_step_pre ind qs subs (s, ctxt) =
   299       (s ^ of_subproofs ind ctxt qs subs ^ of_indent ind, ctxt)
   300     and add_step ind (Let (t1, t2)) =
   301         add_str (of_indent ind ^ "let ")
   302         #> add_term t1 #> add_str " = " #> add_term t2 #> add_str "\n"
   303       | add_step ind (Prove (qs, xs, l, t, subs, (ls, ss), meth :: _, comment)) =
   304         add_step_pre ind qs subs
   305         #> (case xs of
   306              [] => add_str (of_have qs (length subs) ^ " ")
   307            | _ => add_str (of_obtain qs (length subs) ^ " ") #> add_frees xs #> add_str " where ")
   308         #> add_str (of_label l)
   309         #> add_term t
   310         #> add_str (" " ^
   311              of_method (sort_distinct label_ord ls) (sort_distinct string_ord ss) meth ^
   312              (if comment = "" then "" else " (* " ^ comment ^ " *)") ^ "\n")
   313     and add_steps ind = fold (add_step ind)
   314     and of_proof ind ctxt (Proof (xs, assms, steps)) =
   315       ("", ctxt)
   316       |> add_fix ind xs
   317       |> fold (add_assm ind) assms
   318       |> add_steps ind steps
   319       |> fst
   320   in
   321     (* One-step Metis proofs are pointless; better use the one-liner directly. *)
   322     (case proof of
   323       Proof ([], [], []) => "" (* degenerate case: the conjecture is "True" with Z3 *)
   324     | Proof ([], [], [Prove (_, [], _, _, [], _, Metis_Method _ :: _, _)]) => ""
   325     | _ =>
   326       (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
   327       of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^
   328       of_indent 0 ^ (if n <> 1 then "next" else "qed"))
   329   end
   330 
   331 end;