将参数传递给参数为LTE的函数的证明

Question

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

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或任何其他函数来实现呢？

我找到了this question，但是没有我需要的证明就解决了。

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

Answer 1

在您第二次尝试的Just情况下，由于递归，您有一个证明LTE k n，但在声明时需要LTE (S k) (S n)。您可以通过两种方式找到缺少的步骤。 REPL中的Search用于该类型的功能：