Search code examples
coqcoq-tacticssreflect

Coq/SSReflect: standard way to case on (x < y) + (x == y) + (y < x)?

In vanilla Coq, I'd write

Require Import Coq.Arith.Arith.
Goal nat -> nat -> False.
  intros n m.
  destruct (lt_eq_lt_dec n m) as [[?|?]|?].

to get three goals, one for n < m, one for n = m, and one for m < n. In ssreflect, I'd start with

From Coq.ssr Require Import ssreflect ssrbool.
From mathcomp.ssreflect Require Import eqtype ssrnat.
Goal nat -> nat -> False.
  move => n m.

What's the standard/canonical way to divide this into three cases, for n < m, n == m, and m < n, in ssreflect?

Solution

  • You can use ltngtP:

    From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
Goal nat -> nat -> False.
  move => n m.
  case: (ltngtP n m) => [n_lt_m|m_lt_n|n_eq_m].

    In accordance with the ssreflect style, this lemma automatically simplifies comparison functions such as n < m, n == m, etc. in the goal.