congr lemma for invertible

Stream: general

[Eric Wieser]

Right now this fails:

import algebra.invertible

example {R : Type*} [monoid R] {r₁ r₂ : R}
  [invertible r₁] [invertible r₂] (h : r₁ = r₂) : ⅟r₁ = ⅟r₂ :=
by simp [h] -- fails

Is there a way to provide a congr lemma so that this works?

[Eric Wieser]

My naive attempt was:

lemma invertible_congr {R : Type*} [monoid R] {r₁ r₂ : R}
  [i₁ : invertible r₁] [i₂ : invertible r₂] (h : r₁ = r₂) : ⅟r₁ = ⅟r₂ :=
begin
  substI h,
  convert rfl,
end

but this doesn't accept a @[congr] attribute

[Eric Wieser]

If I introduce a stupid alias for invertible.inv_of that takes a monoid argument, then @[congr] is happy:

import algebra.invertible

variables {R : Type*} [monoid R] {r₁ r₂ : R} [invertible r₁] [invertible r₂]

/-- A duplicate of `⅟` that makes `congr` happy -/
abbreviation invertible.inv_of' (r : R) [invertible r] := ⅟r
notation `⅟'` := invertible.inv_of'

/-- `congr` is happy as long as we use `⅟'`-/
@[congr] lemma invertible_congr' (h : r₁ = r₂) : ⅟'r₁ = ⅟'r₂ :=
by { substI h, congr }

/- `simp` is happy as long as we use `⅟'` on the LHS-/
example (h : r₁ = r₂) : ⅟'r₁ = ⅟'r₂ := by simp [h] -- ok
example (h : r₁ = r₂) : ⅟'r₁ = ⅟r₂ := by simp [h] -- ok
example (h : r₁ = r₂) : ⅟r₁ = ⅟'r₂ := by simp [h] -- fails
example (h : r₁ = r₂) : ⅟r₁ = ⅟r₂ := by simp [h] -- fails

[Gabriel Ebner]

Yes, this is a known limitation in Lean 3. It is already gone in Lean 4.

[Eric Wieser]

Are there any known workarounds?

[Gabriel Ebner]

I guess you could state the lemma like this (untested):

class is_monoid (R) [has_mul R] [has_one R] : Prop := ...
instance {R} [monoid R] : is_monoid R := ...

@[congr]
lemma invertible_congr {R : Type*} [has_mul R] [has_one R] [is_monoid R] {r₁ r₂ : R}
  [i₁ : invertible r₁] [i₂ : invertible r₂] (h : r₁ = r₂) : ⅟r₁ = ⅟r₂ :=

[Eric Wieser]

Nice, that does the trick:

import algebra.invertible

variables {R : Type*} [monoid R] {r₁ r₂ : R} [invertible r₁] [invertible r₂]

class is_monoid (R) [has_mul R] [has_one R] : Prop :=
(out [] : ∃ m : monoid R, mul_one_class.to_has_one R = ‹_› ∧ mul_one_class.to_has_mul R = ‹_›)

instance monoid.is_monoid {R} [monoid R] : is_monoid R :=
⟨⟨‹_›, rfl, rfl⟩⟩

@[congr]
lemma invertible_congr {R : Type*} [has_mul R] [has_one R] [is_monoid R] {r₁ r₂ : R}
  [i₁ : invertible r₁] [i₂ : invertible r₂] (h : r₁ = r₂) : ⅟r₁ = ⅟r₂ :=
by {
  unfreezingI { obtain ⟨m : monoid R, rfl, rfl⟩ := is_monoid.out R },
  substI h, congr }

example (h : r₁ = r₂) : ⅟r₁ = ⅟r₂ := by simp [h] -- ok

[Eric Wieser]

Is that something that is ok in mathlib? Perhaps renaming is_monoid to invertible_congr_aux or something to discourage widespread use?

[Reid Barton]

Don't know what's going on here but (a) is_monoid should be called is_monoid and not invertible_congr_aux (b) is_monoid shouldn't be a class, if you want a class, just use monoid

[Eric Wieser]

@Reid Barton, if I use [monoid R] then @[congr] complains. By using the is_monoid R hack above, it doesn't

[Reid Barton]

Is this really worth fixing?

[Reid Barton]

or at least, in this way? it seems like a quite generic sort of issue?

[Eric Wieser]

Right, but this is also a generic recipe for solving it - here's the version with it called aux:

import algebra.invertible

/-- typeclass to hide arguments for `invertible_congr` that `congr` rejects.
The equalities are used to substitute arguments in `invertible_congr` with expressions built from
the data fields. -/
class inductive invertible_congr.aux (R) [has_mul R] [has_one R] : Prop
| intro
    (monoid : monoid R)
    (h_one_eq : mul_one_class.to_has_one R = ‹_›)
    (h_mul_eq : mul_one_class.to_has_mul R = ‹_›) : invertible_congr.aux

instance invertible_congr.aux.inst {R} [monoid R] : invertible_congr.aux R :=
⟨‹_›, rfl, rfl⟩

variables {R : Type*} [monoid R] {r₁ r₂ : R} [invertible r₁] [invertible r₂]

/--
This can't take a `[monoid]` argument as `@[congr]` does not allow the `mul_one_class.to_has_one`
term that appears in the goal. Instead we take a typeclass that allows us to replace the `has_one R`
term with such an expression within the proof. -/
@[congr]
lemma invertible_congr {R : Type*} [has_mul R] [has_one R] [invertible_congr.aux R] {r₁ r₂ : R}
  [i₁ : invertible r₁] [i₂ : invertible r₂] (h : r₁ = r₂) : ⅟r₁ = ⅟r₂ :=
begin
  unfreezingI { obtain ⟨m, rfl, rfl⟩ := ‹invertible_congr.aux R› },
  substI h,
  congr
end

example (h : r₁ = r₂) : ⅟r₁ = ⅟r₂ :=
begin
  simp [h],
end

[Reid Barton]

I don't really think we should be adding a bunch of workarounds to mathlib like this

[Eric Wieser]

The alternative is facing annoying situations where simp makes no progress

[Reid Barton]

seems okay!

[Reid Barton]

There are other tactics

[Eric Wieser]

Sure, but the tradeoff is either:

• have a bizarre workaround like the one above, that no one ever looks at again, which gets silently removed in mathlib4
• have multiple users run into the same problem every time, and produce weird proofs as workarounds that stick around in mathlib4

[Eric Wieser]

How would you solve this goal?

example  {R : Type*} [monoid R] (foo : ℕ → R) (bar : ℕ → R)
  [invertible (foo 1)] [invertible (bar 2)] (h : foo 1 = bar 2) :
  37 + ⅟(foo 1) = 37 + ⅟(bar 2) :=
sorry

[Eric Wieser]

The natural sequence of thing to try is rw h, simp_rw h, and simp [h] in some order, and all of those fail.

[Eric Wieser]

With the code above hidden away in mathlib, simp_rw h works fine

[Reid Barton]

It just looks worse to me to add 20 lines of obscurities per instance of this issue. That's all

[Eric Wieser]

I suppose there are two more options, which are:

• Fix the problem in Lean 3 core
• Write a metaprogram to generate the above boilerplate

I think having Lean 4 on the horizon makes these look less desirable than accumulating the 20 lines each time.

[Mario Carneiro]

I agree with Reid, you should just use congr_arg or something if this comes up, adding typeclasses seems like it will cause lots of downstream problems for a proof-local issue

[Eric Wieser]

What proof would you suggest for the above sorry, Mario?

[Gabriel Ebner]

I might be biased because I suggested the hack, but I don't think it will cause any technical issues (as long as it is only used for this congruence lemma). It's a type class with a single instance, that is only required by a single lemma. And this congruence lemma is only triggered when the simplifier sees an inv_of constant. Any potential negative impact is extremely limited.

The simplifier should be able to rewrite under inv_of; we have similar congruence lemmas for fintype.card etc. Adding this congruence lemma would only be consistent.

Finally, the hack is short-lived. We can remove it immediately after switching to Lean 4. (The congruence lemma will work when written with [Monoid R] instead of [Mul R] [One R] [IsMonoid R].)

[Mario Carneiro]

I see, if it's a specialized typeclass then I agree it's more contained. The docs should make it clear that it's not intended for use beyond that though

[Mario Carneiro]

the is_monoid name sounds like it will get used elsewhere

[Yaël Dillies]

What about monoid_congr_class_warning_do_not_use?

[Mario Carneiro]

@Eric Wieser Is that a MWE? 37 + ⅟(foo 1) doesn't typecheck

[Eric Wieser]

Yaël Dillies said:

What about monoid_congr_class_warning_do_not_use?

At that point, invertible_congr.aux as I use above is better

[Eric Wieser]

Fixed to be a MWE

[Mario Carneiro]

import algebra.invertible

lemma invertible_congr {R : Type*} [monoid R] {r₁ r₂ : R}
  [i₁ : invertible r₁] [i₂ : invertible r₂] (h : r₁ = r₂) : ⅟r₁ = ⅟r₂ :=
begin
  substI h,
  convert rfl,
end

example {R : Type*} [ring R] (foo : ℕ → R) (bar : ℕ → R)
  [invertible (foo 1)] [invertible (bar 2)] (h : foo 1 = bar 2) :
  37 + ⅟(foo 1) = 37 + ⅟(bar 2) :=
by { congr' 1, exact invertible_congr h }

[Eric Wieser]

Probably the argument goes that we should have invertible_congr in that form for human use anyway, and then provide invertible_congr' for Lean 3's sake with the weird typeclass