Доказательство свойств потоковых функций в Идрисе - PullRequest
Новая
       35

Доказательство свойств потоковых функций в Идрисе

1 голос
/ 01 апреля 2019

Я пытаюсь доказать свойства потоковых функций и монадических потоковых функций [1] (и, в конечном счете, программ FRP).

Идрис доволен моей формализацией потоковых функций: 

module SF

import Data.Vect
import Syntax.PreorderReasoning

%default total

data SF : Type -> Type -> Type where
  SFG : (a -> (b, Inf (SF a b))) -> SF a b

steps : {n : Nat} -> SF a b -> Vect n a -> Vect n b
steps {n = Z}   (SFG s) []        = []
steps {n = S m} (SFG s) (a :: as) =
    let (b, s') = s a
        bs = steps s' as
    in (b::bs)

Я могу тривиально определить подъемные / точечные прикладные функции: 

liftM : (a -> b) -> SF a b
liftM f = SFG $ \a => (f a, liftM f)

А также два варианта идентичности для SF: 

identityM : SF a a
identityM = SFG $ \a => (a, identityM)

identity2 : SF a a
identity2 = liftM id

Это проходит проверку целостности Идриса. Однако, если я сейчас попытаюсь доказать, что identityM и identity2 равны, я столкнусь с проблемами. Я могу заявить собственность следующим образом: 

proof1 :  (Eq b)
       => (n : Nat)
       -> (v : Vect n a)
       -> (steps identityM v) = (steps identity2 v)
proof1 Z [] = ?proof1_rhs_1
proof1 (S k) v = ?proof1_rhs_2

Если я спрашиваю о типе ?proof1_rhs_1, Идрис правильно скажет steps identityM [] = steps identity2 []. Тем не менее, если я попытаюсь использовать эквациональные рассуждения, чтобы выразить только это: 

proof1 Z [] = (steps {n=Z} identityM []) ={ ?someR }=
              (steps {n=Z} identity2 []) QED

Тогда Идрис несчастен: 

When checking argument x to function Syntax.PreorderReasoning.Equal.qed:
        Type mismatch between
                steps identity2 [] (Inferred value)
        and
                steps identity2 [] (Given value)

        Specifically:
                Type mismatch between
                        steps identity2
                and
                        []Unification failure

Есть ли способ заставить эту работу?

[1] https://dl.acm.org/citation.cfm?id=2976010

1 Ответ

3 голосов
/ 01 апреля 2019

Это обычное «неявное обобщение Идриса для запутывания правил определения области действия»: 

proof1 :  (Eq b)
       => (n : Nat)
       -> (v : Vect n a)
       -> (steps identityM v) = (steps identity2 v)

означает 

proof1 : {identityM : _} -> {identity2 : _} -> (...)
       -> (steps identityM v) = (steps identity2 v)

Чтобы сослаться на предыдущие определения, вам нужно использовать квалифицированные имена SF.identityM и SF.identity2. Вероятно, у вас есть другие проблемы (Eq b с b, упомянутым больше нигде в остальном типе, кажется сомнительным).

...