introducing an element in tactic mode

Stream: general

[Antoine Chambert-Loir]

I am presently trying to solve the exercises of chapter 4 in {Theorem proving in Lean} using tactics.

In the context

variables (α : Type) (p q : α → Prop)
variable a : α
variable r : Prop

the following

example : r → (∃ x : α, r) :=
    assume hr : r,
    show (∃ x : α, r), from exists.intro a hr

works as a charm, but I can't manage to prove the same example using tactics.

example : (∃ x : α, r) → r :=
begin
    intro h,
    existsi a, exact h,
end

fails miserably, with an “unknown identifier 'a'” error that I don't understand.
By the way, “#check a” returns the expected “a : α”.

What am I doing wrong ?

[Johan Commelin]

Put include a before your example

[Johan Commelin]

@Antoine Chambert-Loir Let me try to explain: Lean looks at the type that you write down, and uses that to determine which variables it should include into the statement. And in fact, it doesn't only look at the type, but also at the term that follows it, if you are in term-mode.
In tactic mode, it cannot do this (because, monad mumble mumble). Hence you need to help it a little bit.

[Johan Commelin]

This is my amateur explanation of what is going on.

[Antoine Chambert-Loir]

Thanks !
To try to understand a bit of this wizardry, what is the difference of status between this term a (that needs to be included) and the other variables introductions ?

[Patrick Massot]

The difference is that a doesn't appear in the statement.

[Patrick Massot]

Having it appearing in the proof is sufficient if you give a proof term, but not in a tactic proof.

[Johan Commelin]

@Antoine Chambert-Loir Lean doesn't automatically include all the variables into all the statements. It tries to be smart, and in 99% of the cases, that's the right thing.
In this way, you can put a group G in your variables together with x y z : G, and write down some lemma involving only x and y. Lean will figure out that it shouldn't include z in that statement. (If it didn't, then calling that lemma would require you to always supply a useless third argument.)

[Patrick Massot]

By the way, you can also avoid this difficulty by using copy-paste instead of variables, writing:

example (α : Type) (a : α) (r : Prop) : r → (∃ x : α, r) :=
begin
end

[Johan Commelin]

But at the moment that Lean is figuring out which variables to include, it can't look inside the tactic proof yet. Maybe this could be changed by making Lean smarter. But my understanding is that if you try that, you would break some computer science barrier of abstraction.

[Antoine Chambert-Loir]

I see it's the right behaviour to have. Thanks again.

[Patrick Massot]

Seriously, overuse of variable can already make statements hard to read (exactly in the same way as in some traditional texts, where you need to remember that in such and such chapter, $\mathbb{k}$ will always denote a ring with finite global dimension). If a variable doesn't even appear in the statement it's very likely it will cause confusion.

[Patrick Massot]

So include is pretty rarely used in big files.

[Kevin Buzzard]

In maths it's the same. "From now until the end of section 12, we assume that $p>2$."

[Patrick Massot]

My example was targeting a specific book with infamous standing notations.

[Kevin Buzzard]

My example was targetting every number theory paper written about mod p modular forms in the 1990s

[Kevin Buzzard]

The opening line "Let $p$ be an odd prime" was a very common story at the beginning of a section back in those days.

[Sebastian Ullrich]

Maybe this could be changed by making Lean smarter. But my understanding is that if you try that, you would break some computer science barrier of abstraction.

Basically, yes. The fundamental issue is that in a tactic script begin foo, apply a end, Lean has no idea whether a will be introduced by the tactic foo or will refer to an outside a.

[Mario Carneiro]

It could be fixed if the tactic state kept track of which variables are available in the section

[Mario Carneiro]

or if the tactic state appeared to have all variables in the section but they get trimmed down at the end

[Rob Lewis]

or if the tactic state appeared to have all variables in the section but they get trimmed down at the end

This sounds unpredictable. You could have a proof that doesn't depend on a variable h, and makes no reference to h, yet still breaks if h is changed.

[Sebastian Ullrich]

This can't be fixed at all during tactic execution because of parallel processing. The type of a lemma has to be determined before tactics are invoked.

[Mario Carneiro]

Alternatively, don't allow variable appearances in theorem proofs to count as includes, just use presence in defs and theorem statements since that's the main thread part

[Mario Carneiro]

I'm not even sure why it works in the first place

[Sebastian Ullrich]

I'm not even sure why it works in the first place

Names outside of tactic arguments are resolved during parsing. This will actually change in Lean 4, so you should get your desired behavior.