moving lemmas between files

Stream: general

[Damiano Testa]

Dear All,

I wanted to use the first of the lemmas below with the assumption that {R : Type*} [linear_ordered_add_comm_group R], (a b c : R). However, those lemmas take as an assumption [linear_ordered_ring R]. If I am not mistaken, there is no multiplication in either the statement, nor the proof. Should these lemmas be moved?

They now are in src/algebra/ordered_ring.lean and I think that they should go to src/algebra/ordered_group.lean.

lemma sub_le_of_abs_sub_le_left (h : abs (a - b) ≤ c) : b - c ≤ a :=
if hz : 0 ≤ a - b then
  (calc
      a ≥ b     : le_of_sub_nonneg hz
    ... ≥ b - c : sub_le_self _ $ (abs_nonneg _).trans h)
else
  have habs : b - a ≤ c, by rwa [abs_of_neg (lt_of_not_ge hz), neg_sub] at h,
  have habs' : b ≤ c + a, from le_add_of_sub_right_le habs,
  sub_left_le_of_le_add habs'

lemma sub_le_of_abs_sub_le_right (h : abs (a - b) ≤ c) : a - c ≤ b :=
sub_le_of_abs_sub_le_left (abs_sub a b ▸ h)

lemma sub_lt_of_abs_sub_lt_left (h : abs (a - b) < c) : b - c < a :=
if hz : 0 ≤ a - b then
   (calc
      a ≥ b     : le_of_sub_nonneg hz
    ... > b - c : sub_lt_self _ ((abs_nonneg _).trans_lt h))
else
  have habs : b - a < c, by rwa [abs_of_neg (lt_of_not_ge hz), neg_sub] at h,
  have habs' : b < c + a, from lt_add_of_sub_right_lt habs,
  sub_left_lt_of_lt_add habs'

lemma sub_lt_of_abs_sub_lt_right (h : abs (a - b) < c) : a - c < b :=
sub_lt_of_abs_sub_lt_left (abs_sub a b ▸ h)

[Johan Commelin]

sounds good to me. just try it, and if it works: PR

[Damiano Testa]

My main issue is that I get lots of timeouts when I replace them...

[Damiano Testa]

So, I got it to compile once, but I could not reproduce it afterwards...

[Johan Commelin]

hmm, that seems bad

[Johan Commelin]

I don't have time to look into this now. Hopefully someone else can help

[Damiano Testa]

Well, I pushed it and we will see what Lean thinks!

#5416

[Damiano Testa]

leanpkg configure complains about a deterministic timeout in a file that I do not think that I touched (and certainly that I did not intend to touch)!

I do not understand what I should try to fix this, though...

Run leanpkg configure
  leanpkg configure
  lean --json -T100000 --make src | python scripts/detect_errors.py
  shell: /bin/bash -e {0}
  env:
    GIT_HISTORY_DEPTH: 20
    short_lean_version: 3.23.0
    pythonLocation: /opt/hostedtoolcache/Python/3.8.6/x64
configuring mathlib 0.1
/home/runner/work/mathlib/mathlib/src/data/polynomial/monic.lean:168:0: error: (deterministic) timeout

Error: Process completed with exit code 1.

[Eric Wieser]

A lot of PRs have been failing there

[Eric Wieser]

https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.235409/near/220330716

[Damiano Testa]

Thanks for the pointer!

I was relying on CI to check that the move is correct, I was worried about this timeout! Hopefully, it is not my fault!

[Damiano Testa]

The second run worked! All checks passed!

[Johan Commelin]

Kicked it on the queue

[Damiano Testa]

Thank you very much!