Invertible 1 simps

Stream: mathlib4

[Thomas Murrills]

Currently we don't have an instance for Invertible (1 : α); it's just a def. That means that the associated simp lemma can't automatically apply, and we have to have first:

/-- `1` is the inverse of itself -/
def invertibleOne [Monoid α] : Invertible (1 : α) :=
  ⟨1, mul_one _, one_mul _⟩
#align invertible_one invertibleOne

@[simp]
theorem invOf_one [Monoid α] [Invertible (1 : α)] : ⅟ (1 : α) = 1 :=
  invOf_eq_right_inv (mul_one _)
#align inv_of_one invOf_one

example [Monoid α] : ⅟(1 : α) = 1 := by simp -- failed to synthesize instance Invertible 1

Should it be instance invertibleOne [Monoid α] : Invertible (1 : α) := ... instead? Or is there a reason we don't do this?

[Kyle Miller]

The issue here is that you can't write ⅟(1 : α) in the first place without the instance; this works fine:

example [Monoid α] [Invertible (1 : α)]: ⅟(1 : α) = 1 := by simp

[Kyle Miller]

My understanding is that simp will use instances that already exist in the expressions.

I think this demonstrates it: edit: no it doesn't since h is considered to be an instance inside the by block...

example [Monoid α] (h : Invertible (1 : α)) : ⅟(1 : α) = 1 := by simp

[Thomas Murrills]

Right, but many times we don't want to introduce [Invertible (1 : α)] in the hypotheses, as we're in the middle of a proof. We want to use (what seems like it should be) the instance for Invertible (1 : α) given by invertibleOne

[Yaël Dillies]

Why not do haveI := invertibleOne α?

[Kyle Miller]

In Lean 3 (or at least I thought so) I thought it was the case that simp lemmas wouldn't try to resynthesize arguments and would instead try to use unification first. That is, I thought this should work:

axiom α : Type
variable [Monoid α]
axiom h : Invertible (1 : α)

example : @Invertible.invOf _ _ _ (1 : α) h = 1 := by
  --have := ⅟(1 : α) -- fails as expected
  simp [invOf_one] -- does not use this simp lemma and fails

[Kyle Miller]

Ok, yes, this is how Lean 3 worked. Working Lean 3 example:

import algebra.invertible

axiom α : Type
variable [monoid α]
axiom h : invertible (1 : α)

example : @invertible.inv_of _ _ _ (1 : α) h = 1 := by simp [inv_of_one]

[Thomas Murrills]

Yaël Dillies said:

Why not do haveI := invertibleOne α?

Well, it's another step for what seems like it should be immediate—shouldn't lean always know that 1 is invertible, especially when simpplifying? Everything seems to work when changing def to instance, so I'm just wondering if there's any reason not to make that change.

[Kyle Miller]

It seems like having a low-priority instance for 1 would make sense to me. Maybe you could look at git blame for the mathlib 3 file and dig through discussion in any relevant PRs to see why it's not a (low-priority) instance?

[Kyle Miller]

But, just to be clear, in Lean 3 this didn't need to be an instance for the simp lemma to apply.

[Thomas Murrills]

Sounds good...I've only been learning git on an as-needed basis, so I will now go and learn what a git blame is :sweat_smile:

[Kyle Miller]

A hint, but I have to go, they've got a convenient interface for it on GitHub

[Thomas Murrills]

I was wondering what that button did :)

[Thomas Murrills]

Ok, that was a nice interface! I found this, which seems relevant:

Since `invertible a` is not a `Prop` (but it is a `subsingleton`), we have to be careful about
coherence issues: we should avoid having multiple non-defeq instances for `invertible a` in the
same context.  This file plays it safe and uses `def` rather than `instance` for most definitions,
users can choose which instances to use at the point of use.
For example, here's how you can use an `invertible 1` instance:
```lean
variables {α : Type*} [monoid α]
def something_that_needs_inverses (x : α) [invertible x] := sorry
section
local attribute [instance] invertible_one
def something_one := something_that_needs_inverses 1
end
```

[Thomas Murrills]

I wonder if those same coherence issues are present in Lean 4...based on the wording it seems likely. But maybe lean 4 has better ways to handle the situation of multiple non-defeq instances?

[Thomas Murrills]

Huh, this ties into the issue in #mathlib4 > rw failing to rewrite coercions...but only sometimes . Because that congr lemma creates an instance of Invertible 1 via Invertible.copy, and since this is unequal to invertibleOne, ⅟1 doesn't simplify.

[Thomas Murrills]

But...hmmm. this is strange. I would have thought it would pick up on the instance that is there.

[Thomas Murrills]

Here's an example using the congr lemma from that conversation.

@[congr]
theorem Invertible.cong [Ring α] (x y : α) [Invertible x] (h : x = y) :
  ⅟x = @Invertible.invOf _ _ _ y (Invertible.copy ‹_› _ h.symm) := by subst h; rfl

example [Ring α] [Invertible ((1 : ℕ) : α)] : ⅟((1 : ℕ) : α) = 1 :=
  by simp -- unsolved goals ⊢ ⅟1 = 1

[Thomas Murrills]

I'm not totally sure why following that simp up with rw [invOf_one] results in "failed to synthesize instance". Shouldn't we not even need typeclass synthesis, seeing as what we need is already present as an argument of ⅟?

[Thomas Murrills]

I wonder if

theorem invOf_one [Monoid α] {_ : Invertible (1 : α)} : ⅟ (1 : α) = 1

would make more sense.

[Thomas Murrills]

Seems like that change makes the simp work!

[Thomas Murrills]

It also makes more sense to me: why use typeclass synthesis when we can use type inference?

[Thomas Murrills]

I think there might be lots of places in Invertible where this would be a good change—unless it has some terrible effects that I'm not anticipating.

[Eric Wieser]

It's very hard to rewrite backwards if the argument is implicit

[Thomas Murrills]

Could that be worth it given how much easier this makes it to rewrite forwards?

[Thomas Murrills]

Or, would it be better to have an implicit- using lemma tagged simp and a user-facing one not tagged simp?

[Thomas Murrills]

E.g.

@[simp]
theorem invOf_one' [Monoid α] {_ : Invertible (1 : α)} : ⅟ (1 : α) = 1 :=
  invOf_eq_right_inv (mul_one _)

theorem invOf_one [Monoid α] [Invertible (1 : α)] : ⅟ (1 : α) = 1 :=
  invOf_eq_right_inv (mul_one _)

[Thomas Murrills]

Since I'm guessing simp only rewrites forward?

[Eric Wieser]

My main observations here are:

• The API of Invertible is rather annoying to work with in both Lean 3 and Lean 4
• We really shouldn't do a big (edit: Lean 4) refactor on it mid-port

[Eric Wieser]

I agree that the approach you describe could work

[Eric Wieser]

Another option would be to make the Invertible arguments explicit, and then the typeclass version probably isn't need at all

[Eric Wieser]

If you want to experiment, you could try out such a refactor in Lean 3 and see what breaks

[Thomas Murrills]

Hmm, okay! I'll give it a shot, but I might ad-hoc things a bit for my application at the moment to just get norm_num done ASAP (instead of touching Invertible.lean).

[Thomas Murrills]

While the above approaches hopefully suffice for this situation, I wonder what a general pattern is for dealing with this situation: where a forward rewrite presents all of the info necessary in such a way that type inference ought to be used, but a backwards rewrite would benefit from typeclass synthesis. I feel like there should be a standard way to handle that (maybe there is one already?)

[Kyle Miller]

@Anne Baanen Do I remember correctly that you're the one who added the Lean 3 feature where simp would try to first use unification for instance arguments? With some limited testing in this thread, it looks like this feature doesn't yet exist in Lean 4.

[Anne Baanen]

You remember correctly that I modified simp handling of instances in lean#659, although it's a bit more subtle than that: instantiate_emetas_fn will loop over all metavariables (i.e. arguments to the simp lemma), trying to synthesize an instance if it is ready according to ready_to_synthesize: the only metavariables in the parameter type are out-params. If the instance is not ready to synthesize, it will proceed to attempt assigning other metas in the hope the previous are assigned in the process, or at least ready for synthesis.

[Thomas Murrills]

Adjusting simp sounds neat! In the meantime, I tried the approach of duplicating definitions above in mathlib3 (the version where I duplicate the whole definition instead of having them refer to each other, since the former is easier to do with regexes...) and nothing broke after changing as many definitions as possible. (That's on the branch invertible-refactor.)