Идрис передает функции доказательство того, что аргументы являются LTE

У меня есть функция, которая вычитает два 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 или любую другую функцию, чтобы реализовать это?

Я нашел этот вопрос, но он был решен без необходимых мне доказательств.

Не могли бы вы подсказать, что я делаю неправильно и как правильно реализовать такую ​​​​проверку?


dependent-type theorem-proving ghc idris
person Most Wanted    schedule 12.04.2020    source источник

Ответы (1)


arrow_upward
2
arrow_downward

В случае 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>p для решения ?hole, что является лучшей функцией в Idris IMO!). Это также приведет к

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

Кроме того, isLTE является smallerThan только с более мощным Dec, чем Maybe, потому что в отрицательном случае вы получаете доказательство того, что k не меньше и не равно n. Таким образом, isLTE не содержит ошибок, а smallerThan всегда может возвращать Nothing.

Вы можете использовать это в функции вызова dummy, например:

foo : Nat -> Nat -> Nat
foo x y = case isLTE x y of
   Yes prf => dummy x y
   No contra => Z
person xash    schedule 12.04.2020
comment
Спасибо за подсказку по поиску - person Most Wanted; 12.04.2020