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

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 )。在第一种情况下，您的目标是nat_rels ...，您在Set中声明了归纳；在第二种情况下，您的目标是在Prop中获得平等。

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

特别是，在\/上进行案例分析会使\/的部分变得有效，并且不能允许您使用这些信息在Set中构建一些数据。

您至少有两个解决方案可供您使用：

如果与你以后想做的事情兼容的话，你可以把你的家人的proposition.从转移到Prop。

1. 或者你可以利用这样一个事实:你想要分支的假设是可判定的，并找到一种从m <= n中产生某种{m == n} + { m <n }的方法；这里的表示法{ _ } + { _ }是Set-值分离的m <= n。