agda - 関連する型がIdrisのラムダによって抽象化されている場合、「一見明白な」事実を証明するにはどうすればよいですか?

Question

構文と Haskell との違いに慣れるために、Idris で基本的なモナド パーサーを作成しています。私はそれがうまく機能する基本を持っていますが、パーサー用の 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