[Merged by Bors] - fix(tactic/linarith): fix bug in linarith

[semorrison]

I discovered this bug while porting linarith to mathlib4, and @digama0 minimised and identified the problem. There is a zulip discussion explaining the details.

When applying Imbert's first acceleration theorem the code was incorrectly interpreting what an "implicitly eliminated variable" was.

I've added two tests, a one-liner that Mario reduced the problem too, as well as a longer one which had been failing in the mathlib4 port (due to different variable ordering).

The change causes one proof to timeout, which has been sped up.

---

[adomani]

I do not know if you are interested, but if I replace the proof that timed out with

lemma coe_real_preimage_closed_ball_inter_eq
  {x ε : ℝ} (s : set ℝ) (hs : s ⊆ closed_ball x (|p|/2)) :
  coe⁻¹' closed_ball (x : add_circle p) ε ∩ s = if ε < |p|/2 then (closed_ball x ε) ∩ s else s :=
begin
  cases le_or_lt (|p|/2) ε with hε hε,
  { rcases eq_or_ne p 0 with rfl | hp,
    { simp only [abs_zero, zero_div] at hε,
      simp only [not_lt.mpr hε, coe_real_preimage_closed_ball_period_zero, abs_zero, zero_div,
        if_false, inter_eq_right_iff_subset],
      exact hs.trans (closed_ball_subset_closed_ball $ by simp [hε]), },
    simp [closed_ball_eq_univ_of_half_period_le p hp ↑x hε, not_lt.mpr hε], },
  { suffices : ∀ (z : ℤ), closed_ball (x + z • p) ε ∩ s = if z = 0 then closed_ball x ε ∩ s else ∅,
    { simp [-zsmul_eq_mul, ← quotient_add_group.coe_zero, coe_real_preimage_closed_ball_eq_Union,
        Union_inter, Union_ite, this, hε], },
    intros z,
    simp only [real.closed_ball_eq_Icc, zero_sub, zero_add] at ⊢ hs,
    rcases eq_or_ne z 0 with rfl | hz, { simp, },
    simp only [hz, zsmul_eq_mul, if_false, eq_empty_iff_forall_not_mem],
    rintros y ⟨⟨hy₁, hy₂⟩, hy₀⟩,
    obtain ⟨hy₃, hy₄⟩ := hs hy₀,
    rcases lt_trichotomy 0 p with hp | rfl | hp,
    { cases int.cast_le_neg_one_or_one_le_cast_of_ne_zero ℝ hz with hz' hz',
      { have : ↑z * p ≤ - p, nlinarith,
        linarith [abs_eq_self.mpr hp.le] },
      { have : p ≤ ↑z * p, nlinarith,
        linarith [abs_eq_self.mpr hp.le] } },
    { simp only [mul_zero, add_zero, abs_zero, zero_div] at hy₁ hy₂ hε,
      linarith },
    { cases int.cast_le_neg_one_or_one_le_cast_of_ne_zero ℝ hz with hz' hz',
      { have : - p ≤ ↑z * p, nlinarith,
        linarith [abs_eq_neg_self.mpr hp.le] },
      { have : ↑z * p ≤ p, nlinarith,
        linarith [abs_eq_neg_self.mpr hp.le] } } },
end

then, on my computer, elaboration takes under 4s.

Essentially, all that I did was replacing the "complicated" nlinarith call by a very simple one and then proceed with linarith as before. I had to split two merged proof to achieve this, though.

[eric-wieser]

bors d+

I haven't reviewed the paper to check this is correct, but it fixes the original examples, works on mathlib, and fixes the testcase I found yesterday.

If you want a review from someone who cross-checked with the paper too, then probably best to wait a bit longer.

[bors]

✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[semorrison]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests