Instance management

Stream: Is there code for X?

[Winston Yin]

I'm editing a file that begins with variables {M : Type*} [some_instance1 M] [some_instance2 M]. I'd like to add some theorems which only need {M : Type*} [some_instance1 M] but not [some_instance2 M]. How do I do that within a section? If I write variables {M : Type*} [some_instance1 M], Lean complains that M has already been defined. I've been writing lemma my_lemma {M : Type*} [some_instance1 M] to get around that, but it gets repetitive.

[Eric Wieser]

Usually the solution is to change the file so that it doesn't begin like that, and instead begins

variables {M : Type*}

section inst1
variables [instance1 M]

...

end inst1

section inst2
variables [instance2 M]

...

end inst2

[Scott Morrison]

Obviously don't use a section for a single declaration, but besides that, now sections is no problem.

[Moritz Doll]

There are two variants for doing this, the one Eric suggested (which I think is way better) and the 'lots of variables' variant, i.e., declaring
variables {M M' : Type*} [some_instance1 M] [some_instance2 M']. For examples in mathlib see https://github.com/leanprover-community/mathlib/blob/master/src/analysis/seminorm.lean#L96 and https://github.com/leanprover-community/mathlib/blob/master/src/linear_algebra/bilinear_map.lean#L39

[Scott Morrison]

I don't like the lots of variables approach. I find reading files that do this pretty painful if you have to jump around the file to work out which number of primes corresponds to which structure... If anyone ever feels like doing tidying up PRs that instead use sections, I'd love to merge them. :-)

[Moritz Doll]

I agree that this is not good, I just wanted to mention that this approach works, too and if you edit files that use that approach already then you probably have to stick to it.

[Winston Yin]

Thanks for the suggestions. The thing is, I’m editing this behemoth of a file cont_mdiff, and the variables defined in the beginning just work so well for the rest of the file. Since I’m adding only 3 lemmas at the end, I think I’ll just write the variables in the lemmas.

[Yaël Dillies]

If you use less variables, I would rather put them at the beginning