another rat reducibility issue?

Stream: mathlib4

[Heather Macbeth]

I'm encountering an odd bug which seems to involve a combination of ℚ-specific issues, transparency, and the new attribute functionality in the apply_rules tactic.

import Mathlib.Algebra.Order.Field.Basic
import Mathlib.Data.Rat.Order
import Mathlib.Tactic.SolveByElim

attribute [dummy_tag_attr] add_lt_add_left div_lt_div_of_lt

-- fails, doesn't apply `add_lt_add_left`
example {p q r : ℚ} (h1 : p < q) (h2 : (0:ℚ) < 2) :
    (r + p) / 2 < (r + q) / 2 := by
  apply_rules (config := { transparency := .reducible }) [h1, h2] using dummy_tag_attr
  done

-- works over a generic field (whereas fails over `ℚ`)
example [LinearOrderedField α] {p q r : α} (h1 : p < q) (h2 : (0:α) < 2) :
    (r + p) / 2 < (r + q) / 2 := by
  apply_rules (config := { transparency := .reducible }) [h1, h2] using dummy_tag_attr
  done

-- works when lemmas are listed outright (whereas fails with attribute)
example {p q r : ℚ} (h1 : p < q) (h2 : (0:ℚ) < 2) :
    (r + p) / 2 < (r + q) / 2 := by
  apply_rules (config := { transparency := .reducible }) [h1, h2, add_lt_add_left, div_lt_div_of_lt]
  done

-- works at default transparency (whereas failes at `.reducible`)
example {p q r : ℚ} (h1 : p < q) (h2 : (0:ℚ) < 2) :
    (r + p) / 2 < (r + q) / 2 := by
  apply_rules [h1, h2] using dummy_tag_attr
  done

[Heather Macbeth]

I'm working off Std commit 04b3c9831e0c141713a70e68af7e40973ec9a1ff, which should be fixing at least one other rat-reducibility issue, as discussed today in
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/slow.20.60positivity.60

[Heather Macbeth]

@Mario Carneiro helped me debug this and I am recording what we learned for future reference. The issue can be simplified to an issue in apply @add_lt_add_left, as follows:

import Mathlib.Algebra.Order.Field.Basic
import Mathlib.Data.Rat.Order

example {p q r : ℚ} (h1 : p < q) (h2 : (0:ℚ) < 2) :
    (r + p) / 2 < (r + q) / 2 := by
  apply div_lt_div_of_lt h2
  apply @add_lt_add_left -- works
  exact h1

example {p q r : ℚ} (h1 : p < q) (h2 : (0:ℚ) < 2) :
    (r + p) / 2 < (r + q) / 2 := by
  apply div_lt_div_of_lt h2
  with_reducible apply @add_lt_add_left -- fails
  exact h1

[Heather Macbeth]

The reason it doesn't work at reducible transparency is that there are actually two LT ℚ instances around, one short-circuiting the other. If you force the goal back to the usual instance with show, then it works again:

example {p q r : ℚ} (h1 : p < q) (h2 : (0:ℚ) < 2) :
    (r + p) / 2 < (r + q) / 2 := by
  apply div_lt_div_of_lt h2
  show r + p < r + q
  with_reducible apply @add_lt_add_left -- works, note that this changes the `LT ℚ` instance
  exact h1

[Heather Macbeth]

A naive conclusion might be that in a tactic you want to insert these shows everywhere. But this is a bit silly. The better conclusion (if I am summarizing Mario correctly) is that .reducible transparency is just too strong for most metaprogramming purposes, and instead you want to use .instance transparency. This works:

example {p q r : ℚ} (h1 : p < q) (h2 : (0:ℚ) < 2) :
    (r + p) / 2 < (r + q) / 2 := by
  apply div_lt_div_of_lt h2
  with_reducible_and_instances apply @add_lt_add_left -- works
  exact h1

[Heather Macbeth]

(and that's the reason why I started asking questions about instance transparency in the last couple days)