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

Question

我正在 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 为中心的定理证明文档。我想也许我需要开始查看 Agda 教程（尽管 Idris 是我确信我想学习的依赖类型语言！）。

Answer 1