Instance transparency issue?

Stream: mathlib4

[Jakob von Raumer]

The following bit in Lean 3

instance has_lt' : has_lt string :=
⟨λ s₁ s₂, ltb s₁.mk_iterator s₂.mk_iterator⟩

instance decidable_lt : @decidable_rel string (<) :=
by apply_instance -- short-circuit type class inference

doesn't work without adaption in Lean 4, but instead I have to do the following:

instance lt' : LT String :=
  ⟨fun s₁ s₂ => ltb s₁.mkIterator s₂.mkIterator⟩

instance decidable_lt : @DecidableRel String (· < ·) := by
  simp only [lt']
  infer_instance  -- short-circuit type class inference

Does anybody know why this is? Is this intended?

[Jakob von Raumer]

I guess the inference doesn't unfold exactly the same was as before?

[Heather Macbeth]

On the following example, it seems that instance transparency is not behaving correctly over ℚ. There is a goal where with_reducible_and_instances (apply mul_le_mul) behaves differently over a generic linearly ordered field than over ℚ. That's not intended, is it?

import Mathlib.Data.Rat.Order

variable [LinearOrderedField α]

/- `.reducible` transparency works correctly over `ℚ`. -/
example {a b : ℚ} : a / 2 ≤ b / 2 := by
  with_reducible (apply mul_le_mul) -- fails, as desired

/- `.instance` transparency works correctly over a generic field. -/
example {a b : α} : a / 2 ≤ b / 2 := by
  with_reducible_and_instances (apply mul_le_mul) -- fails, as desired

/- `.instance` transparency does not work correctly over `ℚ`. -/
example {a b : ℚ} : a / 2 ≤ b / 2 := by
  with_reducible_and_instances (apply mul_le_mul) -- succeeds, wanted it not to
  all_goals sorry

[Heather Macbeth]

Ping @Mario Carneiro with whom I was discussing similar things recently.

[Floris van Doorn]

with_reducible_and_instances seems to work as expected: by unfolding the instance docs4#Rat.instDivRat, the goal becomes a multiplication.
If you want this to fail, define a (semireducible) def def Rat.div := ...that is used to define this instance.

[Heather Macbeth]

@Floris van Doorn Thanks for investigating! Do you think it would be acceptable to the community as a whole to make the Rat Div instance semireducible in this way?

[Floris van Doorn]

I don't see any problem with that change, and it seems good if it makes Rat behave more like a variable type.

[Heather Macbeth]

And while I'm at it, the same for Real?

[Heather Macbeth]

It's tricky because Real gets its Div instance from the default field in docs4#DivInvMonoid. Do you know if there is a way to make any DivInvMonoid with the default value for Div have that instance be semireducible?

[Floris van Doorn]

I think you just define Real.div, then use div := Real.div and div_eq_mul_inv := fun _ _ => rfl

[Heather Macbeth]

I mean, is there a solution which works not just for Real but all at once for any DivInvMonoid constructed to pull the default value for Div.

[Floris van Doorn]

maybe make the default value id (a * b⁻¹) instead of a * b⁻¹ (assuming id is semireducible)

[Heather Macbeth]

Maybe, though, we should do this for every default field which is a typeclass?

[Floris van Doorn]

Yeah, that will probably increase consistency between variable types and concrete types.

[Heather Macbeth]

Maybe there's even a way to do this automatically.

[Floris van Doorn]

if we go that route, it might be even better to make the default value irreducible_id (a * b⁻¹) (where irreducible_id is an irreducible version of id): that will increase the consistency even further.

[Yaël Dillies]

Won't that make the default proofs fail, though?

[Yaël Dillies]

I mean that (div_eq_mul_inv := rfl) won't work anymore.

[Floris van Doorn]

true, but we can make the default proof the tactic that does unfold irreducible_id; rfl

[Heather Macbeth]

Would this be a Lean 4 change?

[Floris van Doorn]

No, I was just thinking about manually changing this in each mathlib4 class where we want to do this.

[Heather Macbeth]

Maybe it could be a Lean 4 change though?

[Heather Macbeth]

Or do you think we want to experiment with that pattern in mathlib before proposing to make it the standard behaviour across Lean?

[Floris van Doorn]

Yes, and I think the behavior is sufficiently unexpected that I don't think it's desired default behavior.

[Heather Macbeth]

I have implemented the suggestions here for making instance transparency behave the same way on particular DivInvMonoids (Rat, Real) as on a generic one. It seems to work: see the branch
https://github.com/leanprover-community/mathlib4/compare/hrmacbeth-instance-transparency

I'll PR first the change to Std (for Rat) and then the change to Mathlib4 (for the default field of DivInvMonoid).

[Heather Macbeth]

Std4#92

[Heather Macbeth]

mathlib4#1896 to get that std change into mathlib

[Heather Macbeth]

And mathlib4#1897 for the mathlib changes.