Problems with termination of a recursive function using zip, map, and products

Question

I've encountered a problem when trying to define a recursive function which uses map over a zip.

Here is a simplified version of my code, firstly one that works

datatype bar = Bar "bar list"

function (sequential) bar_lub :: "[bar,bar] ⇒ bar" ("_⊔b_" [30,60] 60)
  where
    "(Bar ts) ⊔b (Bar us) = Bar (map (λ(t1,t2). t1 ⊔b t2) (zip ts us))"
  by pat_completeness auto

This is fine, and results in the termination goal of

1. ⋀ts us a b. (a, b) ∈ set (zip ts us) ⟹ P (a, b) ~ P (Bar ts, Bar us)

which is easy to prove given an appropriate P and ~.

My problem comes when I change the list to a list of pairs, as follows

datatype 'a foo = Foo "('a foo × 'a) list"

function (sequential) foo_lub1 :: "['a foo, 'a foo] ⇒ 'a foo" ("_⊔_" [30,60] 60)
  where
    "(Foo ts) ⊔ (Foo us) = Foo (map (λ((t1,_), (t2,_)). (t1 ⊔ t2, undefined)) (zip ts us))"
  by pat_completeness auto

Now, we get the termination goal

1. ⋀ts us t1 b1 t2 b2 xc. ((t1, b1), t2, b2) ∈ set (zip ts us) ⟹ P (t1, xc) ~ P (Foo ts, Foo us)

the variable xc has appeared, and is not related to anything. Ideally, I would expect to have the assumption xc = t2, and the proof would be simple.

Does anyone know why this is happening, and any ways to remedy it?

Answer 1

The function packages uses congruence rules to figure out the context of a recursive call. Unfortunately, congruence rules cannot capture all kinds of contexts, and the deep pattern matching on tuples are such a case where it fails. Fortunately, there is a simple workaround: Use the projections fst and snd instead of the tupled abstraction:

function (sequential) foo_lub1 :: "['a foo, 'a foo] ⇒ 'a foo" ("_⊔_" [30,60] 60)
  where
    "(Foo ts) ⊔ (Foo us) = Foo (map (λx. (fst (fst x) ⊔ fst (snd x), undefined)) (zip ts us))"