to_additive and iffs with Exists

Stream: mathlib4

[Yakov Pechersky]

mathlib4#666
Somehow, it fails to translate the internal .match_1, which I need a lot in mathlib4#549

import Mathlib.Tactic.ToAdditive

@[to_additive]
def IsUnit [Mul M] (a : M) : Prop := a ≠ a

-- this works fine
@[to_additive]
theorem isUnit_iff_inv [Mul M] {a : M} : IsUnit a ↔ a ≠ a :=
  ⟨fun h => absurd rfl h, fun h => h⟩
#print isAddUnit_iff_neg

/-
The declaration isUnit_iff_exists_inv depends on the declaration isUnit_iff_exists_inv.match_1 which
is in the namespace isUnit_iff_exists_inv, but does not have the `@[to_additive]` attribute.
This is not supported.  Workaround: move isUnit_iff_exists_inv.match_1 to a different namespace.
-/
@[to_additive]
theorem isUnit_iff_exists_inv [Mul M] {a : M} : IsUnit a ↔ ∃ b : α, a ≠ a :=
  ⟨fun h => absurd rfl h, fun ⟨b, hab⟩ => hab⟩

-- attribute [to_additive isAddUnit_iff_exists_neg.match_1] isUnit_iff_exists_inv.match_1
-- attribute [to_additive] isUnit_iff_exists_inv

[Scott Morrison]

@Edward Ayers ?

[Edward Ayers]

I guess the auxiliary definition traversing part of to_additive is broken. You can get to_addtive to trace what it's doing with the to_additive and to_additive_detail trace classes.

[Heather Macbeth]

I also hit this:
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/to_additive.20thinks.20it's.20in.20a.20namespace

[Floris van Doorn]

I'll take a look

[Floris van Doorn]

Fixed in mathlib4#680

[Ruben Van de Velde]

docBlame linter is failing, in case you hadn't noticed :)

[Scott Morrison]

This is great; lots of ports have been running into this, I think.

[Yakov Pechersky]

Unfortunately, hit another issue:

import Mathlib.Algebra.Group.Defs

@[to_additive]
def IsUnit' [Monoid M] (a : M) : Prop := ∃ b : M, a * b = 1

@[to_additive]
theorem isUnit'_iff_exists_inv [CommMonoid M] {a : M} : IsUnit' a ↔ ∃ b, a * b = 1 := Iff.rfl

@[to_additive]
theorem isUnit'_iff_exists_inv' [CommMonoid M] {a : M} : IsUnit' a ↔ ∃ b, b * a = 1 := by
  simp [isUnit'_iff_exists_inv, mul_comm]

[Yakov Pechersky]

I can work around it by supplying a different proof tactic

[Yakov Pechersky]

:= by
  rw [isUnit_iff_exists_inv]
  simp [mul_comm]

works fine

[Floris van Doorn]

I can fix this case, but it feels a like like playing whack-a-mole. I need to have more information to have more information to fix it properly.
Maybe @Mario Carneiro or @Gabriel Ebner can answer the following questions:

• Is it documented somewhere what kind of auxiliary declarations a declaration can create, and more specifically: how these are named, if they are not giving an internal name (caught by Lean.Name.isInternal). So far I've found <declName> followed by match_<i>, proof_<i>or eq_<i> or <mainModule>._auxLemma.<i>. Are there others?
• Is there a reason that Lean.Name.isInternal doesn't mark all numeric names (with Name.num) as internal? They seem pretty internal to me.

[Gabriel Ebner]

I don't think there's an exhaustive documentation anywhere. One reason why isInternal doesn't return true on .num is because of hygienic names. The macro scopes in a name are encoded as .num.

[Floris van Doorn]

@Yakov Pechersky Your issue is fixed in #699

[Yakov Pechersky]

Thank you!

[Scott Morrison]

mathlib4#699

[Scott Morrison]

I'm happy to merge mathlib4#689; is it ready to go, and the TODO in the PR description can come later?

[Floris van Doorn]

I'm actually currently rewriting it, because there is a case of handling numeral literals it isn't catching (the commented out test-case).
I'm fine either way if you merge the current version already, or wait until my rewrite...
(the TODO in the PR description was mathlib4#699, and I just removed it)

[Floris van Doorn]

I pushed my new version.
I expect that there are still some bugs with the interaction of @[to_additive] and numerals on Nat (and other fixed types), but please report one if you encounter it.

I made the solution quite flexible, so that if there is another function that takes numeric literals as argument, you can tell @[to_additive] to never change the literal, or you can tell @[to_additive] to change the literal only if the first argument is a variable.

[Jireh Loreaux]

I would like to see mathlib4#689 merged as it fixes an issue I was encountering.

[Scott Morrison]

I propose we keep merging fixes to to_additive as fast as they come. :-)