当相关类型被伊德里斯的lambda抽象出来时,我如何证明一个"看似明显"的事实？

Question

我正在Idris中编写一个基本的monadic解析器,以熟悉Haskell的语法和差异.我有基本的工作正常,但我坚持尝试为解析器创建VerifiedSemigroup和VerifiedMonoid实例.

不用多说,这里是解析器类型,Semigroup和Monoid实例,以及VerifiedSemigroup实例的开始.

data ParserM a          = Parser (String -> List (a, String))
parse                   : ParserM a -> String -> List (a, String)
parse (Parser p)        = p
instance Semigroup (ParserM a) where
    p <+> q             = Parser (\s => parse p s ++ parse q s)
instance Monoid (ParserM a) where
    neutral             = Parser (const []) 
instance VerifiedSemigroup (ParserM a) where
    semigroupOpIsAssociative (Parser p) (Parser q) (Parser r) = ?whatGoesHere

我基本上被卡住了intros,具有以下证明状态:

-Parser.whatGoesHere> intros
----------              Other goals:              ----------
{hole3},{hole2},{hole1},{hole0}
----------              Assumptions:              ----------
 a : Type
 p : String -> List (a, String)
 q : String -> List (a, String)
 r : String -> List (a, String)
----------                 Goal:                  ----------
{hole4} : Parser (\s => p s ++ q s ++ r s) =
          Parser (\s => (p s ++ q s) ++ r s)
-Parser.whatGoesHere> 

看起来我应该能够以某种方式rewrite一起使用appendAssociative,但我不知道如何"进入"lambda \s.

无论如何,我坚持练习的定理证明部分 - 我似乎找不到很多以伊德里斯为中心的定理证明文件.我想也许我需要开始查看Agda教程(虽然Idris是我确信我想要学习的依赖类型的语言!).

Answer 1

简单的答案是你做不到.在内涵型理论中,关于功能的推理是相当尴尬的.例如,Martin-Löf的类型理论无法证明:

S x + y = S (x + y)
0   + y = y

x +? S y = S (x + y)
x +? 0   = x

_+_ ? _+?_  -- ???

(据我所知,这是一个实际的定理而不仅仅是"缺乏想象力的证据";但是,我找不到我读它的来源).这也意味着没有更一般的证据:

ext : ? {A : Set} {B : A ? Set}
        {f g : (x : A) ? B x} ?
        (? x ? f x ? g x) ? f ? g

这称为函数扩展性:如果您可以证明所有参数的结果相等(即函数在扩展上相等),那么函数也是相等的.

这可以完美地解决您遇到的问题:

<+>-assoc : {A : Set} (p q r : ParserM A) ?
  (p <+> q) <+> r ? p <+> (q <+> r)
<+>-assoc (Parser p) (Parser q) (Parser r) =
  cong Parser (ext ? s ? ++-assoc (p s) (q s) (r s))

++-assoc你在哪里证明了联想属性_++_.我不确定它在战术上的表现如何,但它会非常相似:应用同余Parser并且目标应该是:

(\s => p s ++ q s ++ r s) = (\s => (p s ++ q s) ++ r s)

然后,您可以应用扩展性来获得假设s : String和目标:

p s ++ q s ++ r s = (p s ++ q s) ++ r s

然而,正如我之前所说,我们没有函数扩展性(请注意,对于类型理论而言,这种情况并非如此:扩展类型理论,同伦类型理论和其他理论能够证明这一陈述).简单的选择是将其视为公理.与任何其他公理一样,您有以下风险:

• 失去一致性(即能够证明虚假;虽然我认为功能扩展性是可以的)

• 打破减少(refl在给出这个公理的情况下,仅对案例分析做什么的函数是什么？)

我不确定伊德里斯如何处理公理,所以我不会详细介绍.请注意,如果你不小心,公理会弄乱一些东西.

艰难的选择是使用setoids.setoid基本上是一种配备自定义相等的类型.这个想法是,你有一个特殊的monoid(或半群),它具有不同的底层相等性,而不是Monoid(或VerifiedSemigroup在你的情况下)在内置的平等(=在Idris,?在Agda中).这通常通过将monoid(半群)操作与相等和一组证明打包在一起来完成,即(在伪代码中):

=   : A ? A ? Set  -- equality
_*_ : A ? A ? A    -- associative binary operation
1   : A            -- neutral element

=-refl  : x = x
=-trans : x = y ? y = z ? x = z
=-sym   : x = y ? y = x

*-cong : x = y ? u = v ? x * u = y * v  -- the operation respects
                                        -- our equality

*-assoc : x * (y * z) = (x * y) * z
1-left  : 1 * x = x
1-right : x * 1 = x

解析器的相等性选择很明确:如果两个解析器的输出同意所有可能的输入,则两个解析器是相等的.

-- Parser equality
_?p_ : {A : Set} (p q : ParserM A) ? Set
Parser p ?p Parser q = ? x ? p x ? q x

这个解决方案有不同的权衡,即新的平等不能完全取代内置的(当你需要重写一些术语时,这往往会出现).但是如果你只是想表明你的代码能够完成它应该做的事情(直到一些自定义的相等),那就太棒了.