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

Question

在 Vanilla 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.

对于 n < m，将其分为三种情况的标准/规范方法是什么？ , n == m , 和 m < n , 在 ssreflect?

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等。