Search code examples
coqcoq-tactic

Coq proving addition inequality

I am a beginner and trying to prove this lemma:

Lemma test:  forall n m p q : nat,
    n <= p \/ m <= q -> n + m <= p + q.

I tried

From Coq Require Export Lia.

Lemma test:  forall n m p q : nat,
        n <= p \/ m <= q -> n + m <= p + q
Proof.
    intros; omega.

and Lia, but it is not working. How could I proceed?

Solution

  • You probably meant

    Lemma test:  forall n m p q : nat,
    n <= p /\ m <= q -> n + m <= p + q.

    with /\ (logical and) rather than \/ (logical or) because your theorem does not hold otherwise. As a counterexample, pick n = p = q = 0 and m = 1.

    When fixed that way, lia finds the proof automatically.

    Also, note it is more idiomatic in Coq to currify types, that is replacing conjunction on the left of an arrow with an arrow. This would read

    Lemma test:  forall n m p q : nat,
    n <= p -> m <= q -> n + m <= p + q.

    which is equivalent.