383 decreasing_by goals?

Stream: new members

[aron]

I have a fairly complicated recursive function. It calls itself 11 times. However I have designed my function such that there is always a clear decreasing measure.

However despite this Lean completely grinds to a halt while type checking this function. When it does finish it asks me to prove that some of the function's recursive calls do indeed have a decreasing measure. This is fine, but even when I do provide these proofs in hypotheses Lean doesn't register that these prove termination.

E.g. the termination_by clause looks like this: termination_by (deptha, depthb, sizeOf a, sizeOf b)

and on one of the recursive calls the proof state looks like this:

...
hdepths : ¬depthFstA < deptha
hdepthseq : depthFstA = deptha
hsizeslt : sizeOf fstA < sizeOf a
⊢ depthFstA < deptha

I have made these hypotheses specifically to nudge Lean to understanding that the deptha param does not decrease here so it should go for the next one, sizeof a. But Lean doesn't seem to understand this.

I believe that the idiomatic way to prove that this decreases would be in the decreasing_by block, but that leads me to the next problem: that for some reason there are 383(!!) goals there for me to prove. This makes zero sense to me. There are 11 recursive calls, and I provide all required parameters upfront on every call (i.e. I don't leave any ?_s to fill in later by case matching on anything).

Could someone give me some pointers on why there might be such a ludicrous number of goals and how to reduce them?

[aron]

Before anyone asks me for a #mwe, this is taken from a 9000+ line file and I have no idea how to reproduce this exponential number of decreasing_by goals in a smaller example – especially without understanding why this happens in the first place :sweat_smile:

[aron]

(Proof that I'm not making up the insane number of decreasing_by goals)

[Aaron Liu]

try haveing a proof of decreasing before every recursive call, so that the default termination prover may pick it up from the context

[Aaron Liu]

aron said:

(Proof that I'm not making up the insane number of decreasing_by goals)

a screenshot of a piece of the function definition might be more useful, I can't see anything here

[aron]

Aaron Liu said:

try haveing a proof of decreasing before every recursive call, so that the default termination prover may pick it up from the context

Yup that's where the hdepthseq and hsizeslt hypotheses come in. But as you can see it doesn't help:

...
hdepths : ¬depthFstA < deptha
hdepthseq : depthFstA = deptha
hsizeslt : sizeOf fstA < sizeOf a
⊢ depthFstA < deptha

[aron]

Aaron Liu said:

aron said:

(Proof that I'm not making up the insane number of decreasing_by goals)

a screenshot of a piece of the function definition might be more useful, I can't see anything here

The function itself is >500 lines long. Which is why I don't expect to get specific help to fix this issue (unless you're happy to look at the entire thing) but some tips for where to begin debugging

[Aaron Liu]

I think maybe a possible cause of all the goals is that you're proving things about the recursive calls

[aron]

What do you mean?

[Aaron Liu]

aron said:

Aaron Liu said:

try haveing a proof of decreasing before every recursive call, so that the default termination prover may pick it up from the context

Yup that's where the hdepthseq and hsizeslt hypotheses come in. But as you can see it doesn't help:

...
hdepths : ¬depthFstA < deptha
hdepthseq : depthFstA = deptha
hsizeslt : sizeOf fstA < sizeOf a
⊢ depthFstA < deptha

Looking at your screenshot, the goal looks like Prod.Lex ..., maybe have : Prod.Lex ... will help?

[Aaron Liu]

aron said:

What do you mean?

like this

def foobar (k : Nat) : { n : Nat // n = 1 } :=
  match k with
  | 0 => ⟨1, rfl⟩
  | k + 1 =>
    ⟨foobar (k / 2) + foobar (k - 5) - foobar k, by
      rw [foobar _ |>.property, foobar _ |>.property, foobar _ |>.property]⟩
termination_by k
decreasing_by
  -- six goals
  all_goals decreasing_tactic

[Aaron Liu]

maybe that's not a very good example

[aron]

mm but in that example foobar indeed calls itself 6 times. I don't, my function only calls itself 11 times and I still get 383 goals

[Aaron Liu]

I remember this being more complicated

[Aaron Liu]

maybe they fixed it

[Aaron Liu]

aron said:

mm but in that example foobar indeed calls itself 6 times. I don't, my function only calls itself 11 times and I still get 383 goals

once again, it would really be great if you showed a snippet of one spot where the function calls itself

[Aaron Liu]

otherwise I don't really have anything to go off of

[aron]

I can provide a gist of the whole thing if that helps? sorry but I don't really know what else would be helpful. I don't see how a context-less snippet of a recursive call would help

[aron]

The decreasing_by with 383 goals is on this line:
https://gist.github.com/Arrow7000/9ebb0c1302b48930bbf139cd1b70caab#file-typesystem-lean-L10020

[aron]

(it's technically two mutually recursive functions btw but I wanted to keep the explanation simple and since the 2nd function only calls the 1st one once and the 1st one only calls the 2nd one once I figured that's not where the explosion in # of goals comes from)

[aron]

I'm pretty confident that it's correctly implemented and the decreasing measures are correct. If it didn't give me 383 goals to prove termination I am pretty sure I can do it easily

[aron]

also the fact Lean slows to an absolute crawl here makes everything so much more painful :cry:

[aron]

(fyi since you asked about this before, unifyConcs is a function that returns a Decidable-esque proof that either two types in my type system can unify or the proof that they can't)

[Aaron Liu]

I see

[aron]

I just found one clue to the puzzle: I just converted a let to a have and it cut down the number of goals from 383 to 39!

[aron]

I tried this because I saw that the definition of fstUniflooked like this, which made me wonder whether each let binding carries with it a ton of stuff about inner recursive calls?

Screenshot 2025-11-04 at 14.49.56.png

[Aaron Liu]

that's what I was saying

[Aaron Liu]

but my example I came up with was kind of bad

[aron]

I know you're not supposed to use have for data, but I'm hoping that once I switch the implementation away from using tactics, let will just behave like a normal variable binding instead of the let tactic?

[Michael Rothgang]

Do you know about the difference between let and letI? Inside a definition (i.e., building data), you probably want to prefer the latter.

[aron]

oh my god just 11 goals!!
Screenshot 2025-11-04 at 14.54.04.png

[aron]

Michael Rothgang said:

Do you know about the difference between let and letI? Inside a definition (i.e., building data), you probably want to prefer the latter.

No, although I did just look at it just before in case there were different kinds of lets that behaved differently, but its description didn't tell me much:

letI behaves like let, but inlines the value instead of producing a let term.

But I don't know what a let term is? I thought it was just variable binding basically?

[Etienne Marion]

I think this is what a let term is. But letI is different. For instance

letI x := 4
f x

is evaluated to f 4, while

let x := 4
f x

is evaluated to itself.

[aron]

noooooo :sob: we're back to 383 goals even with letIs
Screenshot 2025-11-04 at 15.00.44.png

[Aaron Liu]

it seems like the let is what was creating all those goals

[Aaron Liu]

so if you switch back to letI you will have lots of goals

[aron]

Right, but I thought letI would let me bind data without causing a goal explosion

[aron]

What's the idiomatic thing to do here then? you're not supposed to use have for data but let produces an insane number of goals – for reasons which I still don't fully understand. Will this be different if I use let or letI outside of tactic mode?

[Aaron Liu]

no I think it will be the same

[Aaron Liu]

so here's what I think is happening

[Aaron Liu]

let's say you do

  let k := recursive_call
  -- ...
  foobar k
  -- ...
  barfoo k

so the recursive call is done once here obviously

but when Lean is doing postprocessing to get ready to prove termination, it inlines the let into

  -- ...
  foobar recursive_call
  -- ...
  barfoo recursive_call

so now there's two recursive calls

[Aaron Liu]

so this isn't just limited to two, you can get 383 as well

[aron]

so what's the right thing to do here?

[aron]

(also why is have bad to use for data?)

[Aaron Liu]

so the correct thing to do here is to use have

[Aaron Liu]

and it's not necessarily bad for data

[Etienne Marion]

Aaron Liu said:

but when Lean is doing postprocessing to get ready to prove termination, it inlines the let into

  -- ...
  foobar recursive_call
  -- ...
  barfoo recursive_call

so now there's two recursive calls

Are you sure about that? This looks like a very bad way of dealing with an expression with a let term.

[Aaron Liu]

this is my best guess