If I have a goal like:

```
p, q : Prop
H : p -> q
=============
~ p
```

how can I do the proof?

I have `p`

as hypothesis. So `~p`

shouldn't be provable, right?

Or do we need law of excluded middle for that?

This is what I had been trying:

```
Goal
forall (p q:Prop), (p -> q) -> ~p.
Proof.
intros.
intro HH.
```

after this the goal had become:

```
p, q : Prop
H : p -> q
HH : p
============
False
```

Counterexample: let `p`

and `q`

be `True`

.

Is there a tactic to assign values to p and q?

This theorem is false, even in classical logic.

The confusion is likely here:

I have

`p`

as hypothesis. So ~p shouldn't be provable, right?

"Having `p`

as hypothesis" can mean either having `p : Prop`

or having `H : p`

— you only have the first, but might be thinking of the second? Not sure. But even if you did, you could only prove `~~p`

.

It would be better to replace "I have `p`

as hypothesis" with "I have declared the proposition `P`

" , which means "my context contains a declaration `P:Prop`

". If the context contains some declaration `p:P`

, one can say `p`

is an hypothesis assuming `P`

.

Last updated: Jun 18 2024 at 08:01 UTC