CODEWITHSUNDEEP
coqcoq-tacticcoqide
he11boy
he11boy

Reputation: 81

Discriminate goal in Coq

I have two conditions for nat numbers:

H:  a < b
H1: b < a

How to discriminate goal? Does exist any tactics for < ?

Upvotes: 1

Views: 325

Answers (2)

ejgallego
ejgallego

Reputation: 6852

For reference, doing a manual proof is not so difficult in this case:

From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Lemma foo a b (a_lt_b : a < b) : b < a -> False.
Proof. by rewrite ltnNge (ltnW a_lt_b). Qed.

Upvotes: 0

Donald Sebastian Leung
Donald Sebastian Leung

Reputation: 201

Use lia:

From Coq Require Import Lia.

Goal forall a b, a < b -> b < a -> False.
  lia.
Qed.

You can learn more about lia and other decision procedures for arithmetic here.

Upvotes: 2

Related Questions