Zulip Chat Archive

Stream: new members

Topic: p p : P,


view this post on Zulip Philip B. (Sep 14 2020 at 15:33):

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?

view this post on Zulip Yakov Pechersky (Sep 14 2020 at 15:35):

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.

view this post on Zulip Philip B. (Sep 14 2020 at 15:36):

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

view this post on Zulip Yakov Pechersky (Sep 14 2020 at 15:36):

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.

view this post on Zulip Yakov Pechersky (Sep 14 2020 at 15:37):

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

view this post on Zulip Yakov Pechersky (Sep 14 2020 at 15:37):

Is P : Prop?

view this post on Zulip Philip B. (Sep 14 2020 at 15:37):

@Yakov Pechersky yes

view this post on Zulip Philip B. (Sep 14 2020 at 15:38):

Yakov Pechersky said:

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

I see

view this post on Zulip Yakov Pechersky (Sep 14 2020 at 15:40):

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

view this post on Zulip Yakov Pechersky (Sep 14 2020 at 15:41):

So you might want to do something like

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

view this post on Zulip Kevin Buzzard (Sep 14 2020 at 15:45):

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

view this post on Zulip Philip B. (Sep 14 2020 at 15:46):

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

view this post on Zulip Yakov Pechersky (Sep 14 2020 at 15:49):

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.

view this post on Zulip Johan Commelin (Sep 14 2020 at 16:10):

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.


Last updated: May 08 2021 at 04:14 UTC