Manual termination proof and congruence rules · Beginner Questions

I built a minimal working example of something else I am working on, which isolates a problem that I have:

theory "Test"
imports Main
begin

datatype dat1 = NConst nat | NSum "dat2 list"
and dat2 = PlusOne dat1 | PlusTwo dat1

type_synonym eval1_type = "((nat ⇒ nat) ⇒ dat1 ⇒ nat)"
type_synonym eval2_type = "((nat ⇒ nat) ⇒ dat2 ⇒ nat)"

fun evall :: "((nat ⇒ nat) ⇒ dat2 ⇒ nat) ⇒ (nat ⇒ nat) ⇒ dat2 list ⇒ nat"
  where
  "evall ev v [] = 0"
| "evall ev v (e # Θ) = (ev v e) + (evall ev v Θ)"

lemma eval_list_cong [fundef_cong]:
  "⟦ v1 = v2; Θ1 = Θ2; ⋀e. e ∈ set Θ1 ⟹ ev1 v1 e = ev2 v2 e ⟧
  ⟹ evall ev1 v1 Θ1 = evall ev2 v2 Θ2"
  apply (induction Θ1 arbitrary: Θ2)
  by auto

function eval1 :: eval1_type
and eval2 :: eval2_type
  where
  "eval1 v (NConst i) = v i"
| "eval1 v (NSum Θ) = (evall eval2 v Θ)"

| "eval2 v (PlusOne e) = (eval1 v e) + 1"
| "eval2 v (PlusTwo e) = (eval1 v e) + 2"
  by pat_completeness auto
termination
  apply (relation "measure (λk. (case k of
    Inl(v, e) ⇒ size e |
    Inr(v, e) ⇒ size e))")
  apply auto
sorry

I need to do a manual termination proof because my actual piece of work relies on a more complex lexicographic termination order. And suppose I want to outsource the evall function.
The problem that arises now is that Isabelle does not know that the argument e ∈ Θ can be considered smaller thanΘ (sorry).

I suppose this requires an adjustment of the measure function that somehow enters the list recursion from the recursion over dat1 and dat2. But how would I do that exactly?

Manuel Eberl (Sep 19 2024 at 17:58):

If you simplify that proof obligation you see that all that is missing is the fact that size e ≤ size_list size Θ. This is obviously true, and you can prove it e.g. with an auxiliary lemma. Or just ad-hoc using induction:

termination proof (relation "measure (λ(v, e) ⇒ size e)", goal_cases)
  case (2 v Θ e)
  hence "size e ≤ size_list size Θ"
    by (induction Θ) auto
  thus ?case
    by simp
qed auto

Stream: Beginner Questions

Topic: Manual termination proof and congruence rules

Marvin Brieger (Sep 19 2024 at 12:24):

Manuel Eberl (Sep 19 2024 at 17:58):