weird interaction with namespace, parameter, and tactic

Stream: new members

[Gun Pinyo]

Hi there, there is a weird interaction between parameter, namespace, and tactic.

def foo : bool → Type := λ _, unit
namespace bar
section
  parameter b : bool
  include b
  def foo' := foo b
  #check foo' -- Type
  example : Type := by exact foo' -- error here
end

I have an error message saying that foo' : bool → Type . I need to write foo' b to silence the error message.
This is weird because #check foo' saying that it has type Type. Could anyone explain to me why it happens like this?

There are other 2 ways to fix the error
1. remove by exact altogether
2. remove namespace bar
I suspect that it is will have anything to do with namespace and tactic.

[Kevin Buzzard]

Your parameter is included in everything in the section. Try checking foo' outside the section

[Kevin Buzzard]

You should end both the section and the namespace as well or you'll get unexpected errors

[Kevin Buzzard]

parameter means something like "every single thing here depends on exactly this parameter which will be inserted into every definition and lemma" or something. I don't think anyone uses it in practice

[Gun Pinyo]

Your parameter is included in everything in the section. Try checking foo' outside the section

Understand that foo' : bool → Type outside the section but the error arises inside the section, that's why I am confused.

You should end both the section and the namespace as well or you'll get unexpected errors

I have end at the buttom but forget to copy it to the post, sorry about that.

parameter means something like "every single thing here depends on exactly this parameter which will be inserted into every definition and lemma" or something. I don't think anyone uses it in practice

Well, I am using it to make Lean namespace looks a little bit more like Agda's parameterised module. Please note that the code I posted earlier is the simplified version of the actual problem I see on my bigger project.

Btw, does the error message that I got is the expected behaviour?

[Wojciech Nawrocki]

I really wish Lean had parametrised modules

[Kevin Buzzard]

I never use parameters and not many other people use them, so I don't really know how they work and apparently they don't work too well or other people would use them more. Note this before you experiment too much more with parameters :-)

Your definition of foo', because of the parameter and include, is
def foo' (b : bool) := foo b because of the parameter. In the section the parameter is active so the #check doesn't print it out -- the parameter is an input to every single function in the section and Lean is not going to ever tell you this. Outside the section you can see what's going on.

def foo : bool → Type := λ _, unit
namespace bar
section
  parameter b : bool
  include b
  def foo' := foo b
  #check foo' -- Type
  example : Type := by exact foo' -- error here
end
#check foo' -- bool → Type
end bar

[Gun Pinyo]

@Kevin Buzzard I understand that foo' : bool → Type outside the section. But inside the section, up to my understanding, every definition will silently insert the parameter in. But weirdly, it doesn't happen inside the tactic if it is under some namespace. Should I think this as a bug and should try to avoid using parameters?

[Jesse Michael Han]

I think it is indeed a bug, since inside the section and outside of tactic mode,

example : Type := foo'

works as intended (b is inserted as an argument).

[Mario Carneiro]

I don't know if it's a bug, but it is certainly abstraction leakage. Inside tactic mode it doesn't have a good grasp of what namespace and sections it's in, so it's hard to simulate parameters correctly

[Joe]

(deleted)

[Joe]

(deleted)