Stream: Coq users

Topic: A simple Prop proof

Julin S (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 S (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 pas 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 13 2024 at 01:02 UTC