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

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

1 голос
/ 12 апреля 2020

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

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

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

1 Ответ

2 голосов
/ 12 апреля 2020

В случае 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
...