# First steps problem: simple interval overlap proof

Hi all,

I am learning how to use Coq for some simple inequality problems and want to prove that this interval overlap check is correct. I have one step marked with `admit` below that seems really odd to me. In my proof window I see that I need to prove `y1 <= x1` which should not be required… The `intuition` tactic might be hiding a lot of important details but I could not find a better way forward.

Could somebody point me in the right direction, please?

``````Require Import ZArith.

Open Scope Z_scope.

Lemma IntervalIntersection (x1 x2 y1 y2: Z):
(* Two intervals [x1, x2] and [y1, y2] ... *)
(x1 <= x2) /\ (y1 <= y2) /\

(* ... overlap somewhere. *)
(y1 <= x2) /\ (x1 <= y2)

(* Since they overlap, there must be a value c that is element of the intersection. *)
<-> exists (c: Z),
(x1 <= c <= x2) /\ (y1 <= c <= y2).
Proof.
split.
- intro.
eexists.
intuition.
- intro.
destruct H.
intuition.
Qed.

Close Scope Z_scope.
``````

Hi,

With `eexists`, you created an “existential variable” for `c`, i.e. a
“hole” (displayed as `?c`) in the proof term that needs to be filled
later. The `intuition` tactic tries to instantiate this variable.
Unfortunately, it picked the wrong value for `c`!

You can replicate this behaviour with something like

``````Proof.
split.
-  intros (H1&H2&H3&H4).
eexists.
repeat split; eauto.
- (* ... *)
``````

The first goal after `repeat split` is `x1 <= ?c` (where `?c` is a name
for the existential variable). This goal, and the goal after the next
goal, is discharged by `eauto` by instantiating `?c` with `x2` and
applying `H1`. After that, only two goals remain:

1. `y2 <= x2`. This can’t be solved.
2. `y2 <= y2`. This is solved by `intuition`.

With other words, the problem is that you have to be “creative” because
Coq can’t guess the right witness for `c`. For example, something like
`exists (x1 + (x2 - y1) / 2).` might work, but I am not familiar with Z
arithmetic.

I see!

There are two possible solutions for `c`: `x1 <= c <= y2` or `y1 <= c <= x2`. Edit: That was wrong of course…

I thought also that it might be possible to construct a proof where I pose that there exists no `c` at all and try to get to a contradiction somehow. But I don’t know how to turn `exists (c: Z)` into `there is no (c: Z) such that etc.`. Do you know how to do that?

I think the first question is how would you do it on paper?
Then how could you turn this paper proof into something acceptable by the logic of Coq.
Coq being based on constructive logic, proofs by contradiction are usually not a good idea, since they might not be accepted by Coq.
In the present case, I would consider distinguishing two cases: either `x1 < y1` or `y1 <= x1`.
The corresponding statement in the standard library is:

``````Z_lt_le_dec : forall x y : Z, {x < y} + {y <= x}
``````

An alternative being to work directly with witness `c` to be `Z.max x1 y1`.

Ok. I will try your suggestions and get back when I have come up with something. I didn’t know that proof by contradiction is not recommended in Coq. This would be my first approach in this situation.

It should be `Z.max x1 y1`. The following proof works:

``````Require Import ZArith.
Require Import Lia.

Open Scope Z_scope.

Lemma IntervalIntersection (x1 x2 y1 y2: Z):
(x1 <= x2) /\ (y1 <= y2) /\
(y1 <= x2) /\ (x1 <= y2)
<-> exists (c: Z),
(x1 <= c <= x2) /\ (y1 <= c <= y2).
Proof.
split.
- intros.
exists (Z.max x1 y1).
lia.
- intro.
destruct H.
intuition.
Qed.
``````

This proof uses the `lia` tactic, which is a very powerful tactic when
it comes to arithmetic. `lia` also knows about `Z.max`.

Yes, I also found it in the meantime but couldn’t post it here yet. This is so cool! Thank you both for your support Proving negated statements “by contradiction” is perfectly constructive; we don’t even call that “proof by contradiction”, but classical mathematicians typically don’t make a distinction.
It’s just proof by contradiction of positive statements that doesn’t work, unless you add classical axioms with the needed care.
My point was (without entering details) to indicate that “trying to prove `exists c, F` by means of assuming `~(exists c, F)` and deriving a contradiction” (as suggested by @fabric-and-ink) is a priori not a good idea.
It is an instance of `~ ~ P -> P` (for a positive `P` here) which in general would require classical logic (as in `Logic.Classical_Prop`).