## Stream: Coq users

### Topic: A simple Prop proof

#### Julin Shaji (Jun 13 2022 at 07:01):

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

#### Li-yao (Jun 13 2022 at 07:22):

Counterexample: let `p` and `q` be `True`.

#### Julin Shaji (Jun 13 2022 at 07:27):

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

#### Paolo Giarrusso (Jun 13 2022 at 07:58):

This theorem is false, even in classical logic.

#### Paolo Giarrusso (Jun 13 2022 at 08:02):

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

#### Pierre Castéran (Jun 13 2022 at 08:24):

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: Oct 03 2023 at 02:34 UTC