to_additive and coe

Stream: mathlib4

[Kevin Buzzard]

I don't think I know how to check what attributes are attached to a declaration any more (I think #print no longer tells you) but I have evidence to suggest that neither @[coe, to_additive] nor @[to_additive, coe] will attach the coe tag to the to_additivised declaration. Is it worth opening an issue? My memory about this sort of thing in Lean 3 was a bit like learning the order of adjectives in German -- some attributes needed to be before/after others to make them work best. In some sense I don't know which one of coe and to_additive I would instinctively expect to want to put first in order to make this work, but right now I think neither does.

[Kevin Buzzard]

Oh I've just realised that this is slightly more serious than I'd realised. For example @[norm_cast, to_additive] used to put the norm_cast tag on the additivised declaration and now it doesn't, so autoported norm_cast proofs can break. Currently I'm adding the tags manually but this doesn't sound ideal.

[Moritz Doll]

I think opening an issue for that would be good and even better if you could give a #mwe. I will have a look into it later. At the moment the only attributes added are instance and simp.

[Kevin Buzzard]

I'll do this, once I find out how to see the attributes attached to a declaration (I just asked here)

[Moritz Doll]

I would be happy if you produce an error for a proof that should work. then we can add that to the tests after fixing the problem

[Kevin Buzzard]

Yes I'll do this but it would be great for debugging purposes if I could actually see what was going on!

[Moritz Doll]

I'll have a look whether I can hack a command together that shows all the attributes

[Scott Morrison]

This is difficult. There is currently not a uniform method for recording attributes: each attribute is responsible for looking after itself!

[Scott Morrison]

Mario has some ideas for doing this systematically, perhaps someone can find the thread.

[Moritz Doll]

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/How.20to.20inspect.20attributes.3F

[Moritz Doll]

this is probably the change that was referenced in to_additive. I think for norm_cast I can adapt what was done for simp, but in general this is really stupid that we have to write very different code depending on the attribute for copying it in to_additive

[Mario Carneiro]

The attribute delaborator setup I mentioned (which I haven't had much time to work on) was only intended for #print, not for to_additive. I think for to_additive you need a way for attributes to say "I am reapplicable" with a method to copy the attribute from one declaration to another. You might be able to do that using the attribute delaborator to get Syntax and then applying that syntax as an attribute, but that sounds super hacky and would fail in many cases if the appropriate attribute parser doesn't exist.

[Moritz Doll]

mathlib4#847 not really tested - I am waiting for Kevin to give me a #mwe

[Kevin Buzzard]

OK sorry for the delay; it was Saturday evening and I was doing IRL stuff. Here's some mathlib3 code (which is easier to write because I can #print):

import tactic

@[simp, to_additive bargroup]
lemma foogroup (G : Type) [group G] : G = fin 37 := sorry

-- bargroup gets simp
--#print bargroup

--NB `@[to_additive bargroup, simp]` doesn't give bargroup `simp`.

@[norm_cast, to_additive barcoe]
lemma foocoe : ((1 : ℕ) : with_one ℕ) = 1 := sorry

-- barcoe gets norm_cast
-- #print barcoe

--NB `@[to_additive barcoe, norm_cast]` doesn't give barcoe `norm_cast`

-- In Lean 4 there is also the new `coe` attribute, which we also
-- typically want passed on to additivised declarations.

[Kevin Buzzard]

Honestly this would be so much easier if I could just see whether a given declaration had the norm_cast attribute :-/ norm_cast is good at solving things. Basically I'm having to do a lot of work to find an example which proves to me beyond all doubt that it's not there, and what I want to do is just to write a random dumb thing and then simply look.

[Kevin Buzzard]

OK here it is finally @Moritz Doll . Sorry for the delay:

import Mathlib.Order.WithBot

/-

# `simp` plays well with `to_additive`

(as long as it goes before `to_additive`)
-/
@[simp, to_additive bargroup]
theorem foogroup (G : Type) [Group G] : G = Fin 37 := sorry

example (G : Type) [AddGroup G] : G = Fin 37 := by simp? -- works

-- NB @[to_additive bargroup, simp] doesn't attach `simp` to the additivised
-- attribute


universe u

variable {α : Type u}

@[to_additive]
def WithOne (α) :=
  Option α

namespace WithOne

instance [Repr α] : Repr (WithZero α) :=
  ⟨fun o _ =>
    match o with
    | none => "0"
    | some a => "↑" ++ repr a⟩

@[to_additive]
instance [Repr α] : Repr (WithOne α) :=
  ⟨fun o _ =>
    match o with
    | none => "1"
    | some a => "↑" ++ repr a⟩

@[to_additive]
instance : One (WithOne α) :=
  ⟨none⟩

@[to_additive]
instance [Inv α] : Inv (WithOne α) :=
  ⟨fun a => Option.map Inv.inv a⟩

  /-

  ## `coe` doesn't play well with `to_additive`

  -/


-- `@[to_additive, coe]` doesn't work either
@[coe, to_additive]
def coe : α → WithOne α :=
  Option.some

@[to_additive]
instance : CoeTC α (WithOne α) :=
  ⟨coe⟩

example (a : α) : (a : WithOne α) = a := by
  sorry -- ⊢ ↑a = ↑a

-- additivised coercion doesn't seem to get `coe` attribute
example (a : α) : (a : WithZero α) = a := by
  sorry -- ⊢ WithZero.coe a = WithZero.coe a

attribute [coe] WithZero.coe -- add it manually

-- now it's there
example (a : α) : (a : WithZero α) = a := by
  sorry -- ⊢ ↑a = ↑a

/-

## `norm_cast` also doesn't play well with `to_additive`

-/

@[norm_cast, to_additive]
theorem coe_inv [Inv α] (a : α) : ((a⁻¹ : α) : WithOne α) = (↑a)⁻¹ :=
  rfl

example [Inv α] (a : α) : (a : WithOne α)⁻¹ = 1 := by
  -- ⊢ (↑a)⁻¹ = 1
  norm_cast
  -- ⊢ ↑a⁻¹ = 1 (goal changed)
  sorry

example [Neg α] (a : α) : -(a : WithZero α) = 0 := by
  -- ⊢ -↑a = 0
  norm_cast
  -- ⊢ -↑a = 0 (goal didn't change)
  sorry

attribute [norm_cast] WithZero.coe_neg

example [Neg α] (a : α) : -(a : WithZero α) = 0 := by
  -- ⊢ -↑a = 0
  norm_cast
  -- ⊢ ↑(-a) = 0
  sorry

[Kevin Buzzard]

As an unintended consequence I just noticed that the glyphs displayed on my computer for a in code and a in commented code are completely different (the former looks like a g reflected in the x-axis, the latter is a circle with a serif)

[Richard Osborn]

Kevin Buzzard said:

As an unintended consequence I just noticed that the glyphs displayed on my computer for a in code and a in commented code are completely different (the former looks like a g reflected in the x-axis, the latter is a circle with a serif)

That has to do with the fact that italicized 'a's are often written in the single-storey manner as opposed to the double-storey 'a'.

[Mario Carneiro]

Kevin Buzzard said:

Honestly this would be so much easier if I could just see whether a given declaration had the norm_cast attribute :-/ norm_cast is good at solving things. Basically I'm having to do a lot of work to find an example which proves to me beyond all doubt that it's not there, and what I want to do is just to write a random dumb thing and then simply look.

Assuming you are okay with a solution tailored to norm_cast:

import Mathlib.Tactic.NormCast

@[norm_cast] theorem foo : Int.ofNat 1 = 1 := rfl

open Lean Std.Tactic.NormCast
def isNormCastLemma (env : Environment) (decl : Name) : Bool :=
  (normCastExt.up.getState env).isLemma (.decl decl) ||
  (normCastExt.down.getState env).isLemma (.decl decl) ||
  (normCastExt.squash.getState env).isLemma (.decl decl) ||
  (pushCastExt.getState env).isLemma (.decl decl)

#eval show MetaM _ from return isNormCastLemma (← getEnv) ``foo -- true
#eval show MetaM _ from return isNormCastLemma (← getEnv) ``Nat -- false

[Kevin Buzzard]

It did occur to me after whining in #lean4 about not being able to see which attributes were attached to which declarations, that in fact in some sense the opposite is true in Lean 3 -- given half a chance I would whine that sometimes #print gives you half a page worth of attributes most of which I've never heard of and didn't want to see at all. When e.g. teaching, the kind of attributes I want to show to students are stuff like @[simp] and when debugging it's nice to see @[norm_cast] and now @[coe] but actually I'm now wondering whether in reality there's just a short list of attributes which I personally would like to be able to check up on. However for other people there might be a totally different list.

Regardless of all that, thanks! Indeed it's an easier way of checking that neither @[norm_cast, to_additive] nor @[to_additive, norm_cast] attach @[norm_cast] to the additivised declaration.