termination for mutual recursion

Stream: Carleson

[Edward van de Meent]

i'm having some trouble defining the mutually recursive functions I1,I2, I3 in an ergonomic way...
could someone help me with this? i have a #mwe

section
variable {α : ℤ → Type*} [∀ z, Fintype (α z)] [∀ z, LinearOrder (α z)] (l : ℤ)

mutual
def foo {z:ℤ} (hz : l ≤ z) (a:α z) : ℤ :=
  if hz' : z = l then 1 else
    have hl_lt: l < z := by exact lt_of_le_of_ne hz fun a ↦ hz' (id (Eq.symm a))
    have hl_le_pred: l ≤ z - 1 := by
      linarith
    ∏ (a' : α (z - 1)), bar hl_le_pred a'

def bar_fix_fun {z:ℤ} (hz:l ≤ z) (a :α z) (F : (b:α z) → b < a → ℤ) : ℤ :=
  foo hz a ⊓ ⨅ (b :α z), ⨅ (h:b < a), F b h

def bar {z:ℤ} (hz : l ≤ z) (a:α z) : ℤ:=
  WellFoundedLT.fix (bar_fix_fun hz) a

end

end

it should terminate due to the pair (z,a) being bounded below by (l,inf a) and monotonously decreasing...

[Edward van de Meent]

if it helps any, feel free to assume the following:

variable [∀ z, Encodable (α z)]

lemma order_generated_by_encode : ∀ z, ∀ (a b:α z), a ≤ b ↔ Encodable.encode a ≤ Encodable.encode b := sorry

[Floris van Doorn]

The thing I did with the tile construction lemma (section 4.2) is to use an explicit bijection between my finite type and Fin n, and then just use induction on the natural numbers. See: Construction.Ω₁_aux and Construction.Ω₁

[Floris van Doorn]

But maybe using a custom relation and proving that it's well-founded is even nicer.

[Floris van Doorn]

When working with a general relation, you will need well-foundedness, something like

lemma wf (i : ℤ) : WellFounded (α := α i)  (· < ·) := sorry

I'm not seeing in Mathlib that for every linear order on a finite type < is well-founded...

[Floris van Doorn]

Oh, docs#Finite.to_wellFoundedLT

[Edward van de Meent]

i'm not sure if it matters, but as of yet i haven't needed finiteness... just Countability (which is provable) has done fine...

[Floris van Doorn]

Well, if you want well-foundedness, countability is not enough...

[Edward van de Meent]

it is when you choose the ordering though

[Edward van de Meent]

it is easy to show $Y_k$ is countable, and the proof says you choose the ordering, so the ordering you choose can be well-founded

[Floris van Doorn]

In your minimal example, this works (up to one sorry):

import Mathlib.Tactic
section
variable {α : ℤ → Type*} [∀ z, Fintype (α z)] [∀ z, LinearOrder (α z)] (l : ℤ)
noncomputable section

mutual

def foo {z:ℤ} (hz : l ≤ z) (a:α z) : ℤ :=
  if hz' : z = l then 1 else
    have hl_lt: l < z := by exact lt_of_le_of_ne hz fun a ↦ hz' (id (Eq.symm a))
    have hl_le_pred: l ≤ z - 1 := by
      linarith
    have : (z - 1 - l).toNat * 3 + 2 < (z - l).toNat * 3 := sorry
    ∏ (a' : α (z - 1)), bar hl_le_pred a'
termination_by (z - l).toNat * 3

def bar_fix_fun {z:ℤ} (hz:l ≤ z) (a :α z) (F : (b:α z) → b < a → ℤ) : ℤ :=
  foo hz a ⊓ ⨅ (b :α z), ⨅ (h:b < a), F b h
termination_by (z - l).toNat * 3 + 1

def bar {z:ℤ} (hz : l ≤ z) (a:α z) : ℤ:=
  WellFoundedLT.fix (bar_fix_fun hz) a
termination_by (z - l).toNat * 3 + 2
end

end

[Floris van Doorn]

You have to manually specify a measure for each function, that decreases in each recursive call.

[Edward van de Meent]

curious... so the solution is don't mention the a at all in the measure...

[Floris van Doorn]

It would be different if you defined the functions on Σ z : ℤ, α z and had equipped that type with a specific order.

[Floris van Doorn]

and made more recursive calls that decreased in the second component, but not necessarily in the first component.

[Edward van de Meent]

right... so it might've worked if i didn't use WellFoundedLT.fix to specify the recursion...