如何为根深蒂固的归纳类型选择设计？

Question

[在学习充分依据的同时，我想看看不同的设计如何表现。例如，对于一个类型：

data _<_ (x : Nat) : Nat -> Set where
   <-b : x < (suc x)
   <-s : (y : Nat) -> x < y -> x < (suc y)

基础充分容易证明。但是，如果相似的类型定义不同：

data _<_ : Nat -> Nat -> Set where
   z-< : (m : Nat) -> zero < (suc m)
   s<s : (m n : Nat) -> m < n -> (suc m) < (suc n)

很明显，在两种情况下，下降链都不是无限的，但在第二种情况下，很难证明有充分的基础：对于给定的(y -> y < x -> Acc y)，很难证明x存在。

是否有一些原则有助于选择第一个设计优先于第二个设计？

---

证明第二个定义的充分依据并不是很难，它只需要额外的定理。在这里，依靠_==_对于Nat的可判定性，我们可以为情况_<_构造新的(suc y) != x，并且可以重写目标类型以将解决方案用于解决已知的尺寸减小的问题作为解决方案。 suc y。

-- trying to express well-foundedness is tricky, because of how x < y is defined:
-- since both x and y decrease in the inductive step case, need special effort to
-- prove when the induction stops - when no more constructors are available
<-Well-founded : Well-founded Nat _<_
<-Well-founded x = acc (aux x) where
   aux : (x y : Nat) -> y < x -> Acc _<_ y
   aux zero    y       ()
   aux x       zero    z-<           = acc \_ ()
   aux (suc x) (suc y) (s<s y<x) with is-eq? (suc y) x
   ...                   | no  sy!=x = aux x (suc y) (neq y<x sy!=x)
   ...                   | yes sy==x rewrite sy==x = <-Well-founded x

Answer 1

第一个定义在某种意义上是“规范的”，而第二个定义则不是。在阿格达（Agda）中，每种归纳类型都有一个子项关系，该子项关系是有根据的和可传递的，尽管不一定是总的，可确定的或不相关的。对于W型，如下所示：