Zulip Chat Archive

I'm not in mathlib mode, I'm in "write a Lean game using mathlib" mode and the fact that subset_trans is in the root namespace is really inconvenient. For projects which aren't mathlib, I can really see the appeal of the idea that all mathlib stuff should be in a Mathlib namespace. Even if this never happens, isn't it reasonable to put subset_trans in a Set namespace which I can not open?

Alternatively, can anyone tell me how I can make MySet.subset_trans and then write some other code which means that I can avoid the error

ambiguous, possible interpretations
  _root_.subset_trans hAS hST : A ⊆ T

  MySet.subset_trans hAS hST : A ⊆ T

i.e. is there any way I can "switch off" _root_.subset_trans whilst still importing Mathlib.Data.Set.Basic? If not then I am faced with what looks like an impossible problem.

Kevin Buzzard (Jul 18 2024 at 00:14):

Hmm, for some reason if I'm in the MySet namespace then this works, the MySet one gets priority. The problem is that I don't want to be in this namespace, I want to be in the MyFilter namespace for this specific proof, and Open MySet doesn't cut it.

Maybe the answer is that if I'm making a game then I have to make one namespace specific to that game and then I am not allowed to use any namespaces other than that one? I was planning on making several bespoke namespaces where I was putting copies of mathlib lemmas (when users prove a lemma I want to create the illusion that they're making that lemma themselves and it's that lemma which is being used later on, even if the lemma is already there, that's the root of the problem).

Kevin Buzzard (Jul 18 2024 at 00:18):

@Sébastien Gouëzel I remember you arguing that we didn't need a Mathlib namespace because if we're using Lean and doing mathematics then we should be using Mathlib, not making it all again. Making games is perhaps an exception to this rule.

Kevin Buzzard (Jul 18 2024 at 00:36):

Yeah this is now all working. The moral is that if Mathlib is not going to live in its own namespace then it's forcing me to live in my own namespace and furthermore it's forcing me to have only one namespace.

theorem subset_trans : 2 + 2 = 4 := rfl

namespace MyGame

namespace MyFirstNamespace

theorem subset_trans : 2 + 2 = 4 := rfl

end MyFirstNamespace

namespace MySecondNamespace

open MyFirstNamespace

example : 2 + 2 = 4 := by
  apply subset_trans -- ambiguous term

Kevin Buzzard (Jul 18 2024 at 00:37):

Different failure:

theorem subset_trans : 2 + 2 = 4 := rfl

namespace MyFirstNamespace

theorem subset_trans : 2 + 2 = 4 := rfl

end MyFirstNamespace

namespace MySecondNamespace

open MyFirstNamespace

example : 2 + 2 = 4 := by
  apply subset_trans -- ambiguous term

Kevin Buzzard (Jul 18 2024 at 00:38):

theorem subset_trans : 2 + 2 = 4 := rfl

namespace MyOnlyNamespace

theorem subset_trans : 2 + 2 = 4 := rfl

example : 2 + 2 = 4 := by
  apply subset_trans -- works, applies my version

end MyOnlyNamespace