First steps problem: simple interval overlap proof

Using Coq
1

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.
    admit. (* what?! *)
  - intro.
    destruct H.
    intuition.
Qed.

Close Scope Z_scope.
2

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.
   admit. (* what?! *)
- (* ... *)

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.

3

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?

4

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.

5

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.

6

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.

7

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 :slight_smile:

8

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.
See also, for instance, soft question - Proof by contradiction in Constructive Mathematics - Mathematics Stack Exchange or Proofs by contradiction, versus contradiction proofs | Existential Type.

9

@Blaisorblade Sure! (and thanks for the pointers which provide the explanations I wanted to avoid entering to).

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).

1 Like