ancestor attribute

Stream: general

[Chris Hughes]

I'm trying to remove the unnecessary axioms for a group, ring etc. I'm seeing the ancestor attribute everywhere. What does it do, and how should I use it?

[Mario Carneiro]

it records the content of the extends clause of an old_structure_cmd for posterity

[Kevin Buzzard]

There is no more old structure command?

[Johan Commelin]

@Mario Carneiro By now, we could hack lean to do this for us, right?

[Mario Carneiro]

sure

[Johan Commelin]

Kevin Buzzard said:

There is no more old structure command?

There is... we're just logging what it does. For tactics.

[Chris Hughes]

If I'm changing the attributes, then for example monoid will be an ancestor of comm_monoid, but will have some extra axioms. So should ancestors that don't come from extends be marked as ancestors?

[Mario Carneiro]

no

[Chris Hughes]

Will I break all the tactics?

[Mario Carneiro]

I don't think so

[Kevin Buzzard]

What we really want here is a way of inserting into the constructor a way of saying "I'm making a group and the user supplied only some of the fields, so make the rest using this construction" rather than redefining the type

[Mario Carneiro]

in any case, the main consumer is to_additive and so you will know right away if it breaks

[Mario Carneiro]

this exists, it is called auto params

[Kevin Buzzard]

It doesn't exist

[Kevin Buzzard]

Let's take comm_group as an example

[Kevin Buzzard]

It probably extends group, but now you don't want to ask for mul_one and one_mul, however because it's extending group there's no way of retrofitting the autoparam

[Kevin Buzzard]

What we want is the ability not only to retrofit but also to ensure that when a hole command is used that we don't even show the autoparamed fields

[Mario Carneiro]

I know, I thought Chris already had a PR that does this

[Mario Carneiro]

you don't have to convince me that this is a good idea. Ideally this would get some lean support but as it is you just have to make a separate structure with an instance

[Mario Carneiro]

I will certainly grant that autoparams only solve some of the issues, and there are a lot more elaborate mechanisms I would like than what autoparams will give you. For example, defining a complete lattice where you only give the Sup, or only give the Inf, or only give the le

[Mario Carneiro]

or a group with left inverse and left unit, or right inverse and right unit

[Mario Carneiro]

It would be (relatively) easy to write a tactic that gets all these fields and has a store of constructor candidates containing a subset of all the fields and constructing the rest, and applies the first one where the input subset matches

[Mario Carneiro]

but since structure literals are implemented in C++ inextensibly it's tricky to do something like this

[Mario Carneiro]

and it would be nice as a library author to be able to provide all these constructor candidates

[Mario Carneiro]

right now they are these terrible mk' theorems with 14 hypotheses and no syntax support

[Kevin Buzzard]

Right, it would be lovely to see the back of those. It's embarrassing showing undergraduates the official definition of a comm_group in Lean but at least syntax support would help

[Mario Carneiro]

Kevin Buzzard said:

It probably extends group, but now you don't want to ask for mul_one and one_mul, however because it's extending group there's no way of retrofitting the autoparam

Actually you can retrofit autoparams. You just add the field in the child structure a second time with the same name and a default definition

[Kevin Buzzard]

Ha! Does this really work? With old structure command on?

[Mario Carneiro]

yeah, I think it is used in monad for example

[Johan Commelin]

@Chris Hughes Are you aware of this :up:

[Mario Carneiro]

class monad (m : Type u → Type v) extends applicative m, has_bind m : Type (max (u+1) v) :=
(map := λ α β f x, x >>= pure ∘ f)
(seq := λ α β f x, f >>= (<$> x))

[Gabriel Ebner]

These are default values, not auto params.

[Mario Carneiro]

both map and seq are coming from superclasses

[Mario Carneiro]

true, I think I mean opt param not auto param

[Gabriel Ebner]

And the fact that you can declare the default values afterwards requires workarounds which then cause lean#197. (EDIT: wrong issue number, thanks @Scott Morrison)

[Mario Carneiro]

Oh, I had no idea that was related

[Mario Carneiro]

have you diagnosed that issue?

[Gabriel Ebner]

Yes, it goes as follows: since default values may be declared at any point, we can't elaborate the fields from left to right. Instead, they are elaborated in some sort of dependency order: a field may only be elaborated when its type no longer contains any metavariables. In order to reduce the metavariables (this is crucial for new-style structures), projections are reduced. And this is why typeclass notation vanishes.

[Scott Morrison]

Oh, this sounds like it could also be related to lean#197.

[Mario Carneiro]

This is not at all how I expected opt params to be handled

[Mario Carneiro]

Why not eagerly remove auto_param and opt_param markers from the types first (and store them in an internal data structure)? They aren't supposed to be part of the type system proper, they are just annotations that live in expr because everything does

[Gabriel Ebner]

Oh, they are stored in an internal data structure. (Check out #print prefix monad.map)

[Gabriel Ebner]

To be clear, default values for structures are stored as separate declations. auto params are not, and optional arguments of definitions are not either.

[Mario Carneiro]

Here's an idea: always elaborate elements of a structure in left to right order of use in the literal

[Mario Carneiro]

no this is not backward compatible, but it is simple and easy to reason about

[Gabriel Ebner]

When should default values and auto param fields be elaborated?

[Mario Carneiro]

default values don't need to be elaborated, auto params go at the end

[Mario Carneiro]

I don't think it would be a good idea to have an invisible auto param providing data that is later referenced by a user-provided dependent argument

[Gabriel Ebner]

default values don't need to be elaborated

I'm not sure if that's how it's implemented.

[Mario Carneiro]

I mean you already have an elaborated expr corresponding to the default value. You just need to substitute the values of the other fields in it

[Mario Carneiro]

but it can be used by later fields, so its effective elaboration order would be just before first use in a dependent arg

[Gabriel Ebner]

I had something like this implemented already (elaborating fields left-to-right), and it choked on default arguments in monad. Let me see again what's going wrong.

[Mario Carneiro]

In particular that means that if you have a monad instance with map_comp and map := x >>= pure ∘ f then you can't write map_comp := ... before pure := ... and bind := ... unless you have also provided map := ...

[Kevin Buzzard]

Mario Carneiro said:

true, I think I mean opt param not auto param

in which case, so did I

[Gabriel Ebner]

lean#282