[isabelle-dev] Sketch and explore [was: performance problems]

[Florian Haftmann]

Hi all,

since my old »Explorer« draft, although never meant to be something
beyond a proof of concept, seems to be used productively, I spent some
time to polish it up a little, based on rev. c15ee153dec1.

The situation is a little bit uncomfortable, since it is definitely
useful, particularly from a didactic point of view.  But there are still
some oddities and pragmatisms in the code which do not justify a regular
integration into the distribution:

* It does not use any specific logic, but cannot be based on Pure since
it relies on some sledgehammer printing functions (which could be
extracted as separate toolbox, of course).

* Re-printing of proof method text is quite ad-hoc.

* Indentation does not consider any pre-existing indentation.

* Type annotations of printed terms could be more minimal.

In the moment I feel inclined to put the matter into HOL-ex and than
proceed from that.

In the meantime, I am open to feedback.

Cheers,
	Florian

Am 12.09.18 um 08:23 schrieb Florian Haftmann:
>>> On 7 Sep 2018, at 19:18, Makarius <makarius at sketis.net> wrote:
>>>
>>> I can't try it out, since theory "Explorer" is missing.
>>
>> Attached. A very cool thing. 
> 
> Nice to see that old draft from 5 years ago.
> 
> I would still agree that such a tool would be tremendously useful, but
> before going into the distro it would need technical improvement, i.e.
> more civilized approach toward Isar proof text generation, similar to
> Sledgehammer_Isar_Proof.
> 
> Any opinions on that?
> 
> Cheers,
> 	Florian
> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 
-------------- next part --------------
theory Sketch_and_Explore
imports Main \<comment> \<open>TODO: generalize existing sledgehammer functions to Pure\<close>
keywords "sketch" "explore" :: diag
begin

ML \<open>
fun split_clause t =
  let
    val (fixes, horn) = funpow_yield (length (Term.strip_all_vars t)) Logic.dest_all t;
    val assms = Logic.strip_imp_prems horn;
    val concl = Logic.strip_imp_concl horn;
  in (fixes, assms, concl) end;

fun maybe_quote ctxt =
  ATP_Util.maybe_quote (Thy_Header.get_keywords' ctxt);

fun print_typ ctxt T =
  T
  |> Syntax.string_of_typ ctxt
  |> maybe_quote ctxt;

fun print_term ctxt t =
  t
  |> singleton (Syntax.uncheck_terms ctxt)
  |> Sledgehammer_Isar_Annotate.annotate_types_in_term ctxt
      \<comment> \<open>TODO pointless to annotate explicit fixes in term\<close>
  |> Print_Mode.setmp [] (Syntax.unparse_term ctxt #> Pretty.string_of)
  |> Sledgehammer_Util.simplify_spaces
  |> maybe_quote ctxt;

fun print_isar_skeleton ctxt indent keyword (fixes, assms, concl) =
  let
    val (_, ctxt') = Variable.add_fixes (map fst fixes) ctxt;
    val prefix = replicate_string indent " ";
      \<comment> \<open>TODO consider pre-existing indentation -- how?\<close>
    val prefix_sep = "\n" ^ prefix ^ "    and ";
    val show_s = prefix ^ keyword ^ " " ^ print_term ctxt' concl;
    val if_s = if null assms then NONE
      else SOME (prefix ^ "  if " ^ space_implode prefix_sep
        (map (print_term ctxt') assms));
    val for_s = if null fixes then NONE
      else SOME (prefix ^ "  for " ^ space_implode prefix_sep
        (map (fn (v, T) => v ^ " :: " ^ print_typ ctxt T) fixes));
    val s = cat_lines ([show_s] @ map_filter I [if_s, for_s] @
      [prefix ^ "  " ^ (if is_none if_s then "" else "using that ") ^ "sorry"]);
  in
    s
  end;

fun print_sketch ctxt method_text clauses =
  "proof" ^ method_text :: map (print_isar_skeleton ctxt 2 "show") clauses @ ["qed"];

fun print_exploration ctxt method_text [clause] =
    ["proof -", print_isar_skeleton ctxt 2 "have" clause,
      "  then show ?thesis", "    by" ^ method_text, "qed"]
  | print_exploration ctxt method_text (clause :: clauses) =
    "proof -" :: print_isar_skeleton ctxt 2 "have" clause
      :: map (print_isar_skeleton ctxt 2 "moreover have") clauses
      @ ["  ultimately show ?thesis", "    by" ^ method_text, "qed"];

fun coalesce_method_txt [] = ""
  | coalesce_method_txt [s] = s
  | coalesce_method_txt (s1 :: s2 :: ss) =
      if s1 = "(" orelse s1 = "["
        orelse s2 = ")" orelse s2 = "]" orelse s2= ":"
      then s1 ^ coalesce_method_txt (s2 :: ss)
      else s1 ^ " " ^ coalesce_method_txt (s2 :: ss);

fun print_proof_text_from_state print (some_method_ref : ((Method.text * Position.range) * Token.T list) option) state =
  let
    val state' = state
      |> Proof.proof (Option.map fst some_method_ref)
      |> Seq.the_result ""

    val { context = ctxt, facts = _, goal } = Proof.goal state';

    val ctxt_print = fold (fn opt => Config.put opt false)
      [show_markup, Printer.show_type_emphasis, show_types, show_sorts, show_consts] ctxt

    val method_text = case some_method_ref of
        NONE => ""
      | SOME (_, toks) => " " ^ coalesce_method_txt (map Token.unparse toks);
        \<comment> \<open>TODO proper printing required\<close>
    val goal_props = Logic.strip_imp_prems (Thm.prop_of goal);
    val clauses = map split_clause goal_props;
    val lines = if null clauses then
      if is_none some_method_ref then ["  .."]
      else ["  by" ^ method_text]
      else print ctxt_print method_text clauses;
    val message = Active.sendback_markup_properties [] (cat_lines lines);
  in
    (state |> tap (fn _ => Output.information message))
    \<comment> \<open>TODO ideally command would only be \<close>
  end

val sketch = print_proof_text_from_state print_sketch;

fun explore method_ref = print_proof_text_from_state print_exploration (SOME method_ref);

fun sketch_cmd some_method_text =
  Toplevel.keep_proof (K () o sketch some_method_text o Toplevel.proof_of)

fun explore_cmd method_text =
  Toplevel.keep_proof (K () o explore method_text o Toplevel.proof_of)

val _ =
  Outer_Syntax.command \<^command_keyword>\<open>sketch\<close>
    "print sketch of Isar proof text after method application"
    (Scan.option (Scan.trace Method.parse) >> sketch_cmd);

val _ =
  Outer_Syntax.command \<^command_keyword>\<open>explore\<close>
    "explore proof obligations after method application as Isar proof text"
    (Scan.trace Method.parse >> explore_cmd);
\<close>

end
-------------- next part --------------
theory Test_Sketch_and_Explore
  imports Sketch_and_Explore
begin

lemma \<comment> \<open>\<^emph>\<open>sketch\<close> with default proof method\<close>
  "mono ((*) (2 :: nat))"
sketch
  oops

lemma \<comment> \<open>\<^emph>\<open>sketch\<close> with explicit proof method\<close>
  "mono ((*) (2 :: nat))"
sketch (rule monoI)
  oops

lemma \<comment> \<open>\<^emph>\<open>sketch\<close> with default proof method finishing proof\<close>
  "finite (set ''Pointless message.'')"
sketch
  oops

lemma \<comment> \<open>\<^emph>\<open>sketch\<close> with explicit proof method finishing proof\<close>
  "mono Suc"
sketch (rule mono_Suc)
  oops

lemma \<comment> \<open>\<^emph>\<open>sketch\<close> with explicit proof method yielding multiple subgoals\<close>
  "finite (let A = set ''Pointless message.'' in A)"
sketch (rule finite_subset [of _ "set Enum.enum"])
  oops

lemma \<comment> \<open>\<^emph>\<open>explore\<close> finishing proof\<close>
  "\<bar>k\<bar> = \<bar>l\<bar> \<longleftrightarrow> nat \<bar>k\<bar> = nat \<bar>l\<bar>"
explore auto
  oops

lemma \<comment> \<open>\<^emph>\<open>explore\<close> leaving one subgoal\<close>
  "\<bar>k\<bar> div \<bar>l\<bar> = int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)"
explore (auto simp add: abs_if)
  oops

lemma \<comment> \<open>\<^emph>\<open>explore\<close> leaving multiple subgoals\<close>
  "\<bar>k\<bar> div \<bar>l\<bar> = int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)"
explore (auto simp add: abs_if)
  oops

end
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20190321/11d98423/attachment.sig>