Stream: Coq users

Topic: Proof by contradiction

view this post on Zulip Rafael Garcia Leiva (Aug 03 2020 at 11:38):


I have the hypothesis

H : N s = 0

and I want to prove the following

~ (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.

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

view this post on Zulip Karl Palmskog (Aug 03 2020 at 11:47):

this may be useful to understand the default Coq behavior for contradiction:

Last updated: Jan 29 2023 at 01:02 UTC