Zulip Chat Archive

Stream: new members

Topic: shadowing

abaaba (Oct 28 2021 at 06:18):

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.

abaaba (Oct 28 2021 at 06:21):

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

Kyle Miller (Oct 28 2021 at 06:24):

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 (Oct 28 2021 at 06:26):

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

Kyle Miller (Oct 28 2021 at 06:28):

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

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


and this change is scoped to the section.

Kyle Miller (Oct 28 2021 at 06:33):

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 (Oct 28 2021 at 06:34):

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

Kyle Miller (Oct 28 2021 at 06:37):

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 (Oct 28 2021 at 06:40):

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 (Oct 28 2021 at 06:40):

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

Kyle Miller (Oct 28 2021 at 06:41):

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

abaaba (Oct 28 2021 at 06:41):

ooh i see ....

abaaba (Oct 28 2021 at 06:42):


Kyle Miller (Oct 28 2021 at 06:42):

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 (Oct 28 2021 at 06:43):

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

Kyle Miller (Oct 28 2021 at 06:43):

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

Kyle Miller (Oct 28 2021 at 06:44):

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

abaaba (Oct 28 2021 at 06:44):

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

Kyle Miller (Oct 28 2021 at 06:46):

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 (Oct 28 2021 at 06:48):

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 (Oct 28 2021 at 06:49):

This is one way:

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

Kyle Miller (Oct 28 2021 at 06:50):

A test to see it works:

#eval foo' 1 2
-- 1

abaaba (Oct 28 2021 at 06:53):

Indeed. Thanks!

Last updated: Dec 20 2023 at 11:08 UTC