CODEWITHSUNDEEP
coqcoq-tactic
Fusen
Fusen

Reputation: 351

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?

Upvotes: 1

Views: 207

Answers (2)

Fusen
Fusen

Reputation: 351

Thank you for the answer. However,

Proof.
  intros. lia.

gives:

Error: Tactic failure:  Cannot find witness.

Is there a way to proceed?

Upvotes: 0

perthmad
perthmad

Reputation: 291

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.

Upvotes: 4

Related Questions