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

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.

两种情况有什么区别？
以及为什么“归纳定义或不允许对排序集进行案例分析”？

Answer 1

两种情况的区别在于执行case命令时目标的类型（Set vs Prop）。在第一种情况下，你的目标是 nat_rels ... 并且你在 Set 中声明了归纳；在第二种情况下，您的目标是 Prop.

中的平等

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

特别是，对 \/ 进行案例分析会泄露 \/ 有效的一面，并且不允许您使用该信息在 Set.

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

您可以将您的家人 nat_rels 从 Set 搬到 Prop 如果这与您以后想做的事情兼容。
或者你可以利用你想要分支的假设是可判定的这一事实，并找到一种方法从 m <= n 中产生一些 {m == n} + { m <n }；这里的符号 { _ } + { _ } 是命题的 Set 值析取。

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

Why unable to perform case analysis in rather simple case

coq

ssreflect