Mutual recursion with dependency on an inductve proof

Stream: general

[Naruyoko]

I'm trying to define functions with mutual recursion. The recursion also depends on properties of the previous step. The following code does not work:

mutual def f, g, p
with f : ℕ → ℕ → ℕ
| i 0       := i
| i (j + 1) := i + g i j
with g : ℕ → ℕ → ℕ
| i j := (i + 2) ^ (nat.cases_on j 1 (λ j', (list.range (g i j')).nth_le (f i j') (lt_of_lt_of_eq (p j' i) (list.length_range _).symm)) : ℕ)
with p : ∀ (j : ℕ), (∀ (i : ℕ), f i j < g i j)
| 0       := sorry
| (j + 1) := sorry

The specific definitions and predicate are placeholders.

There seems to be 2 problems here:

1. The definition has "ill-formed match/equations expression"
2. Even if I remove mutual recursion, I get am told that it is an "invalid mutual definition, result types must be in the same universe"

Additionally, as in g, I want to split by cases of j inside a larger expression, so I can reuse the structure. I want this in a later mutually recursed proof which only needs to see that shared structure.
How can I achieve this?

[Reid Barton]

How about defining a function of type ℕ -> ℕ -> { a : ℕ \x ℕ // a.1 < a.2 }?

[Naruyoko]

Thank you, I guess that is an option too, and the individual functions and theorems would be extracted from that definition. I am not sure how I can write it in a way that doesn't go in a mess though as I am going to put many theorems that depend on others. I also don't know a way which allow delaying the case splitting either, or have a friendly name for individual functions in the recursive definition and proofs, though those are cosmetics.

[Naruyoko]

I decided to define a structure to bundle the needed functions and properties and explicitly recurse on j (slightly inconvenient since I'd have to repeat some parts). Interestingly, I get a time-out if I use the case matching notation with let prev := ... in on j, but no problem at all if I write out nat.rec.

[Arthur Adjedj]

Do you have an #mwe for the timeout ?

[Naruyoko]

Arthur Adjedj said:

Do you have an #mwe for the timeout ?

Is this good?

https://gist.github.com/Naruyoko/f377dd2577d7ebb2911fbea13ff172c9

I tried to see the minimum complexity to get the timeout. I think I got it too close though, since it times out on Linux (in VirtualBox) but not on Windows 11 for me.

Lean (version 3.50.3, commit 855e5b74e3a5, Release)

Edit: Now the example does not time out anywhere, so I will have to add complexity back in.

[Kevin Buzzard]

Oh you're using lean 3 still?

[Naruyoko]

Yes. Should I migrate?

Updated the gist so I think it should time out now.

[Kevin Buzzard]

Well maybe migrating will fix the problem!

[Kyle Miller]

My guess without testing anything is that Lean is doing zeta reduction on the let (i.e., substituting the value into the body of the let) while doing some analysis, and this recursively calculated value appears multiple times in the body.

It looks like the entire body of the j+1 case is actually a non-recursive function resultAt x -> resultAt x that takes in the value of recursive_function_pattern_match j. Maybe try lifting that out into its own function?

[Kyle Miller]

By the way, you can write

dite (v.val < x.length)
  (assume h, coe <$> (pnat.has_sub.sub <$> (f i) <*> (f ⟨v.val, h⟩)))
  (assume _, none)

as

if h : v.val < x.length
then coe <$> (pnat.has_sub.sub <$> (f i) <*> (f ⟨v.val, h⟩))
else none

[Naruyoko]

In my case, I found that only a few properties needed to be proved, and the rest could be inferred. Therefore, I ended up defining a builder function (something like resultBuilder : Π (x : list ℕ) (f : fin x.length → option ℕ+) (g : fin x.length → option ℕ) (property1 : _) -> resultAt x) that takes the few input functions and propositions and creates the object I wanted. This reduced the repetition between the 0 and j+1 cases. I think it also had a similar effect as your suggestion to make the recursion a separate function (let works now!).

I didn't know if then else syntax could be dependent. Thank you for the tip.

And thanks to everyone who looked at this.