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 中，standard/canonical 如何将其分为三种情况，n < m、n == m 和 m < 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等比较函数

Coq/SSReflect: (x < y) + (x == y) + (y < x) 大小写的标准方式？

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

coq

coq-tactic

ssreflect