shadowing

Stream: new members

[abaaba]

constants (x: nat)
variables (y: nat)
section testSection
  variable (y: Type)
  #print y
end testSection

throws error says y has already been declared; but

constants (x: nat)
variables (y: nat)
section testSection
  variable (x: Type)
  #print x
end testSection

is fine, and x is shadowed.
Why?

[abaaba]

Moreover, I don't understand why we need two different keywords; why not just use variables?

[Kyle Miller]

constants defines new axioms, which are like definitions or theorems but have no definition. variables introduces arguments that Lean will automatically add in a definition or theorem.

Unless you're studying new foundations for logic, you should avoid constants.

[abaaba]

Thanks for explanation. Then am I correct to say that (without considering constants keyword) Lean forbids variable shadowing?

[Kyle Miller]

Lean prevents you from re-declaring variables, yes. You can change properties of variables, though, like this:

variables (z:nat)
section
variables {z} -- now z is implicit

end

and this change is scoped to the section.

[Kyle Miller]

I think a reason for this restriction is that it's unclear how shadowed variables would interact with dependent types. For example, let's say you have

variables {α : Type*} (l : list α)

and then shadow α. Would l still be in the variables list?

[abaaba]

makes sense for me to have variable shadowing disabled too . Wondering why shadowing of hypothesis is allowed in prove mode though ..

[Kyle Miller]

It's usually a mistake accidentally reusing a name for variables, since the point of the feature is to let you carefully maintain what arguments will appear in the following definitions and theorems. But Lean's ok with you shadowing lexical bindings:

def foo (x x : ℕ) : ℕ := x
def foo' : ℕ → ℕ → ℕ := λ x x, x

The hypotheses in tactic mode are similar.

[abaaba]

sorry I'm not sure where is the shadowing in your example, I was referring to in tactic mode, two different hypothesis, both named 'h' can appear simutaneously though ...

[Kyle Miller]

The shadowing is that x appears as an argument twice, so only the second one can be referred to.

[Kyle Miller]

This is in principle the same as what's going on in tactic mode.

[abaaba]

ooh i see ....

[abaaba]

(deleted)

[Kyle Miller]

This shadowing's allowed too:

variables (x : ℕ)
def foo : ℕ := x
def foo' (x : ℤ) : ℤ := x

In the first example, the definition triggers including x as an argument. The second, since it provides its own x, does not.

[abaaba]

Just curious, is the old hypothesis lost in this form?

[Kyle Miller]

What do you mean? Which thing are you referring to as the hypothesis?

[Kyle Miller]

#check foo
-- foo : ℕ → ℕ
#check foo'
-- foo' : ℤ → ℤ

[abaaba]

sorry, I mean is the old declaration inaccessible in the inner scope where second x is declared

[Kyle Miller]

Do you mean the double x argument example? According to this test

def foo' : ℕ → ℕ → ℕ := λ x x, begin   end

both x's are there, but I'm not sure how you refer to the first one, if it's possible at all.

[Kyle Miller]

It seems like it should be possible in some way, since I think(?) that Lean uses de Bruijn encoding, meaning variables numerically refer to the nth binding back.

[Kyle Miller]

This is one way:

def foo' : ℕ → ℕ → ℕ := λ x x, begin dedup, exact x end

[Kyle Miller]

A test to see it works:

#eval foo' 1 2
-- 1

[abaaba]

Indeed. Thanks!