Zulip Chat Archive
Stream: new members
Topic: Stuck on first project - simplification on struct fields
Zack Weinberg (Apr 29 2025 at 16:28):
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 (Apr 29 2025 at 19:50):
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
Last updated: May 02 2025 at 03:31 UTC