Stream: Coq users

Topic: A simple Prop proof


view this post on Zulip 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

view this post on Zulip Li-yao (Jun 13 2022 at 07:22):

Counterexample: let p and q be True.

view this post on Zulip Julin S (Jun 13 2022 at 07:27):

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

view this post on Zulip Paolo Giarrusso (Jun 13 2022 at 07:58):

This theorem is false, even in classical logic.

view this post on Zulip 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.

view this post on Zulip 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: Feb 04 2023 at 21:02 UTC