p p : P,

Stream: new members

[Philip B.]

Hi. I am playing the natural numbers game, Advanced proposition world, level 10. So far my proof is

intros h p,
by_cases p:P; by_cases q:Q,

in the goals pane, I see among other lines a line p p : P,. What does it mean?

[Yakov Pechersky]

You introduced two new terms into your tactic state with your first line intros h p, where p : P is a term p of type P.

[Philip B.]

@Yakov Pechersky I mean in that line why are there two small letters p instead of one?

[Yakov Pechersky]

Then, you added another term to your tactic state with the line by_cases p : P, which creates two subgoals. In each of the subgoals, there is a new term p : P. In the first subgoal, you will have a hypothesis that p is true, and in the other subgoal, that p is false.

[Yakov Pechersky]

The two ps you have, one from intros and one from by_cases are entirely distinct.

[Yakov Pechersky]

Is P : Prop?

[Philip B.]

@Yakov Pechersky yes

[Philip B.]

Yakov Pechersky said:

The two ps you have, one from intros and one from by_cases are entirely distinct.

I see

[Yakov Pechersky]

In Lean, if P : Prop, then if p1 : P and p2 : P, then p1 = p2, that is, P is a proposition, and p1 and p2 are proofs of that proposition. In Lean, proofs of the same proposition are equal -- called "proof irrelevance".

[Yakov Pechersky]

So you might want to do something like

intros h p_from_statement,
by_cases p : P,
by_cases q : Q,
[...]

[Kevin Buzzard]

Are you splitting on the case P is true/false, whilst simultaneously knowing that P is true? This doesn't seem sensible

[Philip B.]

@Kevin Buzzard after thinking some more, I understand that this was a bad idea

[Yakov Pechersky]

Crucially, in the second subgoal of by_cases p : P, you'll have a tactic state with p : ¬P. So that variable p will change from being of type P to type ¬P.

[Johan Commelin]

Philip B. said:

Yakov Pechersky I mean in that line why are there two small letters p instead of one?

Try changing intros h p to intros h blabla. Try the same thing with the p in by_cases p : P.