coq - Coq/SSReflect：(x < y) + (x == y) + (y < x) 的标准方法？

Question

在香草 Coq 中，我会写

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

获得三个目标，一个为n < m，一个为n = m，一个为m < n。在 ssreflect 中，我将从

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

在 ssreflect 中将其分为三种情况的标准/规范方法是n < m什么？n == mm < n

Answer 1

您可以使用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].

按照 ssreflect 风格，这个引理自动简化了目标中的比较函数，如n < m,n == m等。