termination_by failure in new version of Lean and Mathlib

Stream: new members

[Bbbbbbbbba]

I found that some old code I have written breaks with my current version of Lean and Mathlib:

import Mathlib

lemma dec_lemma {b : ℕ+} {x : ℕ} : 0 < x → Nat.log b x < x ∧ 0 < x / b ^ Nat.log b x ∧ x - b ^ Nat.log b x * (x / b ^ Nat.log b x) < x := by
  sorry -- Proof not important

def nat_to_nat (b : ℕ+) (b1 : ℕ+) (x : ℕ) :=
  if h : 0 < x then
    let e := Nat.log b x;
    let n := x / b ^ e;
    have hdec : e < x ∧ 0 < n ∧ x - b ^ e * n < x := dec_lemma h
    have _ := hdec.right.right
    b1 ^ (nat_to_nat b b1 e) * n + (nat_to_nat b b1 (x - b ^ e * n : ℕ))
  else 0
  termination_by x

The error is:

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
b : ℕ+
x : ℕ
h : 0 < x
e : ℕ := Nat.log (↑b) x
n : ℕ := x / ↑b ^ e
hdec : e < x ∧ 0 < n ∧ x - ↑b ^ e * n < x
x✝ : x - ↑b ^ e * n < x
⊢ 0 < x ∧ ↑b ^ Nat.log (↑b) x ≤ x

The hypothesis x✝ is supposed to be what I need, but now Lean seems to have automatically reduced the goal into something different. Is it possible for me to prevent it from doing so?

[Bbbbbbbbba]

Oh, I got decreasing_by to work. However now I get a warning saying that hdec is unused. What would be a graceful way to silence this warning?

def nat_to_nat (b : ℕ+) (b1 : ℕ+) (x : ℕ) :=
  if h : 0 < x then
    let e := Nat.log b x;
    let n := x / b ^ e;
    have hdec : e < x ∧ 0 < n ∧ x - b ^ e * n < x := dec_lemma h
    b1 ^ (nat_to_nat b b1 e) * n + (nat_to_nat b b1 (x - b ^ e * n : ℕ))
  else 0
  termination_by x
  decreasing_by
    exact hdec.left
    exact hdec.right.right

[Mirek Olšák]

One way to suppress unused variable warning is replacing hdec with _hdec

[Eric Wieser]

That seems undesirable though, since then you have to use _hdec in the decreasing_by

[Eric Wieser]

This looks like a design flaw in the warning here

[Mirek Olšák]

or remove the label, and use that the default name for have is this

[Mirek Olšák]

Both of these are of course workarounds.

[Mirek Olšák]

By the way, do you know what caused the first issue, that looked like a bigger magic to me.

[Robin Arnez]

The issue is simp:

import Mathlib

lemma dec_lemma {b : ℕ+} {x : ℕ} : 0 < x → Nat.log b x < x ∧ 0 < x / b ^ Nat.log b x ∧ x - b ^ Nat.log b x * (x / b ^ Nat.log b x) < x := by
  sorry -- Proof not important

/--
info: Try this:
  [apply] simp only [tsub_lt_self_iff, PNat.pos, pow_pos, mul_pos_iff_of_pos_left, Nat.div_pos_iff, true_and]
---
error: unsolved goals
b : ℕ+
x : ℕ
h : 1 ≤ x
e : ℕ := Nat.log (↑b) x
n : ℕ := x / ↑b ^ e
hdec : e < x ∧ 0 < n ∧ x - ↑b ^ e * n < x
x✝ : x - ↑b ^ e * n < x
⊢ 0 < x ∧ ↑b ^ Nat.log (↑b) x ≤ x
-/
#guard_msgs in
def nat_to_nat (b : ℕ+) (b1 : ℕ+) (x : ℕ) :=
  if h : 1 ≤ x then
    let e := Nat.log b x;
    let n := x / b ^ e;
    have hdec : e < x ∧ 0 < n ∧ x - b ^ e * n < x := dec_lemma h
    have _ := hdec.right.right
    b1 ^ (nat_to_nat b b1 e) * n + (nat_to_nat b b1 (x - b ^ e * n : ℕ))
  else 0
termination_by x
decreasing_by
  · sorry
  · simp?

[Robin Arnez]

I would've expected it to try assumption before simp but apparently not?

[Bbbbbbbbba]

Here is another unintuitive thing I have encountered, though my MWE is unfortunately still quite long. The problem is that the proof breaks if if h1 : 0 < x - b ^ Nat.log b x * (x / b ^ Nat.log b x) then is replaced with if h1 : 0 < x - b ^ e * n then, even though I have defined let e := Nat.log b x; and let n := x / b ^ e;.

import Mathlib

open ONote

def nat_to_ord (b : ℕ+) (x : ℕ) :=
  if h : 0 < x then
    let e := Nat.log b x;
    let n := x / b ^ e;
    oadd (nat_to_ord b e) (⟨n, by sorry⟩ : ℕ+) (nat_to_ord b (x - b ^ e * n : ℕ))
  else 0
  termination_by x
  decreasing_by
    all_goals sorry

lemma nat_to_ord_cmp_lt {b : ℕ+} (hlt: x0 < x1) : (nat_to_ord b x0).cmp (nat_to_ord b x1) = Ordering.lt := by
  sorry

theorem nat_to_ord_nf : (nat_to_ord b x).NF := by
  unfold nat_to_ord
  if h : 0 < x then
    let e := Nat.log b x;
    let n := x / b ^ e;
    simp [h]
    apply NF.oadd
    . exact nat_to_ord_nf
    . have : (nat_to_ord b e).NF := nat_to_ord_nf
      apply nfBelow_iff_topBelow.mpr
      constructor
      . exact nat_to_ord_nf
      . unfold TopBelow
        rw [nat_to_ord]
        if h1 : 0 < x - b ^ Nat.log b x * (x / b ^ Nat.log b x) then
        -- if h1 : 0 < x - b ^ e * n then
          simp [h1]
          apply nat_to_ord_cmp_lt
          apply Nat.log_lt_of_lt_pow
          . exact Ne.symm (Nat.ne_of_lt h1)
          . apply Nat.sub_lt_left_of_lt_add
            . exact Nat.mul_div_le x (b ^ e)
            . rw [← mul_add_one]
              apply Nat.lt_mul_div_succ
              exact Nat.pos_of_neZero (b ^ e)
        else
          simp [h1]
  else
    simp [h]
    exact NF.zero
termination_by x
decreasing_by
  all_goals sorry

[Robin Arnez]

simp per default treats let declarations in the context as opaque, you can use simp +zetaDelta to change that though

[Robin Arnez]

Another approach that works here is

rw [dif_pos h]
extract_lets e n

instead of

let e := Nat.log b x;
let n := x / b ^ e;
simp [h]

because it doesn't unfold the let declarations in the goal

[Bbbbbbbbba]

Thanks, this is much cleaner too as I no longer need to repeat my lets!