Error "unknown identifier 'hp'" in chapter 3 "Propositions and Proofs" when using `variable (hp: p)`

[MichaelJFishman]

Description

Lean gives the error "unknown identifier 'hp'" when I put this example code into an otherwise empty file:

variable {p q : Prop}
variable (hp : p)

theorem t1 : q → p := fun (hq : q) => hp

Edit: Lean release v4.11.0 made it so that variables are not recognized in theorems unless we use include var0 var1.... The following snippet works:

variable {p q : Prop}
variable (hp : p)
include hp

theorem t1 : q → p := fun (hq : q) => hp

Possible solution

The code will type check if I change hp: p to an axiom:

variable {p q : Prop}
axiom hp: p

theorem t1 : q → p := fun (hq : q) => hp

However, #print t1 gives me

∀ {p q : Prop}, q → p := fun {p q} hq => hp

not

∀ p q : Prop, p → q → p

which is what the book states the type should be.

Other things I tried that didn't type check

I tried applying one, the other, or both of the following:

1. Using curly braces variable {hp : p} to make hp get used implicitly.
2. Changing t1 to t1 : p → q → p.

With both applied:

variable {p q : Prop}
variable {hp : p}

theorem t1 : p → q → p := fun (hq : q) => hp

Environment

Lean (version 4.12.0, x86_64-unknown-linux-gnu, commit dc2533473114, Release)

Edit: Changed #check t1 to #print t1. Edit 2: Added link to book section

[Dante3085]

I just created an Issue on the Lean 4 Repo that is I think relevant to you'r Issue: Variables not visible inside calc statement. Someone directed me to the release notes for 4.11.0 which state that the mechanism for variable inclusion has changed. Among other things: variables are only available to the proof if they have been mentioned in the theorem header, which is I think the reason why I haven't run into problems sooner. Many examples mention variables in the header.

[MichaelJFishman]

@Dante3085 Thanks! I think this is the same issue.

I can get the variables recognized by using include var0 var1...

variable {p q : Prop}
variable (hp : p)
include hp

theorem t1 : q → p := fun (hq : q) => hp

[nazar01]

Same happens in chapter 4. Quantifiers and Equality in line theorem gex1 : ∃ x, g x x = x := ⟨0, hg⟩

Lean prints unknown identifier 'hg', and adding include hg helps

[eric-wieser]

This has come up on Zulip a few times:

• #new members > lean calculations @ 💬
• #new members > variable visibility in `theorem` vs `def`(book example) @ 💬
• #new members > A basic question about calc without tactics @ 💬

Indeed, the examples need updating.