Automatic tactic for timing functions · Isabelle/ML

Hi all,
first some context about my project: I'm adding a command to Isabelle which should transform a function into its running time function. So far I have only proved termination by pattern completeness and auto, same approach as fun is doing it. Now I also want to support functions which are not covered by fun. Thanks to @Kevin Kappelmann and @Maximilian Schäffeler I now got a schema which is able to recycle the proof of the original function.
Kevin already sent a demo implementation for the tactic, which works well for some functions, here f. (So far everything restricted to 1 arguement functions) On many other functions it sadly has the weird behavior to work if used with apply (tactic ...) but in the ML code variant on a goal, example: h. Apparently apply/tactic does some magic in the background I'm not able to determine. Does someone know what's going wrong?

declare One_nat_def[simp del]

(*simple function*)
function f :: ‹nat ⇒ bool› where
‹f n = (if n ≤ 1 then True else if 2 dvd n then f (n div 2) else f (3 * n + 1))›
  by auto
termination sorry

function (domintros) f_time :: ‹nat ⇒ nat› where
‹f_time n = 1 + (if n ≤ 1 then 1 else 1 + (if 2 dvd n then 1 + f_time (n div 2) else 1 + f_time (3 * n + 1)))›
  by auto

fun h :: "'a list ⇒ nat" where
  "h [] = 1"
| "h (_#xs) = h xs"
function (domintros) T_h :: "'a list ⇒ nat" where
  "T_h [] = 1"
| "T_h (uu # xs) = 1 + T_h xs"
  by pat_completeness auto

ML‹
(*Note: "<function_name>_time" is just an abbreviation for Wellfounded.accp <function_name>_time*)
val dest_wf_accp = \<^Const_fn>‹Wellfounded.accp _ for f x => ‹(f, x)››

fun time_dom_tac induct_rule domintros =
  let fun focused_tac {context = ctxt,...} subgoal =
    let
      (*TODO: this only works for functions with one argument. You have to extend it
        to make it work with multiple arguments*)
      val (f_time, args) = Logic.strip_imp_concl subgoal |> HOLogic.dest_Trueprop |> dest_wf_accp
      val instantiations = map (fn t => SOME (NONE, (t, false))) [args]
      val arbitrary = []
      val induct_rules = SOME [induct_rule]
      (*TODO: find domintros from context rather than passing it explicitly*)
      val domintros = domintros
    in
      (*TODO: for multiple arguments, you first need to apply cases, rewrite the goal,
        and delete the unnecessary assumption as shown in the more complex examples
        we sent to you*)
      Induction.induction_tac ctxt true [instantiations] [arbitrary] [] induct_rules []
      THEN_ALL_NEW (Metis_Tactic.metis_tac [] ATP_Problem_Generate.combsN ctxt domintros)
    end
  (*first fixes the parameters of the goal, then retrieves the subgoal as a term*)
  in Subgoal.FOCUS_PARAMS (focused_tac #> uncurry #> SUBGOAL #> HEADGOAL) end
›

lemma f_time_dom: ‹f_time_dom n›
  by (tactic ‹time_dom_tac @{thm f.induct} @{thms f_time.domintros} @{context} 1›)

ML‹
  (*setup and prove a goal*)
  val my_goal = Goal.init @{cprop "f_time_dom n"}
    |> time_dom_tac @{thm f.induct} @{thms f_time.domintros} @{context} 1
    |> Seq.pull
    |> Option.map (fst #> Goal.finish @{context})
›

lemma "T_h_dom x"
  apply (tactic ‹time_dom_tac @{thm h.induct} @{thms T_h.domintros} @{context} 1›)
  done

ML‹
  (*setup and prove a goal*)
  val my_goal = Goal.init @{cprop "T_h_dom n"}
    |> time_dom_tac @{thm h.induct} @{thms T_h.domintros} @{context} 1
    |> Seq.pull
    |> Option.map (fst #> Goal.finish @{context})
  (* in the real code I'm using the following instead of the cprop antiquotation
    leading to the same result: *)
val lthy = @{context}
val _ = ("T_h" ^ "_dom n")
      |> Syntax.read_prop lthy
      |> Thm.cterm_of lthy
›

Manuel Eberl (Nov 08 2023 at 14:13):

I can't say I know what's going on there, but Ι for one never used Goal.init etc. by hand. I use Goal.prove, and that works:

  val my_goal =
    Goal.prove @{context} [] [] @{prop "T_h_dom n"}
    (fn {context, ...} => HEADGOAL (time_dom_tac @{thm h.induct} @{thms T_h.domintros} context))

Kevin Kappelmann (Nov 08 2023 at 15:12):

There are type variables in your goal that you need to declare to the context (otherwise metis seems to fail):

Stream: Isabelle/ML

Topic: Automatic tactic for timing functions

Jonas Stahl (Nov 08 2023 at 13:39):

Manuel Eberl (Nov 08 2023 at 14:13):

Kevin Kappelmann (Nov 08 2023 at 15:12):