Zulip Chat Archive

Stream: mathlib4

Topic: Instance transparency issue?


Jakob von Raumer (Dec 15 2022 at 20:35):

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 (Dec 15 2022 at 20:38):

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

Heather Macbeth (Jan 26 2023 at 04:59):

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 (Jan 26 2023 at 04:59):

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

Floris van Doorn (Jan 26 2023 at 10:00):

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 (Jan 26 2023 at 18:24):

@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 (Jan 26 2023 at 18:25):

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 (Jan 26 2023 at 18:26):

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

Heather Macbeth (Jan 26 2023 at 18:29):

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 (Jan 26 2023 at 18:30):

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

Heather Macbeth (Jan 26 2023 at 18:31):

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 (Jan 26 2023 at 18:31):

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

Heather Macbeth (Jan 26 2023 at 18:32):

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

Floris van Doorn (Jan 26 2023 at 18:33):

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

Heather Macbeth (Jan 26 2023 at 18:34):

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

Floris van Doorn (Jan 26 2023 at 18:34):

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 (Jan 26 2023 at 18:35):

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

Yaël Dillies (Jan 26 2023 at 18:36):

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

Floris van Doorn (Jan 26 2023 at 18:41):

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

Heather Macbeth (Jan 26 2023 at 18:42):

Would this be a Lean 4 change?

Floris van Doorn (Jan 26 2023 at 18:43):

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

Heather Macbeth (Jan 26 2023 at 18:47):

Maybe it could be a Lean 4 change though?

Heather Macbeth (Jan 26 2023 at 18:48):

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 (Jan 26 2023 at 20:07):

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

Heather Macbeth (Jan 28 2023 at 01:31):

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 (Jan 28 2023 at 01:38):

Std4#92

Heather Macbeth (Jan 28 2023 at 02:05):

mathlib4#1896 to get that std change into mathlib

Heather Macbeth (Jan 28 2023 at 02:10):

And mathlib4#1897 for the mathlib changes.


Last updated: Dec 20 2023 at 11:08 UTC