termination_by proof with Prod.lex

Stream: lean4

[Floris van Doorn]

In the following code snippet, I want to prove a function to be terminating by giving an explicit measure. I'm quite sure this measure is decreasing, but Lean returns an unprovable goal in one of the cases: it asks me to prove that the measure is decreasing in the first component, but it is decreasing in the second component (and the first component remains the same).
I'm happy to give a manual have-statement, but I don't know how to do that (I tried something in a comment, that doesn't work). I prefer to avoid decreasing_by.

-- some given function
def modifyString : List String → Option String := fun s ↦ some (String.join s)

def myFunction : List String → List String → String
  | [], []     => ""
  | [], x::s   => x ++ myFunction s []
  | pre::l, s' =>
    let s := s' ++ [pre]
    match modifyString s with
    | some post => post ++ myFunction l []
    | none      =>
      -- have : WellFoundedRelation.rel (l.length + s.length, l.length) ((pre::l).length + s'.length, (pre::l).length) := by
      --   sorry
      myFunction l s
      -- goal: cannot prove `⊢ l.length + (s'.length + 1) < l.length + 1 + s'.length`
  termination_by l s => (l.length + s.length, l.length)

Similar thread here (but without satisfactory answer): #lean4 > termination_by and Prod.Lex

[Henrik Böving]

-- some given function
def modifyString : List String → Option String := fun s ↦ some (String.join s)

def myFunction : List String → List String → String
  | [], []     => ""
  | [], x::s   => x ++ myFunction s []
  | pre::l, s' =>
    let s := s' ++ [pre]
    match modifyString s with
    | some post => post ++ myFunction l []
    | none      =>
      -- have : WellFoundedRelation.rel (l.length + s.length, l.length) ((pre::l).length + s'.length, (pre::l).length) := by
      --   sorry
      myFunction l s
      -- goal: cannot prove `⊢ l.length + (s'.length + 1) < l.length + 1 + s'.length`
  termination_by l s => (l.length + s.length, l.length)
  decreasing_by all_goals grind

[Henrik Böving]

I think the unprovable goal could be because of some heuristic that is applied to the goal before being passed on to the have mechanism? Maybe that shouldn't be done if the goal isn't trivially provable right away?

CC @Joachim Breitner

[Joachim Breitner]

Floris van Doorn schrieb:

I prefer to avoid decreasing_by.

Why? I find it much more natural than have statements in the function that then end up in the equational of the function, when really the proofs should be relevant only and thus contained to recursion checking.

[Joachim Breitner]

Especially with “interesting” lexicographic proofs you probably want manual control over whether to use left or right', so this works:

-- some given function
def modifyString : List String → Option String := fun s ↦ some (String.join s)

def myFunction : List String → List String → String
  | [], []     => ""
  | [], x::s   => x ++ myFunction s []
  | pre::l, s' =>
    let s := s' ++ [pre]
    match modifyString s with
    | some post => post ++ myFunction l []
    | none      =>
      -- have : WellFoundedRelation.rel (l.length + s.length, l.length) ((pre::l).length + s'.length, (pre::l).length) := by
      --   sorry
      myFunction l s
      -- goal: cannot prove `⊢ l.length + (s'.length + 1) < l.length + 1 + s'.length`
  termination_by l s => (l.length + s.length, l.length)
  decreasing_by
  · apply Prod.Lex.left
    simp
  · apply Prod.Lex.left
    simp; omega
  · apply Prod.Lex.right'
    · simp; omega
    · simp

[Joachim Breitner]

Or, if you have many goals of similar shape, you can automate that using

  decreasing_by all_goals solve
    | apply Prod.Lex.left <;> (simp <;> omega)
    | apply Prod.Lex.right' <;> (simp <;> omega)
 ```

[Joachim Breitner]

Oh, decreasing_by all_goals grind handles this? So hopefully in a future version of lean this will just work by default.

[Floris van Doorn]

Joachim Breitner said:

Floris van Doorn schrieb:

I prefer to avoid decreasing_by.

Why? I find it much more natural than have statements in the function that then end up in the equational of the function, when really the proofs should be relevant only and thus contained to recursion checking.

Maybe I should start using decreasing_by more. I agree that it is quite nice in this case. It's a bit annoying you'd have to deal with the cases that Lean otherwise does automatically.
I still think that there should always be some have-invocation that should satisfy the termination checker, even when not giving a decreasing_by argument.

[Joachim Breitner]

Floris van Doorn schrieb:

I agree that it is quite nice in this case. It's a bit annoying you'd have to deal with the cases that Lean otherwise does automatically.

You could start with

all_goals try solve | decreasing_tactic

to discharge them

[Joachim Breitner]

Hmm, oddly, if I have the goal as shown after decreasing_by, then assumption works but decreasing_tactic doesn’t:

-- some given function
def modifyString : List String → Option String := fun s ↦ some (String.join s)

def myFunction : List String → List String → String
  | [], []     => ""
  | [], x::s   => x ++ myFunction s []
  | pre::l, s' =>
    let s := s' ++ [pre]
    match modifyString s with
    | some post => post ++ myFunction l []
    | none      =>
      -- have : WellFoundedRelation.rel (l.length + s.length, l.length) ((pre::l).length + s'.length, (pre::l).length) := by
      --   sorry
      have : Prod.Lex (fun x1 x2 => x1 < x2) (fun x1 x2 => x1 < x2) (l.length + (s' ++ [pre]).length, l.length)
               ((pre :: l).length + s'.length, (pre :: l).length) := sorry
      myFunction l s
      -- goal: cannot prove `⊢ l.length + (s'.length + 1) < l.length + 1 + s'.length`
  termination_by l s => (l.length + s.length, l.length)
  decreasing_by
    all_goals try solve | decreasing_tactic
    assumption

Ah, that’s because decreasing_tactic first tries to use lexicographic ordering before trying assumption (https://github.com/leanprover/lean4/blob/ad1a017949674a947f0d6794cbf7130d642c6530/src/Init/WFTactics.lean#L80-L81). That is indeed a bit unfortunate.