Stuck on first project - simplification on struct fields

Stream: new members

[Zack Weinberg]

I am trying to prove two versions of a function are equivalent. This is what I have so far:

abbrev ONE_S_IN_NS : Nat := 1000000000
abbrev Nsec : Type := Fin ONE_S_IN_NS
structure Timespec where
  sec  : Int
  nsec : Nsec
deriving Repr

def timespec_to_ns (tv: Timespec) : Int :=
  tv.sec * ONE_S_IN_NS + tv.nsec

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

def timespec_difference_at_least_cases
  (after : Timespec) (before: Timespec) (min_ns: Nsec) : Bool :=
  if after.sec = before.sec then
    after.nsec < before.nsec || after.nsec > before.nsec + min_ns
  else if after.sec = before.sec + 1 then
    let delta_ns := Int.ofNat (after.nsec + ONE_S_IN_NS) - before.nsec;
    delta_ns < 0 || delta_ns >= min_ns
  else true

theorem timespec_differences_equivalent :
  timespec_difference_at_least_mul = timespec_difference_at_least_cases
  := by
  funext a b m
  unfold timespec_difference_at_least_mul timespec_difference_at_least_cases timespec_to_ns
  simp
  if case1: a.sec = b.sec then
    rw [case1]
    simp
    sorry
  else sorry -- more cases to be worked out later

Right after the simp I have a messy formula in the goal window,

a b : Timespec
m : Nsec
case1 : a.sec = b.sec
⊢ (decide (b.sec * 1000000000 + ↑↑a.nsec - (b.sec * 1000000000 + ↑↑b.nsec) < 0) ||
      decide (↑↑m ≤ b.sec * 1000000000 + ↑↑a.nsec - (b.sec * 1000000000 + ↑↑b.nsec))) =
    (decide (a.nsec < b.nsec) || decide (b.nsec + m < a.nsec))

and now I need to do some algebraic manipulation to cancel out b.sec * 1000000000. The obvious next step would seem to be rw [← Int.sub_sub] to distribute the minus sign in - (b.sec * 1000000000 + ↑↑b.nsec) but that fails with "tactic 'rewrite' failed, motive is not type correct" presumably because b.nsec isn't an Int. Everything else I've tried gives either similar type errors or pattern matching failures.

I can't find anything about this kind of problem in the manuals. Any advice you might have would be helpful.

(Note: I'm currently trying to do this without benefit of mathlib, because <https://github.com/leanprover-community/ProofWidgets4/issues/115> prevents me from installing mathlib. In particular this means I don't have the use of linarith.)

[Johannes Tantow]

I think it would be best to switch from showing that both functions result in the same boolean value to showing that the first results in true iff the second results in true. This removes all the decide statements.

theorem timespec_differences_equivalent :
  timespec_difference_at_least_mul = timespec_difference_at_least_cases
  := by
  funext a b m
  rw [Bool.eq_iff_iff] -- new introduced
  simp [timespec_difference_at_least_mul, timespec_difference_at_least_cases, timespec_to_ns]
  if case1: a.sec = b.sec then
    rw [case1]
    simp
    rw [← Int.sub_sub]


    sorry
  else sorry -- more cases to be worked out later