1

我有一个减去两个Nats 的函数。我如何证明我传递给它的第一个参数实际上小于第二个参数

dummy : (k : Nat) -> (n : Nat) -> {auto smaller : LTE k n} -> Nat
dummy k n = n - k

我尝试了几个不起作用的解决方案

smallerThan : (k : Nat) -> (n : Nat) -> Maybe (LTE k n)
smallerThan Z k = Just (LTEZero {right=k})
smallerThan (S k) Z = Nothing
smallerThan (S k) (S n) = case isLTE k n of
                            Yes prf => Just prf
                            No contra => Nothing

smallerThan (S k) (S n) = case smallerThan k n of
                            Nothing => Nothing
                            Just lte => Just (cong lte)

我知道我的洞的类型smallerThan (S k) (S n) = Just (?hole)是LTE (S k) (S n)，但是如何正确使用fromLteSucc或任何其他功能来实现它？

我找到了这个问题，但没有我需要的证据就解决了。

您能否提示我做错了什么以及如何正确实施这种检查？

4

1 回答 1

2

在Just您第二次尝试的情况下，由于递归，您有一个证明LTE k n，但正如您所说，需要LTE (S k) (S n). 您可以通过两种方式找到缺失的步骤。在 REPL 中搜索该类型的函数：

Idris> :search LTE k n -> LTE (S k) (S n)
= Prelude.Nat.LTESucc : LTE left right -> LTE (S left) (S right)
If n <= m, then n + 1 <= m + 1

甚至更简单，通过 REPL 或编辑器使用证明搜索（我可以使用<space>pto solve ?hole，这是 Idris IMO 中最好的功能！）。这也会导致

 smallerThan (S k) (S n) = case smallerThan k n of
                             Nothing => Nothing
                             Just lte => Just (LTESucc lte)

此外，isLTE只是比smallerThan更强大，因为在否定的情况下，您会得到一个不小于或等于的证明。所以没有错误，而总是可以返回。DecMaybeknisLTEsmallerThanNothing

您可以在dummy调用函数中使用它，例如：

foo : Nat -> Nat -> Nat
foo x y = case isLTE x y of
   Yes prf => dummy x y
   No contra => Z
于 2020-04-12T16:34:25.767 回答