ancestor

Stream: general

[Sebastien Gouezel]

Can someone explain what the ancestor attribute is for? (It doesn't appear as an attribute in https://leanprover-community.github.io/mathlib_docs/attributes.html, and is only mentioned in to_additive there). For instance, I can see in field.lean

@[protect_proj, ancestor division_ring comm_ring]
class field (α : Type u) extends comm_ring α, has_inv α, nontrivial α :=
(mul_inv_cancel : ∀ {a : α}, a ≠ 0 → a * a⁻¹ = 1)
(inv_zero : (0 : α)⁻¹ = 0)

which mentions as ancestordivision_ring, but not has_inv or nontrivial, so I have a hard time guessing how it should be used in general.

[Mario Carneiro]

I think field's ancestry was changed

[Mario Carneiro]

it's supposed to list the contents of the extends clause, because this information is not preserved by old_structure_cmd structures

[Sebastien Gouezel]

ok, so in the case of field it should just be comm_ring has_inv nontrivial?

[Sebastien Gouezel]

And if you extend things with less params (for instance bar (a b) extends foo1 a, foo2 b), should it just be ancestor foo1 foo2 or is there some more trickery do be done?

[Patrick Massot]

I think this is used only by the subtype instance tactic which is maybe no longer used now everything is bundled.

[Mario Carneiro]

I think it is just ancestor foo1 foo2

[Mario Carneiro]

that said, you shouldn't be doing that in the first place

[Kevin Buzzard]

Sebastien Gouezel said:

And if you extend things with less params (for instance bar (a b) extends foo1 a, foo2 b), should it just be ancestor foo1 foo2 or is there some more trickery do be done?

Isn't this an antipattern?

[Sebastien Gouezel]

This is an antipattern for classes, as typeclass search will go crazy, but for normal structures it shouldn't be a problem.

[Yury G. Kudryashov]

ancestor is used by to_additive to automatically map to_* functions. I don't know who else uses this information.

[Yury G. Kudryashov]

In particular, I don't know if there is some code using @[ancestor] on field.

[Floris van Doorn]

Yury G. Kudryashov said:

ancestor is used by to_additive to automatically map to_* functions. I don't know who else uses this information.

Oh, I didn't know about the ancestor attribute. We could use this for the is_auto_generated definition to check which instances are auto-generated (which is useful for e.g. linters).

[Eric Wieser]

attr#ancestor and attr#to_additive now collectively document this i think