为什么不能在相当简单的案例中进行案例分析

Question

好吧，代码

From mathcomp Require Import ssreflect ssrnat ssrbool eqtype.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Inductive nat_rels m n : bool -> bool -> bool -> Set :=
| CompareNatLt of m < n : nat_rels m n true false false
| CompareNatGt of m > n : nat_rels m n false true false
| CompareNatEq of m == n : nat_rels m n false false true.
Lemma natrelP m n : nat_rels m n (m < n) (m > n) (m == n).
Proof.
case (leqP m n); case (leqP n m).
move => H1 H2; move: (conj H1 H2) => {H1} {H2} /andP.
rewrite -eqn_leq => /eqP /ssrfun.esym /eqP H.
by rewrite H; constructor.
move => H. rewrite leq_eqVlt => /orP. 
case.

错误为Error: Case analysis on sort Set is not allowed for inductive definition or.case之前的最后一个目标是

m, n : nat
H : m < n
============================
m == n / m < n -> nat_rels m n true false (m == n)

我已经在非常类似的情况下使用了这种构造(rewrite leq_eqVlt => /orP; case(，它刚刚起作用：

Lemma succ_max_distr n m : (maxn n m).+1 = maxn (n.+1) (m.+1).
Proof.
wlog : m n / m < n => H; last first.
rewrite max_l /maxn; last by exact: ltnW.
rewrite leqNgt.
have: m.+1 < n.+2 by apply: ltnW.
by move => ->.
case: (leqP n m); last by apply: H.
rewrite leq_eqVlt => /orP.  case.

1. 这两种情况有什么区别
2. 以及为什么"；归纳定义或"？"不允许对排序集进行案例分析

Answer 1

这两种情况的区别在于执行case命令时的目标类型(Set vs Prop(。在第一种情况下，你的目标是nat_rels ...，你在Set中声明了归纳；在第二种情况下，你的目标是在Prop中实现平等。

当目标处于Set(第一种情况(时，不能对/进行案例分析的原因是/已声明为Prop值。与此类声明相关的主要限制是，不能使用Prop中的信息内容在Set(或更一般的Type(中构建内容，因此Prop在提取时与擦除语义兼容。

特别是，对/进行案例分析会泄露/有效的一面，不能允许您使用该信息在Set中构建一些数据。

您至少有两种解决方案可供选择：

1. 您可以将您的家庭nat_rels从Set移动到Prop，如果这与您以后想要做的事情兼容的话
2. 或者，你可以利用你想要分支的假设是可判定的这一事实，并找到一种从m <= n中产生一些{m == n} + { m <n }的方法；这里的符号CCD_ 24是命题的CCD_