Show termination using Lex (ℕ × ℕ)

Stream: mathlib4

[Markus Schmaus]

I'm trying to use Lex (ℕ × ℕ) for showing termination. But it doesn't work the way I thought it would. Is there a way to make it work?

import Mathlib

def aggr (ns : List ℕ) : ℕ :=
  let rec go (n : ℕ) (ns : List ℕ) :=
    if nil : ns = List.nil then n
    else
      have : List.length (List.tail ns) < List.length ns := by
        have := List.length_pos_of_ne_nil nil |> ne_zero_of_lt
        simp_all only [ne_eq, List.length_tail, ← Nat.pred_eq_sub_one, not_false_eq_true,
          Nat.pred_lt]
      go n.succ ns.tail -- works
  termination_by (List.length ns)

  go 0 ns

abbrev finiteBy (ns : List ℕ) : Lex (ℕ × ℕ) :=
  toLex (ns.length, ns.headD 0)

def aggr' (ns : List ℕ) : ℕ :=
  let rec go (n : ℕ) (ns : List ℕ) :=
    if nil : ns = List.nil then n
    else
      have : finiteBy (List.tail ns) < finiteBy ns := by
        have := List.length_pos_of_ne_nil nil |> ne_zero_of_lt
        simp only [finiteBy, List.length_tail, List.headD_eq_head?, Prod.Lex.lt_iff]
        apply Or.inl
        simp_all only [ne_eq, List.length_tail, ← Nat.pred_eq_sub_one, not_false_eq_true,
          Nat.pred_lt]
      go n.succ ns.tail -- failed to prove termination, suggests proving `False`
  termination_by finiteBy ns

  go 0 ns

Of course in this mwe it doesn't really make sense to use finiteBy instead of length, but in my real use case I need lexicographical ordering.

[Joachim Breitner]

I don't think you need to use Lex explicitly, just use termination_by (ns.lengh, ns.headD 0) maybe?

[Markus Schmaus]

termination_by (ns.lengh, ns.headD 0) doesn't seem to use lexicographical ordering, here is a mwe that shows this:

import Mathlib

def aggr'' (ns : List ℕ) : ℕ :=
  let rec go (n : ℕ) (ns : List ℕ) :=
    if nil : ns = List.nil then n
    else if head_zero : ns.headD 0 = 0 then
      have : List.length (List.tail ns) < List.length ns := by
        have := List.length_pos_of_ne_nil nil |> ne_zero_of_lt
        simp_all only [ne_eq, List.length_tail, ← Nat.pred_eq_sub_one, not_false_eq_true,
          Nat.pred_lt]
      go n.succ ns.tail -- This works
    else
      let ns' := (ns.headD 0).pred :: ns.tail
      have : ns'.length = ns.length := by
        unfold_let ns'
        have := List.length_pos_of_ne_nil nil |> ne_zero_of_lt |> Nat.succ_pred
        simp_all only [List.headD_eq_head?, List.length_cons, List.length_tail, ←
          Nat.pred_eq_sub_one]
      have : ns'.headD 0 < ns.headD 0 := by
        unfold_let ns'
        simp only [List.headD_cons]
        simp_all only [List.headD_eq_head?]
      go n.succ ns' -- termination fails here
  termination_by (ns.length, ns.headD 0)

  go 0 ns

[Joachim Breitner]

Hmm, it is using the lexicographic ordering, but the the problem is that the default decreasing_tactic is not complete:

It uses docs#Prod.Lex.right, but in your case you need the more general docs#Prod.Lex.right'. You can make progress with

decreasing_by
    · simp_wf; omega
    · simp_wf
      apply Prod.Lex.right'
      · sorry
      · sorry

e.g.

def aggr'' (ns : List ℕ) : ℕ :=
  let rec go (n : ℕ) (ns : List ℕ) :=
    if nil : ns = List.nil then n
    else if head_zero : ns.headD 0 = 0 then
      have : List.length (List.tail ns) < List.length ns := by
        have := List.length_pos_of_ne_nil nil |> ne_zero_of_lt
        simp_all only [ne_eq, List.length_tail, ← Nat.pred_eq_sub_one, not_false_eq_true,
          Nat.pred_lt]
      go n.succ ns.tail -- This works
    else
      let ns' := (ns.headD 0).pred :: ns.tail
      go n.succ ns' -- termination fails here
  termination_by (ns.length, ns.headD 0)
  decreasing_by
    · simp_wf; omega
    · simp_wf
      apply Prod.Lex.right'
      · apply Nat.le_of_eq
        exact RelSeries.fromListChain'.proof_1 ns nil
      · apply Nat.pred_lt
        simpa using head_zero
  go 0 ns

(the odd lemma is picked up by appy? – :shrug: )