out_param & add_torsor

Stream: general

[Yury G. Kudryashov]

I'm trying to make the G argument of add_torsor G P an out_param so that Lean will automatically find the tangent space for an affine space. Sometimes it works but sometimes it fails. E.g., I had to leave G as an explicit argument of vsub_set and it fails to deal with vector_span. @Gabriel Ebner Is it a bug or a feature?

[Gabriel Ebner]

#mwe / where does it fail?

[Yury G. Kudryashov]

The code in the branch fails at vsub_set_subset_vector_span in linear_algebra/affine_space.

[Yury G. Kudryashov]

With or without up arrow it fails to figure out that vector_span k s is a submodule k V, not submodule k ?.

[Yury G. Kudryashov]

If I remove variable (G) from here, then it fails on vsub_set_empty.

[Gabriel Ebner]

This is probably because while V is an out param, the type class parameter [add_comm_group V] is not an out param.

[Yury G. Kudryashov]

I added more out_params, now instance resolution in the LHS of vector_span_def fails. It says that _inst_4 is not defeq to what it's looking for. I don't understand why.

[Gabriel Ebner]

This is also unclear to me.

[Mario Carneiro]

It's because you declared it as an abbreviation

[Mario Carneiro]

if it's a class then it works fine

[Mario Carneiro]

In fact even @[class] abbreviation works

[Mario Carneiro]

#mwe

class bar (A : out_param Type*) (B : Type*) := mk

abbreviation foo (k : Type*) (A : out_param Type*) (B : Type*) :=
bar A B

variables (k : Type*) (A : out_param Type*) (B : Type*) [foo k A B]

#check (by apply_instance : foo k _ B) -- fails

[Mario Carneiro]

I think what's happening is that by declaring it an abbreviation for a class, lean reuses the instance cache for bar, which means it's searching for bar ? B when only foo k A B is in the context (it apparently doesn't unfold the hypotheses too)

[Yury G. Kudryashov]

Thank you for the explanation!

[Patrick Massot]

Do you think this will be enough to unblock you?

[Yury G. Kudryashov]

I'll try tonight.

[Yury G. Kudryashov]

I wonder if I'll have to duplicate all add_torsor instances as affine_space instances.

[Yury G. Kudryashov]

@Mario Carneiro I made it compile with notation. I tried @[class] abbreviation and it failed.

[Yury G. Kudryashov]

CI should build oleans in 10-20 minutes. If you can checkout https://github.com/leanprover-community/mathlib/tree/affine-out-param and make it build with class or @[class] abbreviation, this would be wonderful.

[Yury G. Kudryashov]

But I guess we can just use add_torsor everywhere.

[Yury G. Kudryashov]

I wish we had a way to make two names completely equivalent.

[Yury G. Kudryashov]

@Patrick Massot @Joseph Myers What do you think about using add_torsor directly?

[Mario Carneiro]

I suggest you don't use abbreviation (why are you using it here in the first place?). Shouldn't @[class] def be just as good?

[Yury G. Kudryashov]

@[class] def affine_space (V : out_param $ Type*) (P : Type*) [out_param $ add_comm_group V] :=
add_torsor V P

doesn't work

[Yury G. Kudryashov]

125:66: failed to synthesize type class instance for
k : Type u_1,
V : Type u_2,
P : Type u_3,
_inst_1 : ring k,
_inst_2 : add_comm_group V,
_inst_3 : module k V,
_inst_4 : affine_space V P,
s : set P
⊢ add_torsor V P

[Yury G. Kudryashov]

(at the definition of vector_span)

[Yury G. Kudryashov]

Linear algebra uses abbreviations to get automatic upgrades from semimodule to module.

[Yury G. Kudryashov]

I also tried

abbreviation affine_space (V : out_param Type*) (P : Type*) [out_param $ add_comm_group V] :=
add_torsor V P

and

abbreviation affine_space (V : out_param Type*) (P : Type*) [add_comm_group V] :=
add_torsor V P

[Mario Carneiro]

Just declare instances for what you want

[Mario Carneiro]

I don't think you should try to do "automatic upgrading" because the classes differ in what's an out_param

[Yury G. Kudryashov]

I don't want them to differ at all.

[Yury G. Kudryashov]

Should some combination of out_params work?

[Patrick Massot]

Yury G. Kudryashov said:

Patrick Massot Joseph Myers What do you think about using add_torsor directly?

Of course I prefer reading affine_space, but if the decision is between a nice name vs nice elaboration then I prefer nice elaboration of course.

[Yury G. Kudryashov]

I suggest using add_torsor for now, and reevaluate this decision after migration to Lean 4.

[Joseph Myers]

I based the use of abbreviation directly on how it's used for vector_space, to give a familiar name in that particular context. If abbreviation causes problems here, using add_torsor seems reasonable, but the module doc string would need some careful revisions, to say that affine spaces are represented using [module k V] [add_torsor V P] rather than defining affine_space, and to say why things are implemented that way. Likewise if Euclidean affine spaces need to use normed_add_torsor rather than euclidean_affine_space to get the benefit of out_param. (Making V implicit in the Euclidean context would mean the notation for angles becomes ∠ A B C, as in normal informal geometry, rather than the present ∠ V A B C.)

[Joseph Myers]

If add_torsor is used directly, it should still be possible to use affine_space as a namespace where appropriate. The documentation of mathlib naming conventions says very little about when to put things in a namespace and I don't think I've been very consistent about it for affine spaces. Some results for affine subspaces are in the affine_subspace namespace, some in the affine_space namespace. For results about affine independence I didn't put them in a namespace at all, since names involving affine_independent seem globally unambiguous enough.

[Patrick Massot]

The practical rule comes from the dot notation: put things in the namespace of the main assumption or ingredient.

[Joseph Myers]

That's why affine_subspace.direction has to be in that namespace, for example, and why weighted_vsub is in the finset namespace. It seems less obviously relevant for many of the lemmas, but maybe e.g. those with affine_independent as a hypothesis should actually be in a affine_independent namespace to allow use of dot notation there.

[Joseph Myers]

One other question occurs to me: does use of out_param for add_torsor have implications for the possibility of relating additive and multiplicative actions and torsors with to_additive in future?

[Yury G. Kudryashov]

In the same branch I'm removing add_action, add_torsor, and affine_space namespaces.

[Yury G. Kudryashov]

Because names use vadd/vsub anyway, so there are no name conflicts.

[Joseph Myers]

I think at least simplex (currently affine_space.simplex) could do with being in a namespace, there are lots of different concepts that get called a simplex so it seems questionable to claim _root_.simplex for this particular one. Likewise triangle.

[Yury G. Kudryashov]

Pushed angles without V