Proving equivalence of two versions of a function

Stream: Program verification

[Zack Weinberg]

I have been beating my head against this proof for two weeks now and so I am going to stop asking questions about tiny pieces of it and just drop the whole thing on you and beg for help.

import Mathlib
import Mathlib.Tactic

-- Conversion factor from seconds to nanoseconds (10⁹)
abbrev ONE_S_IN_NS : Nat := 1000000000

-- The nanoseconds field of a `struct timespec` is guaranteed to be
-- in the range 0 ≤ tv_nsec < ONE_S_IN_NS.
abbrev Nsec : Type := Fin ONE_S_IN_NS

-- Lean analogue of `struct timespec`.  A Timespec represents an
-- interval of time since some unspecified epoch instant.  We seek to
-- prove an equivalence between two methods of computing whether the
-- *difference* between two Timespec quantities is greater than some
-- interval, so we don't care what the epoch actually is.
--
-- In C, the seconds field is a `time_t`, which is normally either a
-- 32- or 64-bit signed machine integer.  For our purposes—measuring
-- time intervals typically no more than a few tens of seconds—we can
-- ignore the possibility of machine integer overflow and model the
-- seconds field using Int, i.e. a mathematical integer with unbounded
-- range.
structure Timespec where
  sec  : Int
  nsec : Nsec
deriving Repr

-- This function defines the conversion from a Timespec quantity to
-- the total number of nanoseconds that have elapsed since that
-- Timespec's (unspecified) epoch.
def timespec_to_ns (tv: Timespec) : Int :=
  tv.sec * ONE_S_IN_NS + tv.nsec

-- Version one of the calculation we're interested in.
def timespec_difference_at_least_mul
  (after : Timespec) (before: Timespec) (min_ns: Nsec) : Bool :=
  let delta := (timespec_to_ns after) - (timespec_to_ns before);
  delta < 0 || delta ≥ min_ns

-- Version two of the calculation we're interested in.
def timespec_difference_at_least_cases
  (after : Timespec) (before: Timespec) (min_ns: Nsec) : Bool :=
  if after.sec = before.sec then
    after.nsec ≥ before.nsec + min_ns || after.nsec < before.nsec
  else if after.sec = before.sec + 1 then
    let delta_ns := Int.ofNat (ONE_S_IN_NS + after.nsec) - before.nsec;
    -- There is no `|| delta_ns < 0` on this expression because in this
    -- case delta_ns cannot be negative.
    delta_ns ≥ min_ns
  else true

-- The statement to be proved:
theorem timespec_differences_equivalent :
  timespec_difference_at_least_mul = timespec_difference_at_least_cases
  := by
  funext a b m
  rw [Bool.eq_iff_iff]
  simp [timespec_difference_at_least_mul,
        timespec_difference_at_least_cases,
        timespec_to_ns]
  sorry

I believe that timespec_difference_at_least_mul and timespec_difference_at_least_cases are indeed equivalent. If a counterexample exists, it indicates a bug in timespec_difference_at_least_cases; my larger goal is to have a version of `timespec_difference_at_least_cases (in a conventional programming language) that has no such bugs.

As you may guess from some of my other posts, I have been able to prove subcases of the equivalence but not in a way that lets me integrate them into a complete proof. For example, this lemma is valid:

lemma equivalence_when_equal_seconds (an bn m: Int) :
  an < bn ∨ m ≤ an - bn ↔ an < bn ∨ bn + m ≤ an
  := by
  apply Iff.or
  case h₁ /- an < bn ↔ an < bn -/ =>
    tauto
  case h₂ /- m ≤ an - bn ↔ bn + m ≤ an -/ =>
    apply Iff.intro
    case mp => exact Int.add_le_of_le_sub_left
    case mpr => exact Int.le_sub_left_of_add_le

and its statement is approximately what the equivalence above reduces to when after.sec = before.sec, but it doesn't unify because (I think) there are a bunch of type conversions in the way. And that's where I keep getting stuck. rewrite and simp sometimes see through type conversions and sometimes don't and I am starting to believe that I have begun in the wrong place somehow.

Note that the use of Fin expresses something important about the original problem domain that I am reluctant to give up. For instance, the logic of the after.sec = before.sec + 1 case is valid only because Timespec.nsec is always less than ONE_S_IN_NS. However, possibly there is a more fluent way to specify that than with Fin.

[Eric Wieser]

You might find it easier here to first write an "ideal" implementation of Sub TimeSpec and LE TimeSpec, and write some characterization lemmas about those operations first

[Eric Wieser]

Then you can prove that both implementations match the ideal one, and that they therefore match each other by transitivity

[Zack Weinberg]

That's kinda what timespec_difference_at_least_mul already is, though? Maybe I don't understand what you have in mind

[Aaron Liu]

I managed to reduce it to two statements I don't find very obviously true

theorem timespec_differences_equivalent :
  timespec_difference_at_least_mul = timespec_difference_at_least_cases
  := by
  funext a b m
  rw [Bool.eq_iff_iff]
  simp [timespec_difference_at_least_mul,
        timespec_difference_at_least_cases,
        timespec_to_ns]
  rw [equivalence_when_equal_seconds]
  split_ifs with h
  · rw [h]
    simp only [add_lt_add_iff_left, Nat.cast_lt, Fin.val_fin_lt]
    rw [or_comm]
    apply or_congr_left'
    intro hnsec
    rw [add_assoc, add_le_add_iff_left]
    norm_cast
    rw [Fin.le_iff_val_le_val, Fin.val_add]
    -- this isn't obvious to me
    sorry
  · -- this isn't obvious to me
    sorry

[Niels Voss]

Just looking at it briefly, but I'm a bit concerned about this: after.nsec ≥ before.nsec + min_ns

Remember that Fin addition wraps by default, so if min_ns is like 800000000 and after.nsec is 600000000 and before.nsec is 500000000 then this will be true even if you might like it to be false

[Zack Weinberg]

I swear I read documentation that said that Fin addition would enlarge the bound as necessary. Maybe that was Lean 3? Anyway, wrapping addition is very much not what I wanted.

[Niels Voss]

Maybe you could consider not using Fin addition and instead using Nat addition? You already said you wanted to keep Fin in the structure, but you can define another function Timespec.nsecNat or something without having to change the structure

[Zack Weinberg]

Yeah. I've managed to get a lot further with this by minimizing my use of Fin. Instead I use Nat for nanosecond quantities and carry around the bounds as separate hypotheses. This makes a lot more of the standard toolbox usable and gets rid of all the double conversions. I also discovered a useful trick for complicated algebraic manipulation:

    ...
    have rearrangement (variables...) : [mess] = [simplified]
        := by linarith
    simp [rearrangement]
    ...

works for anything linarith can prove! This should be mentioned in beginner documentation somewhere ;-)

Now I'm stuck on something different: the last (hopefully) two steps of the proof boil down to being able to prove a < N → a < (complex expression) where the complex expression is, to the human eye, obviously greater than or equal to N, but I don't know how to express that in Lean except for the very simplest cases (where something like Nat.lt_add_rightis exactly applicable). Here's the whole thing again with a lot of comments and sorry placeholders for the remaining steps.

import Mathlib
import Mathlib.Tactic

-- Conversion factor from seconds to nanoseconds (10⁹)
abbrev ONE_S_IN_NS : Nat := 1000000000

-- Lean analogue of `struct timespec`.  A Timespec represents an
-- interval of time since some unspecified epoch instant.  We seek to
-- prove an equivalence between two methods of computing whether the
-- *difference* between two Timespec quantities is greater than some
-- interval, so we don't care what the epoch actually is.
--
-- In C, the seconds field is a `time_t`, which is normally either a
-- 32- or 64-bit signed machine integer.  For our purposes—measuring
-- time intervals typically no more than a few tens of seconds—we can
-- ignore the possibility of machine integer overflow and model the
-- seconds field using Int, i.e. a mathematical integer with unbounded
-- range.
--
-- In C, the nanoseconds field is a `long` (yes, signed, for no good
-- reason) and is constrained to the range [0, ONE_S_IN_NS) by
-- convention alone.  Fin has properties we don't want
-- (e.g. arithmetic on Fin is defined to be modulo its limit) and is
-- also just awkward to work with.  Instead, our version of Timespec
-- uses Nat for the nanoseconds field and, rather like Fin, bundles a
-- proof that it's in the appropriate range.
structure Timespec where
  sec        : Int
  nsec       : Nat
  nsec_bound : (nsec < ONE_S_IN_NS)
deriving Repr

-- This function defines the conversion from a Timespec quantity to
-- the total number of nanoseconds that have elapsed since that
-- Timespec's (unspecified) epoch.
def timespec_to_ns (tv: Timespec) : Int :=
  tv.sec * ONE_S_IN_NS + tv.nsec

-- This is the simple version of
-- timespec_difference_at_least.
--
-- The calculation it performs is valid for any `min_ns: Nat`, but we limit
-- it to `min_ns: Fin ONE_S_IN_NS` so that an `=` equivalence between this
-- function and timespec_difference_at_least_cases, below, is type correct.
def timespec_difference_at_least_mul
  (after : Timespec) (before: Timespec) (min_ns: Fin ONE_S_IN_NS) : Bool :=
  let delta := (timespec_to_ns after) - (timespec_to_ns before);
  delta < 0 ∨ delta ≥ min_ns.val

-- This is the cleverer version of timespec_difference_at_least that avoids
-- needing to do any multiplication.
--
-- Unlike timespec_difference_at_least_mul, it *does* rely on `min_ns`
-- being in the specified finite range.
def timespec_difference_at_least_cases
  (after : Timespec) (before: Timespec) (min_ns: Fin ONE_S_IN_NS) : Bool :=
  if after.sec = before.sec then
    after.nsec < before.nsec ∨ after.nsec ≥ before.nsec + min_ns.val
  else if after.sec = before.sec + 1 then
    (ONE_S_IN_NS + after.nsec) - before.nsec ≥ min_ns.val
  else
    -- Either after.sec < before.sec, or after.sec > before_sec + 1.
    -- In the former case, (timespec_to_ns after) < (timespec_to_ns before)
    -- no matter what the nsec values are.  In the latter case,
    -- (timespec_to_ns after) - (timespec_to_ns before) must be at
    -- least one whole second and therefore greater than any possible
    -- value of min_ns.
    true

-- There are four cases to consider for the proof, depending on the
-- relationship between after.sec and before.nsec:
--   after.sec < before.sec
--   after.sec = before.sec
--   after.sec = before.sec + 1
--   after.sec > before.sec + 1
-- These are exhaustive, by trichotomy of the ordering relation on ℕ.
--
-- We prove each case individually.

-- The after.sec = before.sec case, which is the easiest.
-- We don't need any of the bounds on an, bn, or m.
lemma case_as_eq_bs (an bn m: ℕ)
  : an < bn ∨ (m:ℤ) ≤ (an:ℤ) - (bn:ℤ) ↔ an < bn ∨ bn + m ≤ an
  := by
  apply or_congr_right'
  intro h
  zify
  exact le_sub_iff_add_le'

-- Simplification lemma used by the remaining cases:
lemma x_ne_x_plus_stuff (x: ℤ) (y: ℕ)
  : ¬(x = x + 1 + (y:ℤ) + 1)
  := by linarith

-- The after.sec < before.sec case, which is the second easiest since
-- both functions always return true.
lemma case_as_lt_bs
  (as : ℤ)
  (δs an bn m : ℕ)
  (an_bound : an < ONE_S_IN_NS)
  : as * 1000000000 + ↑an < (as + 1 + ↑δs) * 1000000000 + ↑bn
    ∨ ↑m ≤ as * 1000000000 + ↑an - ((as + 1 + ↑δs) * 1000000000 + ↑bn)
    ↔ ¬as = as + 1 + ↑δs + 1 ∨ m ≤ 1000000000 + an - bn
  := by
    -- the right-hand side of the equivalence is always true
    simp [x_ne_x_plus_stuff]
    -- now we have the disjunction
    -- ⊢ as * 1000000000 + ↑an < (as + 1 + ↑δs) * 1000000000 + ↑bn
    --   ∨ ↑m ≤ as * 1000000000 + ↑an - ((as + 1 + ↑δs) * 1000000000 + ↑bn)
    -- the left side of which is always true
    left
    -- cancel duplicate terms on both sides of the remaining inequality
    rewrite [add_mul, add_mul, add_assoc, add_assoc, Int.add_lt_add_iff_left]
    norm_cast
    -- now we have an < 1*1000000000 + (δs * 1000000000 + bn),
    -- with all variables Nat,
    -- and we know an < 1000000000
    revert an_bound
    simp [ONE_S_IN_NS]
    exact Nat.lt_add_right (δs * 1000000000 + bn)

-- The after.sec > before.sec + 1 case, which is very similar to the
-- after.sec < before.sec case.
lemma case_as_gt_bs_plus_one
  (bs : ℤ)
  (an bn m q : ℕ)
  (m_bound : m < ONE_S_IN_NS)
  (an_bound : an < ONE_S_IN_NS)
  (bn_bound : bn < ONE_S_IN_NS)
  : (bs + 1 + ↑(q + 1)) * 1000000000 + ↑an < bs * 1000000000 + ↑bn
    ∨ ↑m ≤ (bs + 1 + ↑(q + 1)) * 1000000000 + ↑an - (bs * 1000000000 + ↑bn)
    ↔ ¬q + 1 = 0 ∨ m ≤ 1000000000 + an - bn
  := by
    -- the right-hand side of the equivalence is always true
    simp [Nat.add_one_ne_zero]
    -- now we have the disjunction
    -- ⊢ (bs + 1 + (↑q + 1)) * 1000000000 + ↑an < bs * 1000000000 + ↑bn
    --   ∨ ↑m ≤ (bs + 1 + (↑q + 1)) * 1000000000 + ↑an
    --           - (bs * 1000000000 + ↑bn)
    -- the right side of which is always true, but proving it requires
    -- all three bounds and a bunch of algebraic rearrangement
    right
    have rearrangement (x: ℤ) (i j k: ℕ)
      : ((((x + 1) + (↑k + 1)) * 1000000000) + ↑i)
         - ((x * 1000000000) + ↑j)
      = 2 * 1000000000 + k * 1000000000 + i - j
      := by linarith
    simp [rearrangement]
    -- ⊢ ↑m ≤ 2000000000 + ↑q * 1000000000 + ↑an - ↑bn
    -- an < 1000000000 and bn < 1000000000
    -- so the smallest the RHS can be is when q=0, an=0, bn=999999999
    -- and that's still 1000000001, and m also < 1000000000 so it must
    -- be smaller, but I don't know how to put that into Lean-ese
    sorry

-- The most interesting case is when after.sec = before.sec + 1.
lemma case_as_eq_bs_plus_one
  (bs : ℤ)
  (an bn m : ℕ)
  (m_bound : m < ONE_S_IN_NS)
  (an_bound : an < ONE_S_IN_NS)
  (bn_bound : bn < ONE_S_IN_NS)
  : (bs + 1 + ↑0) * 1000000000 + ↑an < bs * 1000000000 + ↑bn
    ∨ ↑m ≤ (bs + 1 + ↑0) * 1000000000 + ↑an - (bs * 1000000000 + ↑bn)
    ↔ ¬0 = 0 ∨ m ≤ 1000000000 + an - bn
  := by
    -- eliminate obviously false clauses on both sides of the ↔
    -- simp can see one for itself but needs some help for the other
    simp [add_mul]
    have false_by_bounds (bs: ℤ) (an bn: ℕ)
      (an_bound: an < ONE_S_IN_NS)
      (bn_bound: bn < ONE_S_IN_NS)
      : ¬(bs * 1000000000 + 1000000000 + ↑an < bs * 1000000000 + ↑bn)
      := by linarith
    simp [false_by_bounds bs an bn an_bound bn_bound]
    -- rearrange the remaining left side of the iff
    have rearrangement (x: ℤ) (i j: ℕ)
      : x * 1000000000 + 1000000000 + ↑i - (x * 1000000000 + ↑j)
        = 1000000000 + i - j
      := by linarith
    rewrite [rearrangement bs an bn]
    -- ⊢ ↑m ≤ 1000000000 + ↑an - ↑bn ↔ m ≤ 1000000000 + an - bn
    -- bn < 1000000000, so the subtraction on the RHS cannot underflow,
    -- and both sides _should_ be equivalent, but again I don't know
    -- how to put that into Lean-ese
   sorry

theorem timespec_differences_equivalent
  : timespec_difference_at_least_mul = timespec_difference_at_least_cases
  := by
  funext a b m
  rewrite [Bool.eq_iff_iff]
  obtain ⟨m, m_bound⟩ := m
  obtain ⟨as, an, an_bound⟩ := a
  obtain ⟨bs, bn, bn_bound⟩ := b
  simp [timespec_difference_at_least_mul,
        timespec_difference_at_least_cases,
        timespec_to_ns,
        ONE_S_IN_NS]
  split_ifs with as_rel_bs
  . -- have as_rel_bs: as = bs
    simp [as_rel_bs]
    exact case_as_eq_bs an bn m
  . -- have as_rel_bs: ¬(as = bs)
    rcases lt_trichotomy as bs with as_lt_bs | _ | as_gt_bs
    . -- have as_lt_bs: as < bs
      obtain ⟨δs, rfl⟩ := Int.exists_add_of_le as_lt_bs
      exact case_as_lt_bs as δs an bn m an_bound
    . tauto -- as = bs already disposed of above
    . -- have as_gt_bs: bs < as
      -- this case must be split further into as = bs + 1 and as > bs + 1
      obtain ⟨δs, rfl⟩ := Int.exists_add_of_le as_gt_bs
      simp [x_ne_x_plus_stuff]
      cases δs with
      | zero =>
        exact case_as_eq_bs_plus_one bs an bn m m_bound an_bound bn_bound
      | succ q =>
        exact case_as_gt_bs_plus_one bs an bn m q m_bound an_bound bn_bound

[Yakov Pechersky]

being able to prove a < N → a < (complex expression)

intro h
refine h.trans_le ?_

[Yakov Pechersky]

Going to try it on your examples.

[Yakov Pechersky]

lemma case_as_gt_bs_plus_one
  (bs : ℤ)
  (an bn m q : ℕ)
  (m_bound : m < ONE_S_IN_NS)
  (an_bound : an < ONE_S_IN_NS)
  (bn_bound : bn < ONE_S_IN_NS)
  : (bs + 1 + ↑(q + 1)) * 1000000000 + ↑an < bs * 1000000000 + ↑bn
    ∨ ↑m ≤ (bs + 1 + ↑(q + 1)) * 1000000000 + ↑an - (bs * 1000000000 + ↑bn)
    ↔ ¬q + 1 = 0 ∨ m ≤ 1000000000 + an - bn
  := by
    -- the right-hand side of the equivalence is always true
    simp [Nat.add_one_ne_zero]
    -- now we have the disjunction
    -- ⊢ (bs + 1 + (↑q + 1)) * 1000000000 + ↑an < bs * 1000000000 + ↑bn
    --   ∨ ↑m ≤ (bs + 1 + (↑q + 1)) * 1000000000 + ↑an
    --           - (bs * 1000000000 + ↑bn)
    -- the right side of which is always true, but proving it requires
    -- all three bounds and a bunch of algebraic rearrangement
    right
    have rearrangement (x: ℤ) (i j k: ℕ)
      : ((((x + 1) + (↑k + 1)) * 1000000000) + ↑i)
         - ((x * 1000000000) + ↑j)
      = 1000000000 + 1000000000 + k * 1000000000 + i - j
      := by linarith
    simp [rearrangement, -Int.reduceAdd]
    -- ⊢ ↑m ≤ 2000000000 + ↑q * 1000000000 + ↑an - ↑bn
    -- an < 1000000000 and bn < 1000000000
    -- so the smallest the RHS can be is when q=0, an=0, bn=999999999
    -- and that's still 1000000001, and m also < 1000000000 so it must
    -- be smaller, but I don't know how to put that into Lean-ese
    zify at m_bound
    zify at bn_bound
    refine m_bound.le.trans ?_
    rw [le_sub_iff_add_le, add_assoc, add_assoc, add_le_add_iff_left]
    refine bn_bound.le.trans ?_
    simp only [le_add_iff_nonneg_right]
    positivity

[Yakov Pechersky]

Didn't even use an_bound.

[Zack Weinberg]

Oh, this is what refine is for? I couldn't figure it out from the documentation. (The tactics documentation could use a lot more examples.)

I'm not surprised it turns out not all of the bounds are necessary; these lemmas were spat out by extract_goal from the places where they're used, and the plan was to minimize their arguments once proven, but of course one can't do that until one is done proving them.

[Yakov Pechersky]

You don't even need to be explicit about the rearrangement

lemma case_as_gt_bs_plus_one
  (bs : ℤ)
  (an bn m q : ℕ)
  (m_bound : m < ONE_S_IN_NS)
  (an_bound : an < ONE_S_IN_NS)
  (bn_bound : bn < ONE_S_IN_NS)
  : (bs + 1 + ↑(q + 1)) * 1000000000 + ↑an < bs * 1000000000 + ↑bn
    ∨ ↑m ≤ (bs + 1 + ↑(q + 1)) * 1000000000 + ↑an - (bs * 1000000000 + ↑bn)
    ↔ ¬q + 1 = 0 ∨ m ≤ 1000000000 + an - bn
  := by
    -- the right-hand side of the equivalence is always true
    simp [Nat.add_one_ne_zero]
    right
    ring_nf
    zify at m_bound bn_bound
    refine m_bound.le.trans ?_
    rw [add_sub, le_sub_iff_add_le, show (2_000_000_000 : Int) = 1_000_000_000 + 1_000_000_000 from rfl, add_assoc, add_assoc, add_le_add_iff_left]
    refine bn_bound.le.trans ?_
    simp only [le_add_iff_nonneg_right]
    positivity

[Yakov Pechersky]

I used ring_nf to do the cancellations

[Yakov Pechersky]

Had to undo the 1B + 1B step to get into a nice form

[Yakov Pechersky]

OK, even less juggling. I used bn < 1B and made a 1B + bn <= 2B

by
    -- the right-hand side of the equivalence is always true
    simp [Nat.add_one_ne_zero]
    right
    ring_nf
    zify at m_bound bn_bound
    refine m_bound.le.trans ?_
    rw [add_sub, le_sub_iff_add_le]
    refine (add_le_add_left bn_bound.le _).trans ?_
    norm_num
    rw [add_assoc, le_add_iff_nonneg_right]
    positivity

[Zack Weinberg]

Where the heck is ring_nf documented?
I suspect I could have been using it a lot earlier if I'd known about it

[Yakov Pechersky]

When you use ring as a non-finishing tactic, it'll complain

[Yakov Pechersky]

and say, "use ring_nf to normalize expressions"

[Zack Weinberg]

Same question about ring then!

[Zack Weinberg]

And norm_num for that matter
I'm finding the documentation well-nigh useless and I don't know if I'm looking in the wrong place or what

[Aaron Liu]

Here's a list of all the tactics in mathlib:
tactics

[Zack Weinberg]

Like take https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/Ring/RingNF.html#Mathlib.Tactic.RingNF.ringNF
which is what comes up if I put "ring_nf" into the search box
I do not know what most of these words mean

[Zack Weinberg]

or, from the page @Aaron Liu linked,

tac <;> tac' runs tac on the main goal and tac' on each produced goal, concatenating all goals produced by tac'.

I think I see what that does but I have no idea when I would want to use it

[Aaron Liu]

Sometimes you do a cases a <;> cases b <;> cases c <;> simp

[Zack Weinberg]

... cases doesn't compute for me in this context

[Aaron Liu]

Take a look

[Zack Weinberg]

I'm sorry, this is just continuing to go further down the rabbit hole of things being defined in terms of other things that I don't understand either. I'm really not much of a mathematician.

[Yakov Pechersky]

lemma case_as_eq_bs_plus_one
  (bs : ℤ)
  (an bn m : ℕ)
  (bn_bound : bn < ONE_S_IN_NS)
  : (bs + 1 + ↑0) * 1000000000 + ↑an < bs * 1000000000 + ↑bn
    ∨ ↑m ≤ (bs + 1 + ↑0) * 1000000000 + ↑an - (bs * 1000000000 + ↑bn)
    ↔ ¬0 = 0 ∨ m ≤ 1000000000 + an - bn
  := by
    -- eliminate obviously false clauses on both sides of the ↔
    -- simp can see one for itself but needs some help for the other
    rw [le_tsub_iff_left (b := m) (bn_bound.le.trans (by simp))]
    zify
    ring_nf
    -- crucial here are add_sub and le_sub_iff_add_le'
    simp only [add_sub, le_sub_iff_add_le', not_true_eq_false, false_or, or_iff_right_iff_imp]
    rw [add_rotate, add_assoc, add_lt_add_iff_left]
    intro H
    linarith

[Yakov Pechersky]

First I saw that the iff had things that look like m ≤ 1000000000 + an - bn on both sides of the iff (after a ring_nf). I moved bn over the left using the tsub lemma, with a side proof that I can, because we know that 1B + an > bn (not hitting nat subtraction truncation, basically).

[Yakov Pechersky]

Then a simp to help with this goal

⊢ 1000000000 + bs * 1000000000 + ↑an < bs * 1000000000 + ↑bn ∨ ↑m ≤ 1000000000 + (↑an - ↑bn) ↔
  ¬True ∨ ↑bn + ↑m ≤ 1000000000 + ↑an

[Yakov Pechersky]

note how ↑m ≤ 1000000000 + (↑an - ↑bn) and ↑bn + ↑m ≤ 1000000000 + ↑an are basically the same

[Zack Weinberg]

@Yakov Pechersky Thank you, this is hugely helpful

[Yakov Pechersky]

Then you get a 1000000000 + bs * 1000000000 + ↑an < bs * 1000000000 + ↑bn which needs some help cancellation, and add_rotate (I guessed the name, none of add_comm, add_left_comm, add_right_comm were relevant) gets you there.

[Yakov Pechersky]

Where add_lt_add_iff_left is one I knew by name -- the name is precisely the "move" I want to make.

[Yakov Pechersky]

we then get a

bs : ℤ
an bn m : ℕ
bn_bound : bn < ONE_S_IN_NS
H : ↑an + 1000000000 < ↑bn
⊢ ↑bn + ↑m ≤ 1000000000 + ↑an

and that's something that linarith can easily handle.

[Kevin Buzzard]

Zack Weinberg said:

I also discovered a useful trick for complicated algebraic manipulation:

    ...
    have rearrangement (variables...) : [mess] = [simplified]
        := by linarith
    simp [rearrangement]
    ...

works for anything linarith can prove! This should be mentioned in beginner documentation somewhere ;-)

You can even do things like rw [show mess = simplified by linarith]

Zack Weinberg said:

Same question about ring then!

The course notes for Imperial's formalizing mathematics course contain documentation of some of the basic tactics which is far more extensive than the documentation available in the official docs. See here. Maybe this is helpful? We cover both refine and ring (and in the ring docs we also mention this rw [show ...] trick). See also the glossary here for explanation of some of the terms used.