Stream: Coq users

Topic: Proof by contradiction

Rafael Garcia Leiva (Aug 03 2020 at 11:38):

Hi,

I have the hypothesis

H : N s = 0

and I want to prove the following

______________________________________(1/2)
~ (exists t : nat, R s t /\ t < s)

My idea was to assume that 't' exists and reach a contradiction by showing that in that case N s should be less than 0. Which tactic should I use?

A link to a document with examples of proofs by contradiction in Coq would be also very helpful.

Many thanks in advance.

Théo Winterhalter (Aug 03 2020 at 11:45):

The way negation is constructed in Coq is by saying ~ A := A -> False. So to show your goal you can begin by introducing some hypothesis of type exists t : nat, R s t /\ t < s using intro h for instance.

Karl Palmskog (Aug 03 2020 at 11:47):

this may be useful to understand the default Coq behavior for contradiction: https://existentialtype.wordpress.com/2017/03/04/a-proof-by-contradiction-is-not-a-proof-that-derives-a-contradiction/

Last updated: Sep 28 2023 at 11:01 UTC