Termination with implicit else branch

Stream: lean4

[Leni Aniva]

This does not compile:

def go (n: Nat) (i: Nat) (a: Nat): IO Nat := do
  if i ≥ n then
    return a
  go n (i + 1) (a + i)
  termination_by n - i

which shows

failed to prove termination, possible solutions:
  - Use `have`-expressions to prove the remaining goals
  - Use `termination_by` to specify a different well-founded relation
  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
n i a : Nat
⊢ n - (i + 1) < n - i

but this does

def go (n: Nat) (i: Nat) (a: Nat): IO Nat := do
  if i ≥ n then
    return a
  else
    go n (i + 1) (a + i)
  termination_by n - i

What causes this behaviour? The two expressions are identical

[Henrik Böving]

It's most likely due to the way that the if gets lowered by do notation. The code gets compiled to a join point which does not have access to the fact that ¬i ≥ n which causes the automated proof to fail.

@Joachim Breitner is this something easy to support by changing the do elaborator?

[Mario Carneiro]

I would like to know more about how termination_by acquires the assumption i >= n in the second case. This seems kind of magical since it's not a dite application, it must be using some congr lemma or something to descend into it and pick up the relevant fact

[Mario Carneiro]

whatever it is, I want to extend it to work on List.map so I can write my nested inductive recusions

[Joachim Breitner]

The well-founded definition processing replaces all ites with dites, relatively early in the pipeline
https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/PreDefinition/WF/Ite.lean
(since 2022)

[Joachim Breitner]

Unfortunately, it’s not using congr lemmas like Isabelle does, that would be neat, but it seems that our logic doesn’t quite allow that (although I’m happy to be proven wrong)

[Joachim Breitner]

Hmm, since we are in non-constructive mode anyways with well-founded recursion, I wonder if we can prove termination using congr lemmas the way Isabelle does. It would probably need a fixed point that instead of

fix : {α : Sort u} {C : α → Sort v} {r : α → α → Prop} (h : WellFounded r)  (F : (x : α) → (ih : (y : α) → r y x → C y) → C x)  (x : α) : C x

says something like

fix' : {α : Sort u} {C : α → Sort v}  (F : (x : α)  (ih : (y : α) → C y) → C x)  (x : α) : C x

(unconstrained ih!) and a separate theorem

fix_eq : {α : Sort u} {C : α → Sort v} {r : α → α → Prop} (h : WellFounded r)  (F : (x : α) → (ih : (y : α) → C y) → C x)
  (termination : ∀ (x : α) (ih1 ih2 : (y : α) → C y) → (eq_on_smaller : (y : α) → r y x → ih1 y = ih2 y)  → F ih1 x = F ih2 x)
  : fix' F = F (fix' F)

where the termination side condition essentially says “even though F is defined on all α, only smaller ones affect the outcome” as an extrinsic variant of “F is defined only on smaller α”.

Is something like this plausible? Desirable? Maybe only if C x is a-priori non-empty?

[Mario Carneiro]

Joachim Breitner said:

The well-founded definition processing replaces all ites with dites, relatively early in the pipeline
https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/PreDefinition/WF/Ite.lean
(since 2022)

Doesn't it need to prove equivalence somehow? This seems like it's only transforming the term itself

[Mario Carneiro]

Joachim Breitner said:

Unfortunately, it’s not using congr lemmas like Isabelle does, that would be neat, but it seems that our logic doesn’t quite allow that (although I’m happy to be proven wrong)

I'm not sure I understand the concern. The way I would propose to implement this is to do something similar to the ite -> dite transformation and replace uses of List.map with List.pmap (ideally in some extensible way so that we can also do something similar for List.foldl, Array.forM, etc), and then do the termination proof in that extended context

[Joachim Breitner]

I was just rambling about how to do termination proofs without rewriting the terms (using compositional congr lemmas after the fact). If we want to stick to rewriting, then yes, that is the way to go.

Does this compose well? What if the code has xs |>.map f |>. filter g |>. foldl h, and the recursive call is in h? It seems nontrivial to me to thread the x \in xs information through such a pipeline in an automatic and general way.

And then we still have to prove that to be equal to the original code when proving the unfolding lemma. And the user might be confused when they see code they didn't write in the context of their termination proofs.

Sounds worth a master thesis and a paper to me :-). Or do we know of systems that do this already?