证明两个自然数不相等的证据？

Question

使用 Shapeless 的 Nat 类型，我如何得出两个自然数不相等的证据？

这就是我目前所拥有的，但它只能证明给定的Nat不等于0。我如何证明任意两个Nat值不相等？

trait NEq[A <: Nat, B <: Nat] extends Serializable

object NEq {
  def apply[A <: Nat, B <: Nat](implicit neq: A != B): NEq[A, B] = neq

  type !=[A <: Nat, B <: Nat] = NEq[A, B]

  implicit def neq1[B <: Nat] = new !=[Succ[B], _0] {}
  implicit def neq2[B <: Nat] = new !=[_0, Succ[B]] {}
}

Answer 1

为什么不呢：

 def neq[A <: Nat, B <: Nat](implicit ev: A <:!< B) = ev

示例：

scala> neq[_1, _2]
res8: shapeless.<:!<[shapeless.nat._1,shapeless.nat._2] = shapeless.package$$anon@7db44dae

scala> neq[_1, _1]
<console>:15: error: ambiguous implicit values:
 both method nsubAmbig1 in package shapeless of type [A, B >: A]=> shapeless.<:!<[A,B]
 and method nsubAmbig2 in package shapeless of type [A, B >: A]=> shapeless.<:!<[A,B]
 match expected type shapeless.<:!<[shapeless.nat._1,shapeless.nat._1]
              neq[_1, _1]
                 ^

另请参阅：Type constraint for type inequality in scala

和this，以防万一你出于某种原因想在运行时检查它。

Answer 2

使用 Shapeless 的 =:!= 是完成此操作的最简单方法，但它不是很通用（如果您需要证明两个数字相差一个，等等怎么办？），而且通常在我开始时使用它我最终切换到自定义类型 class.

您的 NEq 只遗漏了一点——您已经有了基本案例，但您需要归纳步骤。您知道 Succ 永远不会是 _0，但您也知道如果两个 Succ 的内容不同，则它们也不相同：

trait NEq[A <: Nat, B <: Nat] extends Serializable

object NEq {
  def apply[A <: Nat, B <: Nat](implicit neq: A != B): NEq[A, B] = neq

  type !=[A <: Nat, B <: Nat] = NEq[A, B]

  implicit def neq1[B <: Nat]: Succ[B] != _0 = new !=[Succ[B], _0] {}
  implicit def neq2[B <: Nat]: _0 != Succ[B] = new !=[_0, Succ[B]] {}

  implicit def neq3[A <: Nat, B <: Nat](implicit neq: A != B): Succ[A] != Succ[B] =
    new !=[Succ[A], Succ[B]] {}
}

这将按预期工作。

证明两个自然数不相等的证据？

Evidence that two natural numbers are not equal?

scala

shapeless