Zulip Chat Archive

Stream: general

Topic: confused


view this post on Zulip Thorsten Altenkirch (Feb 17 2021 at 15:10):

Think I have used variables in proofs before but today nothing works. What is wrong:

variable P : Prop

variable p : P

example : P := p

example : P :=
begin
  exact p,
end

I have boiled it down. Why does it say unknown identifier here?

view this post on Zulip Heather Macbeth (Feb 17 2021 at 15:14):

include p
example : P :=
begin
  exact p,
end

view this post on Zulip Heather Macbeth (Feb 17 2021 at 15:15):

If I understand correctly, by default Lean only brings into tactic mode the variables which appear in the hypotheses or conclusion.

view this post on Zulip Johan Commelin (Feb 17 2021 at 15:16):

For completeness: omit is the evil twin of include (-;

view this post on Zulip Thorsten Altenkirch (Feb 17 2021 at 15:16):

Thank you. Actually I have used this before and forgot about it... :-( This just drove me mad.

view this post on Zulip Johan Commelin (Feb 17 2021 at 15:18):

Ooh, just run omit mad to unmad yourself again :rofl:

view this post on Zulip Jeremy Avigad (Feb 17 2021 at 18:41):

The reason that Lean makes you include p explicitly is that a tactic block is really a metaprogram, there is no way for the parse to figure out what p really means. You can have tactics that add things to the context, delete things from the context, and rename things in the context. So Lean doesn't even try to guess what you want to include (even though with exact p is seems pretty obvious).

view this post on Zulip Thorsten Altenkirch (Feb 18 2021 at 10:31):

I noticed that once I am including a variable type inference fails because I suppose it also tries to use the new assumptions. Basically I only wanted to use variables as a replacement for a proof I don't want to do in the moment - I guess I better use sorry in this case?


Last updated: May 10 2021 at 17:39 UTC