confused about nesting namespaces

Stream: lean4

[Paige Thomas]

If I have the following in one file

namespace Chapter2_


/--
  The type of formulas.
-/
inductive Formula_ : Type
  | false_ : Formula_
  | true_ : Formula_
  | atom_ : String → Formula_
  | not_ : Formula_ → Formula_
  | and_ : Formula_ → Formula_ → Formula_
  | or_ : Formula_ → Formula_ → Formula_
  | imp_ : Formula_ → Formula_ → Formula_
  | iff_ : Formula_ → Formula_ → Formula_
  deriving Inhabited, DecidableEq, Repr

and I import it into a file containing this

namespace Chapter2_


open Formula_

...code...

Can I make the code that follows open Formula_ belong to an additional nested namespace under Chapter2_ called Prop_ without making changes to that code? That is, make the code in the first file just in the namespace Chapter2_ and the code in the second file in the namespace Chapter2_.Prop_? I tried adding namespace Prop_ in various locations in the second file, but it seems to break the code that follows it. I think maybe I'm confused about how namespaces work. My thought was that everything under namespace blah essentially gets blah. prepended to it.

[Kyle Miller]

If you add namespace Prop_ anywhere after namespace Chapter2_, then the code that follows will be in the Chapter2_.Prop_ namespace.

You can use the #where command to see where you are

[Paige Thomas]

If I do this

namespace Chapter2_

namespace Prop_

open Formula_

and later on have

def Formula_.is_tautology
  (F : Formula_) :
  Prop :=
  ∀ (V : Valuation), satisfies V F

and then

def is_logical_consequence
  (P Q : Formula_) :
  Prop :=
  (P.imp_ Q).is_tautology

the last gives

invalid field 'is_tautology', the environment does not contain 'Chapter2_.Formula_.is_tautology'
  P.imp_ Q
has type
  Formula_

[Paige Thomas]

why does the last not see it as Chapter2_.Prop_.Formula_.is_tautology?

[Kyle Miller]

If you define Formula_.is_tautology inside this nested namespace, you've defined Chapter2_.Prop_.Formula_.is_tautology, but dot notation is looking in the namespace for Formula_, which is Chapter2_.Formula.

[Kyle Miller]

If you want to use dot notation, you'll have to define is_tautology in that namespace.

[Kyle Miller]

You should see that is_tautology (P.imp_ Q) is fine, since it'll find is_tautology in the current namespace.

[Paige Thomas]

I see. Thank you.

[Paige Thomas]

Hmm. It seems I need to do Formula_.is_tautology (P.imp_ Q).

[Kyle Miller]

Oh right, I forgot you defined it as that. Yes, that's expected.

[Kyle Miller]

@David Thrane Christiansen has a defmethod macro for being able to define functions meant to be used with dot notation from within another namespace. This would be convenient here! (code)

[Paige Thomas]

Oh? That would be nice!

[Kyle Miller]

That file I linked is self-contained, and you could drop it into your project.

[Paige Thomas]

Should I try to import the project?

[Paige Thomas]

I guess it seems a little odd to copy the file.

[Paige Thomas]

Is there a chance the macro might get moved into something like mathlib?

[Yaël Dillies]

Kyle Miller said:

David Thrane Christiansen has a defmethod macro for being able to define functions meant to be used with dot notation from within another namespace. This would be convenient here! (code)

Oh! That would have been great for @Hannah Scholz in #19760

[Kyle Miller]

Copying the file is what I'd do. Verso is a relatively large dependency for just this feature.

The risk is if Lean changes and it needs fixing, you wouldn't be able to just update the dependency. However, if you keep track of the source of the file, you can manually update it.

"Vendoring dependencies" is an age-old development method.

[Kyle Miller]

I'll mention that an alternative (and what mathlib does) is instead either (1) manage carefully which namespace you're in or (2) use _root_ like so to temporarily go back to the root namespace:

def _root_.Chapter2_.Formula_.is_tautology
  (F : Formula_) :
  Prop :=
  ∀ (V : Valuation), satisfies V F

[Paige Thomas]

Hmm. I'm not sure how to apply this here. There are two different definitions of is_tautology that both use the same definition of Formula_.

[Paige Thomas]

If I did that for both they would clash right?

[Paige Thomas]

The _root_ approach that is.

[Paige Thomas]

Would the macro work in that case?

[Paige Thomas]

That is, if I do def _root_.Chapter2_.Formula_.is_tautology in two different namespaces, will the definitions clash?

[Kyle Miller]

The macro is equivalent to this _root_ approach

[Kyle Miller]

Yes, they will clash.

[Paige Thomas]

I guess the only option is to drop the dot notation then?

[Paige Thomas]

If I have

namespace Chapter2_.Prop_

open Formula_

the open Formula_ somehow knows to use the definition of Formula_ from the Chapter2_ namespace and not try to find it in the Chapter2_.Prop_ namespace?

[Kyle Miller]

namespace Chapter2_.Prop_ makes all the names in Chapter2_ and Chapter2_.Prop_ available, so when you do open Formula_, it can resolve that Formula_ refers to Chapter2_.Formula_, and then makes the names in there available.

[Paige Thomas]

Oh. And I assume namespace Chapter2_.Prop_ is the same as

namespace Chapter2_
namespace Prop_

?

[Kyle Miller]

Yeah

[Paige Thomas]

Thank you!

[David Thrane Christiansen]

Yeah, that macro is there mostly to complain if the name before the dot doesn't resolve, and partly to help with maintenance when I move things around. It helped a lot with early iterative development, but in the long run I'd like to eliminate it.

[Edward van de Meent]

David Thrane Christiansen said:

... but in the long run I'd like to eliminate it.

Could you elaborate on why? it seems to me like this is a nice language feature to have?

[David Thrane Christiansen]

I think it's fine as an idiomatic language feature, but it doesn't make the Verso codebase easier to understand. It's been very helpful during rapid development, but the core of Verso is getting pretty stable, so I'd rather optimize for being less surprising, easier to maintain, and not so clever when possible. That said, this is not something I feel strongly about :)