如何针对荒谬/不可构造的类型进行模式匹配？

Question

根据我的理解，这两个定义a̶r̶e̶̶e̶q̶u̶i̶v̶a̶l̶e̶n̶t̶表示相同的行为：

data _<_ : ℕ → ℕ → Set where                       
    lt-zero : {n : ℕ} → zero < suc n
    lt-suc  : {m n : ℕ} → m < n → (suc m) < (suc n)

lt : ℕ → ℕ → Bool
lt  _       zero   = false
lt  zero   (suc n) = true
lt (suc m) (suc n) = m < n

除了 _<_ 可以更容易地用来证明关于它自己的事情，而 lt，根据我的发现，更容易用于编程其他行为。例如，我可以看到如何使用 lt:

轻松定义 min 函数

min : ℕ → ℕ → ℕ
min x y where lt x y
... | true  = x
... | false = y

有没有办法让我使用 _<_ 定义 min 和其他类似的函数？根据我的发现，如果 y 小于 x，则无法模式匹配 x < y。在这些情况下是否有其他方法可以使用 _<_？

编辑：向 _<_ 添加一个不真实的案例是否是一个明智的想法？

̶e̶d̶i̶t̶2̶：̶

编辑 3：我更改了以下 min 的定义，以便在使用 min.

时能够省略 x <? y 的证明

data _<?_ (n m : ℕ) : Set where
    isLT  : n < m → n <? m
    notLT : m ≤ n → n <? m

min : (x y : ℕ) → {p : x <? y} → ℕ
min x y (isLT _)  = x
min x y (notLT _) = y

这没有按预期工作。如果我使用 C-c C-n 来评估 min 1 2，它会 returns min 1 2。如果我给它一个证明，我可以让它达到 return 分钟，但是如果我评估 min 2 1 (isLT _) 它 returns 2，而不是给我一条错误消息。有没有办法让我使用 _<_ 定义 min，以便 Agda 可以评估 min 1 2？

Answer 1

有一种方法可以消除 Agda 中不可能的模式。使用您对 _<_ 的定义你可以尝试证明传递性来说明这一点。

le-trans : ∀ {m n k} → m < n → n < k → m < k
le-trans {k = k} lt-zero b = {!!}
le-trans (lt-suc a) (lt-suc b) = lt-suc (le-trans a b)

Goal: 0 < k
b  : suc .n < k

我们在第一个参数上进行模式匹配，步骤案例是假设的简单应用。在基本情况下，我们必须在 k 上进行模式匹配，因为您的数据类型的基本构造函数表示 zero < suc n，但我们对 k 还一无所知。在 k 上进行模式匹配时，我们看到两种情况

le-trans : ∀ {m n k} → m < n → n < k → m < k
le-trans {k = zero} lt-zero b = {!!}
le-trans {k = suc k} lt-zero b = {!!}
le-trans (lt-suc a) (lt-suc b) = lt-suc (le-trans a b)

在第一个中，我们看到了不可能发生的事情，即 Goal: 0 < zero 并且我们有一个 b : suc .n < zero 类型的元素，它不可能发生。然后，你可以在 b 上进行模式匹配，Agda 会发现你不能构造这样的东西，并将消除这种情况 le-trans {k = zero} lt-zero ()。而在另一种情况下，您可以使用基本构造函数来证明它。

le-trans : ∀ {m n k} → m < n → n < k → m < k
le-trans {k = zero} lt-zero ()
le-trans {k = suc k} lt-zero b = lt-zero
le-trans (lt-suc a) (lt-suc b) = lt-suc (le-trans a b)

因此，在数据类型中定义不正确的大小写是不合适的。您定义元素的构造方式。您对 _<?_ 的最后定义是有道理的，实际上可以使用。

编辑 min

一旦你有了 _<?_ 的归纳关系，你就可以按如下方式工作。定义一个为您提供 m <? n 的函数，然后对于 min 函数，执行抽象调用该函数。

data _≥_ : ℕ → ℕ → Set where
  get-z : ∀ {n} → n ≥ zero
  get-s : ∀ {m n} → m ≥ n → (suc m) ≥ (suc n)

data _<?_ (n m : ℕ) : Set where
  y-< : n < m → n <? m
  n-< : n ≥ m → n <? m

f<? : (m n : ℕ) → m <? n
f<? zero zero = n-< get-z
f<? zero (suc n) = y-< lt-zero
f<? (suc m) zero = n-< get-z
f<? (suc m) (suc n) with f<? m n
f<? (suc m) (suc n) | y-< x = y-< (lt-suc x)
f<? (suc m) (suc n) | n-< x = n-< (get-s x)

min : ℕ → ℕ → ℕ
min x y with f<? x y
min x y | y-< _ = x
min x y | n-< _ = y

如何针对荒谬/不可构造的类型进行模式匹配？

How to pattern match against absurd / unconstructable Type?

agda