# Zulip Chat Archive

## Stream: new members

### Topic: p p : P,

#### 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?

#### 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`

.

#### 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?

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

#### Yakov Pechersky (Sep 14 2020 at 15:37):

The two `p`

s you have, one from `intros`

and one from `by_cases`

are entirely distinct.

#### Yakov Pechersky (Sep 14 2020 at 15:37):

Is `P : Prop`

?

#### Philip B. (Sep 14 2020 at 15:37):

@Yakov Pechersky yes

#### Philip B. (Sep 14 2020 at 15:38):

Yakov Pechersky said:

The two

`p`

s you have, one from`intros`

and one from`by_cases`

are entirely distinct.

I see

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

#### 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,
[...]
```

#### 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

#### Philip B. (Sep 14 2020 at 15:46):

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

#### 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`

.

#### 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