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

我正在 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.

不管怎样，我陷入了练习的定理证明部分——而且我似乎找不到太多以伊德里斯为中心的定理证明文档。我想也许我需要开始查看 Agda 教程（尽管 Idris 是我确信我想学习的依赖类型语言！）。

简单的答案是你不能。在内涵类型理论中，关于函数的推理是相当尴尬的。例如，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))

where ++-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 (or VerifiedSemigroup在你的情况下）适用于内置的平等（=在伊德里斯，≡在 Agda 中），你有一个特殊的幺半群（或半群），具有不同的底层等式。这通常是通过将幺半群（半群）运算与等式和一堆证明打包在一起来完成的，即（伪代码）：

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

这一解决方案有不同的权衡，即新的等式不能完全替代内置的等式（当您需要重写某些术语时，这往往会出现）。但如果您只是想证明您的代码做了它应该做的事情（达到某些自定义的相等性），那就太好了。