Theory Termination

section ‹Termination heuristics›
text_raw ‹\label{sec:termination}›

theory Termination
  imports "../Dict_Construction"
begin

text ‹
  As indicated in the introduction, the newly-defined functions must be proven terminating. In
  general, we cannot reuse the original termination proof, as the following example illustrates:
›

fun f :: "nat ⇒ nat" where
"f 0 = 0" |
"f (Suc n) = f n"

lemma [code]: "f x = f x" ..

text ‹
  The invocation of @{theory_text ‹declassify f›} would fail, because @{const f}'s code equations
  are not terminating.

  Hence, in the general case where users have modified the code equations, we need to fall back
  to an (automated) attempt to prove termination.

  In the remainder of this section, we will illustrate the special case where the user has not
  modified the code equations, i.e., the original termination proof should ``morally'' be still
  applicable. For this, we will perform the dictionary construction manually.
›

― ‹Some ML incantations to ensure that the dictionary types are present›
local_setup ‹Class_Graph.ensure_class @{class plus} #> snd›
local_setup ‹Class_Graph.ensure_class @{class zero} #> snd›

fun sum_list :: "'a::{plus,zero} list ⇒ 'a" where
"sum_list [] = 0" |
"sum_list (x # xs) = x + sum_list xs"

text ‹
  The above function carries two distinct class constraints, which are translated into two
  dictionary parameters:
›

function sum_list' where
"sum_list' d_plus d_zero [] = Groups_zero__class_zero__field d_zero" |
"sum_list' d_plus d_zero (x # xs) = Groups_plus__class_plus__field d_plus x (sum_list' d_plus d_zero xs)"
by pat_completeness auto

text ‹
  Now, we need to carry out the termination proof of @{const sum_list'}. The @{theory_text function}
  package analyzes the function definition and discovers one recursive call. In pseudo-notation:

  @{text [display] ‹(d_plus, d_zero, x # xs) ↝ (d_plus, d_zero, xs)›}

  The result of this analysis is captured in the inductive predicate @{const sum_list'_rel}. Its
  introduction rules look as follows:
›

thm sum_list'_rel.intros
― ‹@{thm sum_list'_rel.intros}›

text ‹Compare this to the relation for @{const sum_list}:›

thm sum_list_rel.intros
― ‹@{thm sum_list_rel.intros}›

text ‹
  Except for the additional (unchanging) dictionary arguments, these relations are more or less
  equivalent to each other. There is an important difference, though: @{const sum_list_rel} has
  sort constraints, @{const sum_list'_rel} does not. (This will become important later on.)
›

context
  notes [[show_sorts]]
begin

term sum_list_rel
― ‹@{typ ‹'a::{plus,zero} list ⇒ 'a::{plus,zero} list ⇒ bool›}›

term sum_list'_rel
― ‹@{typ ‹'a::type Groups_plus__dict × 'a::type Groups_zero__dict × 'a::type list ⇒ 'a::type Groups_plus__dict × 'a::type Groups_zero__dict × 'a::type list ⇒ bool›}›

end

text ‹
  Let us know discuss the rough concept of the termination proof for @{const sum_list'}. The goal is
  to show that @{const sum_list'_rel} is well-founded. Usually, this is proved by specifying a
  ∗‹measure function› that
  ▸ maps the arguments to natural numbers
  ▸ decreases for each recursive call.
›
text ‹
  Here, however, we want to instead show that each recursive call in @{const sum_list'} has a
  corresponding recursive call in @{const sum_list}. In other words, we want to show that the
  existing proof of well-foundedness of @{const sum_list_rel} can be lifted to a proof of
  well-foundedness of @{const sum_list'_rel}. This is what the theorem
  @{thm [source=true] wfP_simulate_simple} states:

  @{thm [display=true] wfP_simulate_simple}

  Given any well-founded relation ‹r› and a function ‹g› that maps function arguments from ‹r'› to
  ‹r›, we can deduce that ‹r'› is also well-founded.

  For our example, we need to provide a function ‹g› of type
  @{typ ‹'b Groups_plus__dict × 'b Groups_zero__dict × 'b list ⇒ 'a list›}.
  Because the dictionary parameters are not changing, they can safely be dropped by ‹g›.
  However, because of the sort constraint in @{const sum_list_rel}, the term @{term "snd ∘ snd"}
  is not a well-typed instantiation for ‹g›.

  Instead (this is where the heuristic comes in), we assume that the original function
  @{const sum_list} is parametric, i.e., termination does not depend on the elements of the list
  passed to it, but only on the structure of the list. Additionally, we assume that all involved
  type classes have at least one instantiation.

  With this in mind, we can use @{term "map (λ_. undefined) ∘ snd ∘ snd"} as ‹g›:
›

thm wfP_simulate_simple[where
  r = sum_list_rel and
  r' = sum_list'_rel and
  g = "map (λ_. undefined) ∘ snd ∘ snd"]

text ‹
  Finally, we can prove the termination of @{const sum_list'}.
›

termination sum_list'
proof -
  have "wfP sum_list'_rel"
  proof (rule wfP_simulate_simple)
    ― ‹We first need to obtain the well-foundedness theorem for @{const sum_list_rel} from the ML
        guts of the @{theory_text function} package.›
    show "wfP sum_list_rel"
      apply (rule accp_wfPI)
      apply (tactic ‹resolve_tac @{context} [Function.get_info @{context} @{term sum_list} |> #totality |> the] 1›)
      done

    define g :: "'b Groups_plus__dict × 'b Groups_zero__dict × 'b list ⇒ 'c::{plus,zero} list" where
      "g = map (λ_. undefined) ∘ snd ∘ snd"

    ― ‹Prove the simulation of @{const sum_list'_rel} by @{const sum_list_rel} by rule induction.›
    show "sum_list_rel (g x) (g y)" if "sum_list'_rel x y" for x y
      using that
      proof (induction x y rule: sum_list'_rel.induct)
        case (1 d_plus d_zero x xs)
        show ?case
          ― ‹Unfold the constituent parts of @{term g}:›
          apply (simp only: g_def comp_apply snd_conv list.map)
          ― ‹Use the corresponding introduction rule of @{const sum_list_rel} and hope for the best:›
          apply (rule sum_list_rel.intros(1))
          done
      qed
  qed

  ― ‹This is the goal that the @{theory_text function} package expects.›
  then show "∀x. sum_list'_dom x"
    by (rule wfP_implies_dom)
qed

text ‹This can be automated with a special tactic:›

experiment
begin

termination sum_list'
  apply (tactic ‹
    Transfer_Termination.termination_tac
      (Function.get_info @{context} @{term sum_list'})
      (Function.get_info @{context} @{term sum_list})
      @{context}
      1›; fail)
  done

end

text ‹
  A similar technique can be used for making functions defined in locales executable when, for some
  reason, the definition of a ``defs'' locale is not feasible.
›

locale foo =
  fixes A :: "nat"
  assumes "A > 0"
begin

fun f where
"f 0 = A" |
"f (Suc n) = Suc (f n)"

― ‹We carry out this proof in the locale for simplicity; a real implementation would probably
    have to set up a local theory properly.›
lemma f_total: "wfP f_rel"
apply (rule accp_wfPI)
apply (tactic ‹resolve_tac @{context} [Function.get_info @{context} @{term f} |> #totality |> the] 1›)
done

end

― ‹The dummy interpretation serves the same purpose as the assumption that class constraints have
    at least one instantiation.›
interpretation dummy: foo 1 by standard simp

function f' where
"f' A 0 = A" |
"f' A (Suc n) = Suc (f' A n)"
by pat_completeness auto

termination f'
  apply (rule wfP_implies_dom)
  apply (rule wfP_simulate_simple[where g = "snd"])
   apply (rule dummy.f_total)
  subgoal for x y
    apply (induction x y rule: f'_rel.induct)
    subgoal
     apply (simp only: snd_conv)
     apply (rule dummy.f_rel.intros)
     done
    done
  done

text ‹Automatic:›

experiment
begin

termination f'
  apply (tactic ‹
    Transfer_Termination.termination_tac
      (Function.get_info @{context} @{term f'})
      (Function.get_info @{context} @{term dummy.f})
      @{context}
      1›; fail)
  done

end

end