termination_by and Prod.Lex

Stream: lean4

[Scott Morrison]

I'm failing to work out how to have the correct hypothesis in the following proof so that termination_by works with the lexicographic order.

Can anyone help me with the 2nd call to R r here?

axiom f : Nat → Nat
axiom g : Nat → Nat
axiom s : Nat → Nat
axiom h : (n : Nat) → ¬ (f (s n) < f n) → (f (s n) = f n ∧ g (s n) < g n)

noncomputable def R (n : Nat) : Nat :=
  let r := s n
  if h₀ : f r < f n then
    R r
  else
    have h₁ : f r = f n := (h n h₀).1
    have h₂ : g r < g n := (h n h₀).2
    R r
termination_by R n => (f n, g n)

[Scott Morrison]

Note that the error message

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
case h
n: Nat
r: Nat := s n
h₀: ¬f r < f n
h₁: f r = f n
h₂: g r < g n
⊢ f (s n) < f n

incorrectly appears on the 1st call to R r. I'll track down/create the issue for this in a moment.

[Scott Morrison]

axiom f : Nat → Nat
axiom g : Nat → Nat
axiom s : Nat → Nat
axiom h : (n : Nat) → ¬ (f (s n) < f n) → (f (s n) = f n ∧ g (s n) < g n)

def Prod.Lex.right'' [LT α] [LT β] {a₁ a₂ : α} {b₁ b₂ : β} (ha : a₁ = a₂) (hb : b₁ < b₂) :
    Prod.Lex (· < ·) (· < · ) (a₁, b₁) (a₂, b₂) :=
  ha ▸ Prod.Lex.right a₁ hb

noncomputable def R (n : Nat) : Nat :=
  let r := s n
  if h₀ : f r < f n then
    R r
  else
    have h₁ : f r = f n := (h n h₀).1
    have h₂ : g r < g n := (h n h₀).2
    have := Prod.Lex.right'' h₁ h₂
    R r
termination_by R n => (f n, g n)
decreasing_by
  first | assumption | (constructor; assumption)

works, but makes me sad.

[Scott Morrison]

(both that I needed to define Prod.Lex.right'' and that I needed to write a custom decreasing_by)

[Ioannis Konstantoulas]

Never mind, I was being silly.

[Ioannis Konstantoulas]

The following manual proof worked for me:

noncomputable def R' (n : Nat) : Nat :=
  let r := s n
  R' r
termination_by R' _ => (f n, g n)
decreasing_by
  simp_wf
  have : (f r < f n) ∨ (f r ≥ f n) :=
    Nat.lt_or_ge (f r) (f n)
  cases this with
  | inl h₉ => apply Prod.Lex.left; exact h₉
  | inr h₈ =>
    have h₅ := Nat.not_lt_of_le h₈
    apply Prod.Lex.right'
    have h₁ : f r = f n := (h n h₅).1
    linarith
    have h₂ : g r < g n := (h n h₅).2
    assumption

[Scott Morrison]

It hadn't occurred to me to put all the work in decreasing_by. I think that won't work in my application, but I'll have a think about it, thanks. :-)

[Ioannis Konstantoulas]

In any case, the problem seems to be that the type of Prod.Lex.right is

constructor Prod.Lex.right.{u, v} : ∀ {α : Type u} {β : Type v} {ra : α → α → Prop} {rb : β → β → Prop} (a : α)
  {b₁ b₂ : β}, rb b₁ b₂ → Prod.Lex ra rb (a, b₁) (a, b₂)

whereas we intuitively treat it as

constructor Prod.Lex.right1.{u, v} : ∀ {α : Type u} {β : Type v} {ra : α → α → Prop} {rb : β → β → Prop} (a1 a2  : α)
  {h : a1 = a2} {b₁ b₂ : β}, rb b₁ b₂ → Prod.Lex ra rb (a1, b₁) (a2, b₂)

or similar, and Lean cannot reconcile the two.

[Ioannis Konstantoulas]

A positional marker in R to distinguish the two calls fixes the error position, but then the required goal is decidedly wrong:

noncomputable def R (n : Nat) (t : Bool) : Nat :=
  let r := s n
  if h₀ : f r < f n then
    R r true
  else
    have h₁ : f r = f n := (h n h₀).1
    have h₂ : g r < g n := (h n h₀).2
    R r false
termination_by R n _ => (f n, g n)

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
case h
n: ℕ
t: Bool
r: ℕ := s n
h₀: ¬f r < f n
h₁: f r = f n
h₂: g r < g n
⊢ f (s n) < f n

So there can be no have that can close the goal in that branch, since the goal is False.