Zulip Chat Archive

Stream: general

Topic: introducing an element in tactic mode


view this post on Zulip Antoine Chambert-Loir (Nov 15 2019 at 20:34):

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 ?

view this post on Zulip Johan Commelin (Nov 15 2019 at 20:35):

Put include a before your example

view this post on Zulip Johan Commelin (Nov 15 2019 at 20:41):

@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.

view this post on Zulip Johan Commelin (Nov 15 2019 at 20:41):

This is my amateur explanation of what is going on.

view this post on Zulip Antoine Chambert-Loir (Nov 15 2019 at 20:43):

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 ?

view this post on Zulip Patrick Massot (Nov 15 2019 at 20:44):

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

view this post on Zulip Patrick Massot (Nov 15 2019 at 20:44):

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

view this post on Zulip Johan Commelin (Nov 15 2019 at 20:48):

@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.)

view this post on Zulip Patrick Massot (Nov 15 2019 at 20:49):

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

view this post on Zulip Johan Commelin (Nov 15 2019 at 20:49):

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.

view this post on Zulip Antoine Chambert-Loir (Nov 15 2019 at 20:49):

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

view this post on Zulip Patrick Massot (Nov 15 2019 at 20:53):

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, k\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.

view this post on Zulip Patrick Massot (Nov 15 2019 at 20:53):

So include is pretty rarely used in big files.

view this post on Zulip Kevin Buzzard (Nov 15 2019 at 21:13):

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

view this post on Zulip Patrick Massot (Nov 15 2019 at 21:29):

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

view this post on Zulip Kevin Buzzard (Nov 15 2019 at 21:41):

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

view this post on Zulip Kevin Buzzard (Nov 15 2019 at 21:43):

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

view this post on Zulip Sebastian Ullrich (Nov 16 2019 at 09:07):

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.

view this post on Zulip Mario Carneiro (Nov 16 2019 at 09:08):

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

view this post on Zulip Mario Carneiro (Nov 16 2019 at 09:09):

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

view this post on Zulip Rob Lewis (Nov 16 2019 at 09:14):

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.

view this post on Zulip Sebastian Ullrich (Nov 16 2019 at 09:41):

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.

view this post on Zulip Mario Carneiro (Nov 16 2019 at 10:08):

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

view this post on Zulip Mario Carneiro (Nov 16 2019 at 10:09):

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

view this post on Zulip Sebastian Ullrich (Nov 16 2019 at 10:20):

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.


Last updated: May 08 2021 at 19:11 UTC