confused

Stream: general

[Thorsten Altenkirch]

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?

[Heather Macbeth]

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

[Heather Macbeth]

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

[Johan Commelin]

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

[Thorsten Altenkirch]

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

[Johan Commelin]

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

[Jeremy Avigad]

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

[Thorsten Altenkirch]

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?