SSReflect中对(x<y)+(x==y)+(y<x)分情况讨论的标准写法是什么

SSReflect下的标准拆分写法 #

你可以使用ssrnat提供的ltngtP比较视图，配合case策略完成三分支拆分，写法如下：

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

拆分后会直接得到三个子目标：

• 第一个子目标上下文会出现n < m的假设
• 第二个子目标上下文会出现n == m的假设
• 第三个子目标上下文会出现m < n的假设

如果需要同时给假设命名，可直接在case后附加命名模式，是更符合SSReflect风格的写法：

case: ltngtP n m => [n_lt_m | n_eq_m | m_lt_n].

ltngtP是SSReflect生态中专门为有序类型设计的三分法消去视图，不需要手动拆分求和类型，是该场景下的标准规范用法。

内容的提问来源于stack exchange，提问作者Jason Gross