How do I tell the termination checker about a theorem?

Stream: lean4

[Alex Zani]

Ok, so I have the following function which makes the termination checker unhappy:

def advanceWhile (state : ParseState) (pred : (Char → Bool)) : ParseState :=
  match isOk: state.acceptNext with
  | ParseResult.ok state' c => if pred c then state'.advanceWhile pred else state
  | _ => state

It's telling me that it cannot prove this:

state : ParseState
pred : Char → Bool
state' : ParseState
c : Char
isOk : state.acceptNext = ParseResult.ok state' c
h✝ : pred c = true
⊢ sizeOf state' < sizeOf state

Now, I actually proved this in a separate theorem.

theorem acceptNext_shrinks_state (state state' : ParseState) :
  state.acceptNext = ParseResult.ok state' v → sizeOf state' < sizeOf state := ...

How do I tell the termination checker to look at that theorem?

[Mario Carneiro]

decreasing_by exact acceptNext_shrinks_state at the end of the definition

[Mario Carneiro]

give or take

[Alex Zani]

When I open decreasing_by, the goal is now:

⊢ (invImage (fun x => PSigma.casesOn x fun state pred => state) instWellFoundedRelationOfSizeOf).1 ⟨state', pred⟩ ⟨state, pred⟩

which is quite different from "sizeOf state' < sizeOf state".
I then have to do a whole bunch of unfolding to get through the multiple layers of typeclasses. Is there a way around that?

[Mario Carneiro]

hm, try adding termination_by state before the decreasing_by

[Alex Zani]

Mario Carneiro said:

hm, try adding termination_by state before the decreasing_by

It get "no extra parameters bounds, please omit the =>"

[Mario Carneiro]

note the edit

[Alex Zani]

Ah yes. I tried that and it didn't change anything.

[Mario Carneiro]

the goal in the decreasing_by should be different

[Mario Carneiro]

you could also try termination_by sizeOf state, which should produce the same goal but maybe with a less obfuscated statement

[Alex Zani]

Mario Carneiro said:

you could also try termination_by sizeOf state, which should produce the same goal but maybe with a less obfuscated statement

I tried it three ways and it unfortunately isn't any simpler. (I do appreciate the help though)

-- No termination_by
-- ⊢ (invImage (fun x => PSigma.casesOn x fun state pred => state) instWellFoundedRelationOfSizeOf).1 ⟨state', pred⟩ ⟨state, pred⟩
-- termination_by state
-- ⊢ (invImage (fun x => PSigma.casesOn x fun state pred => state) instWellFoundedRelationOfSizeOf).1 ⟨state', pred⟩ ⟨state, pred⟩
-- termination_by (sizeOf state)
-- ⊢ (invImage (fun x => PSigma.casesOn x fun state pred => sizeOf state) instWellFoundedRelationOfSizeOf).1 ⟨state', pred⟩ ⟨state, pred⟩

[Mario Carneiro]

i guess it's fine, all three statements are really sizeOf state' < sizeOf state in disguise

[Mario Carneiro]

simp_wf will clean them up

[Alex Zani]

Mario Carneiro said:

simp_wf will clean them up

Forgot to reply earlier, but thanks, yes. simp_wf is a godsend.