当Idris中的lambda抽象了相关类型时，我该如何证明一个“看似显而易见”的事实？

Question

当Idris中的lambda抽象了相关类型时，我该如何证明一个“看似显而易见”的事实？

14

我正在用Idris编写一个基本的单子解析器，以熟悉其语法和与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。

无论如何，我被困在练习的定理证明部分 - 我似乎找不到很多关于Idris-centric的定理证明文档。我想也许我需要开始看Agda教程（尽管我坚信我想学的是依赖类型语言Idris！）。

- h.forrest.alexander

5

为了符合 lambda，您需要“函数外延原理”（funext：（f，g：a-> b）->（（x：a）-> f x = g x ）-> f = g）。可悲的是，据我所知，Agda和Idris都无法证明这个陈述，因此必须将其作为公设。另一种选择是引入自己的相等概念（例如，p = q <=> forall s. parse p s = parse q s'），但我认为Idris 的 VerifiedSemigroup` 不具备处理自定义相等性的功能。 - Vitus

谢谢！这有点澄清了事情。知道术语“函数外延性”让我对这个想法有了更深入的解释。看起来我需要在某个地方依赖公理才能使这个验证实例工作 - 至少现在是这样。所以我不完全确定如何继续 - funext = believe me 看起来像是作弊 - 但再说一遍，这并不像我在其他语言中尝试过的玩具问题那样需要严格的证明，如果有的话，只会在注释中。 - h.forrest.alexander

由于仍然没有答案：您是否希望我将评论转换为实际答案？ - Vitus

我还没有时间尝试使用你的答案来解决这个问题。我计划先尝试弄清楚这个问题，然后更新我的问题，但是工作和暑期期末考试占据了我的时间。如果你有解决方案，我一定想看看！ - h.forrest.alexander

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Vitus · Accepted Answer

简单的答案是你不能。在内涵类型理论中推理函数相当困难。例如，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进行案例分析的函数该怎么办？）

我不确定Idris如何处理公理，所以我不会详细解释。请记住，如果您不小心处理公理，可能会搞乱一些东西。

另一种困难的方法是使用集合同构。集合同构基本上是带有自定义相等性的类型。其思想是，与其在内置相等性（在Idris中为=，在Agda中为≡）上工作的Monoid（或在您的情况下为 VerifiedSemigroup），不如拥有具有不同底层相等性的特殊单态（或半群）。通常，这是通过将单态（半群）操作与相等性和一堆证明打包在一起来完成的，即（伪代码中）：

=   : 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

这个解决方案有不同的权衡考虑，即新的相等性不能完全替代内置的相等性（当您需要重写一些术语时，这种情况往往会出现）。但如果您只想展示您的代码按照某个自定义的相等性完成了所需功能，那么这是非常好的。