instance clash with Mathlib instance.

Stream: mathlib4

[Shreyas Srinivas]

Hi, I know why this is happening and I am looking for workarounds for the moment. Consider the following:

import DGAlgorithms.Models.Vector
import Mathlib.Combinatorics.SimpleGraph.Basic

structure Graph (α : Type) (n : Nat) where
  data : Vector α n
  adj_arr : Vector (Array <| Fin n) n
deriving Repr, BEq

The above is not an MWE. DGAlgorithms.Models.Vector contains a copy of the Vector from batteries#793 . This clashes with Mathlib.Data.Vector in the form of the error import Mathlib.Data.Vector failed, environment already contains 'Vector.instGetElemNatLt._cstage2' from DGAlgorithms.Models.Vector.Basic.

Question : Is there a mechanism for qualified imports to circumvent this?

Note : The Vector file copy is a temporary stand-in for what I hope will be Batteries.Data.Vector very soon. I just need it sooner.

[Ruben Van de Velde]

Yeah, that's what I was afraid of. I recommend making your changes inside mathlib and only when you think it's ready for batteries, to move it all at once

[Shreyas Srinivas]

I think in this particular case, a PR removing Mathlib.Data.Vector is better, because Mathlib Vectors are apparently not used anywhere in the rest of mathlib.

[Shreyas Srinivas]

I am not sure that it makes sense in this particular instance: One simply needs a migration PR which removes Mathlib.Data.Vector which is apparently unused inside Mathlib

[Ruben Van de Velde]

Last I checked, they were not used much, but still somewhat

[Ruben Van de Velde]

If Vector is unused now, you don't need a migration pr, you should just remove it preemptively

[Shreyas Srinivas]

It is not used anywhere : https://github.com/search?q=repo%3Aleanprover-community%2Fmathlib4%20Vector&type=code

[Ruben Van de Velde]

Just scrolling through that link, I already find

theorem card_vector [Fintype α] (n : ℕ) : Fintype.card (Vector α n) = Fintype.card α ^ n := by

[Shreyas Srinivas]

Correction, it is used in a couple of places.

[Ruben Van de Velde]

Thank you

[Shreyas Srinivas]

We made a lot of changes to the Vector API to keep it close to the Array API

[Shreyas Srinivas]

This would have certainly broken mathlib even if it was done inside mathlib

[Ruben Van de Velde]

Maybe in your branch, but it would not be merged into master

[Shreyas Srinivas]

That's true, but I am trying to explain why developing it in batteries made sense, other than the fact that the discussion happened entirely in the batteries stream. It's goal is to be efficient first and foremost, making use of the special array support in the compiler. In mathlib, getting something easy for proofs might have taken precedence.

[Shreyas Srinivas]

Anyway, what's my quickfix in the example above? I am keen on using the Vector API rather than re-inventing them again under a different name. Can I fix this by adding a namespace in my project's Vector files? More precisely what is lean's equivalent of haskell's import qualified Vector as V

[Shreyas Srinivas]

can this be fixed by renaming the namespace in Mathlib's Vector to, say, MathVector?

[Eric Wieser]

Why are you not getting an error that your Vector clashes with mathlib 's Vector?

[Shreyas Srinivas]

Module namespacing

[Shreyas Srinivas]

I haven't directly imported mathlib Vector

[Eric Wieser]

Shreyas Srinivas said:

Module namespacing

What do you mean by this?

[Shreyas Srinivas]

I haven't brought mathlib Vector into scope

[Eric Wieser]

Is your vector type called YourModule.Vector?

[Shreyas Srinivas]

No

[Eric Wieser]

Shreyas Srinivas said:

I haven't brought mathlib Vector into scope

If it's imported transitively then it's in scope

[Eric Wieser]

And if it's not imported transitively the error here doesn't make sense

[Shreyas Srinivas]

My phone is about to lose battery power. I will respond later

[Shreyas Srinivas]

If Mathlib Vector is in scope then I have no idea why this happens. The error says that the import of Mathlib.Data.Vector failed.

[Shreyas Srinivas]

The error happens before I use Vector though. At the import line

[Eric Wieser]

Yes, because you are importing two files which both define Vector

[Eric Wieser]

Or at least, I assume you are. I can't see your other file, so it's hard to say.

[Shreyas Srinivas]

It is identical to the vector folder in batteries#793

[Shreyas Srinivas]

I am waiting for that PR to merge so I want to be able to swap the current folders out without too much effort

[Eric Wieser]

You can't define _root_.Vector in two different files and import them at the same time

[Eric Wieser]

That PR should surely not be merged without a mathlib adaptation PR?

[Eric Wieser]

In which case, the solution for you is to work on the version of mathlib that you create in that mathlib PR

[Eric Wieser]

Or alternatively, put everything in a DG namespace in your local copy

[Shreyas Srinivas]

Good point. I will add a mathlib adaptation PR. Should the namespace be Mathlib?

[Eric Wieser]

I think deciding what to do with Vector in Mathlib is a subject for another thread

[Kim Morrison]

Maybe: in a non dependent PR, move Vector to Mathlib.Vector. that could be merged right away?

[Kim Morrison]

Then, in an adaptation PR (i.e. relying on the batteries branch), delete what has been upstreamed, and deprecate the rest.

[Shreyas Srinivas]

I learnt that there are one or two places where Mathlib's Vector API is used. It is very different from the Batteries Vector at this point

[Shreyas Srinivas]

It seems much simpler to just deprecate what's in mathlib