История изменений

Исправление monk, 04.04.21 22:15 (текущая версия) :

(например, чтобы срабатывала проверка на входе одной функции рекурсивной фуркции и сочеталась с проверкой на выходе другой), то придётся понимать как устроены доказательства.

{-@ append :: xs:[a] -> ys:[a] -> {v:[a] | (len v) = (len xs) + (len ys)} @-}
append [] ys     = ys
append (x:xs) ys = x : append xs ys

Или покажи пример на зависимых типах.

в сложности доказательств (как и жидких)

В случае жидких всё, что нерекурсивно или рекурсивно по одному аргументу доказывается автоматически (как пример с append). То, что не доказывается автоматически, доказывается очень наглядно:

Например, есть рекурсивное определение фибоначчи

{-@ fib::{x:Int | x >=0} -> {r : Int|r>0} @-}
fib :: Int -> Int
fib 0 = 1
fib 1 = 1
fib n = fib (n-1) + fib (n-2)

условие, что результат больше нуля, компилятор выводит автоматически.

и с аккумулятором

{-@ fibacc::Int -> Int -> n:Int -> {n1:Int | n1 >=0 && (n1 >= n || n1 < 2)} -> Int / [n1-n] @-} 
fibacc :: Int -> Int -> Int -> Int -> Int
fibacc _ _ _ 0 = 1
fibacc _ _ _ 1 = 1
fibacc f1 f2 n n1 
 | n == n1 = f1 + f2
 | otherwise = fibacc f2 (f1+f2) (n+1) n1

{-@ fib2::{n:Int | n >=0} -> r:Int @-}
fib2 :: Int -> Int
fib2 n = fibacc 1 1 2 n

В фигурных скобках ограничения жидких типов.

Теперь, если надо доказать, что fib n = fib2 n для всех n можно попробовать просто дописать постусловие:

{-@ fib2::{n:Int | n >=0} -> {r:Int | r = fib n} @-}

Не получается. Компилятор недостаточно умён. Можно написать ему доказательство:

{- fibaccLemma :: f1:Int -> f2:Int -> {k:Int | k >= 0} -> {n:Int | n >=2 && n-k>=2 }  -> { fibacc f1 f2 k n == fibacc f1 f2 k (n-1) + fibacc f1 f2 k (n-2) } / [n-k] @-}
fibaccLemma :: Int -> Int -> Int -> Int -> Proof
fibaccLemma f1 f2 k n | n - k == 2
    = fibacc f1 f2 k n == fibacc f1 f2 k (n-1) + fibacc f1 f2 k (n-2)
    === fibacc f2 (f1+f2) (k+1) n == fibacc f2 (f1+f2) (k+1) (n-1) + f1 + f2
    === fibacc (f1+f2) (f1+f2+f2) (k+2) n == f2+f1+f2+f1+f2
    === f1+f2+f1+f2+f2 == f2+f1+f2+f1+f2
    *** QED
fibaccLemma f1 f2 k n | n - k > 2
    = fibacc f1 f2 k n == fibacc f1 f2 k (n-1) + fibacc f1 f2 k (n-2)
    === fibacc f2 (f1+f2) (k+1) n == fibacc f2 (f1+f2) (k+1) (n-1) + fibacc f2 (f1+f2) (k+1) (n-2)
    ? fibaccLemma f2 (f1+f2) (k+1) n
    *** QED

{-@ fibTheorem :: {n:Int | n >= 0} -> { fib n == fib2 n } @-}
fibTheorem :: Int -> Proof 
fibTheorem 0 = fib 0 == fib2 0
    === 1 == fibacc 1 1 2 0
    === 1 == 1
    *** QED
fibTheorem 1 = fib 1 == fib2 1 
    === 1 == fibacc 1 1 2 1
    === 1 == 1 
    *** QED
fibTheorem n = fib n == fib2 n
    === fib (n-1) + fib (n-2) == fibacc 1 1 2 n
    ? fibaccLemma 1 1 2 n
    === fib (n-1) + fib (n-2) == fibacc 1 1 2 (n-1) + fibacc 1 1 2 (n-2)
    === fib (n-1) + fib (n-2) == fib2 (n-1) + fib2 (n-2)
    *** QED

В случае же зависимых типов доказательство получается почти нечитаемое.

Исходная версия monk, 04.04.21 21:57: