1

嗯，代码

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.

错误是 is之前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. 以及为什么“归纳定义或不允许对排序集进行案例分析”？
4

1 回答 1

2

这两种情况的区别在于执行case命令时的目标类型（Set vs Prop）。在第一种情况下，您的目标是nat_rels ...并且您声明了 inductive in Set; 在第二种情况下，您的目标是实现平等Prop。

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

特别是\/，\/在Set.

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

  1. 如果这与您以后想要做的事情兼容，您可以将您的家人nat_rels从Set那里搬到那里。Prop
  2. 或者你可以利用你想要分支的假设是可判定的这一事实，并找到一种方法来产生{m == n} + { m <n }一些m <= n; 这里的符号{ _ } + { _ }是Set命题的-值析取。
于 2021-06-19T08:14:53.510 回答