Agdaにおける決定的な平等はn^2未満の場合？

Question

私は推論したいプログラミングランゲージのASTのデータ型を持っていますが、ASTのコンストラクタは約10種類あります。

data Term : Set where 
    UnitTerm : Term 
    VarTerm : Var -> Term 
    ... 
    SeqTerm : Term -> Term -> Term 

私は、この言語の構文木のために決定的な平等性を持つ関数を書こうとしています。理論的にはこれは簡単です。複雑すぎることはありません。単純なデータがASTに保存されているだけです。

問題は、このような関数を書くには、約100個のケースが必要だと考えられます。コンストラクタごとに10個のケースが必要です。

eqDecide : (x : Term) -> (y : Term) -> Dec (x ≡ y) 
    eqDecide UnitTerm UnitTerm = yes refl 
    eqDecide UnitTerm (VarTerm x) = Generic.no (λ()) 
    ... 
    eqDecide UnitTerm (SeqTerm t1 t2) = Generic.no (λ()) 
    EqDecide (VarTerm x) UnitTerm = Generic.no (λ()) 
    ... 

問題は、重複したケースがたくさんあることです。可能な他のコンストラクタは統合できないので、コンストラクタが一致する最初のパターンマッチの後、理想的にはアンダースコアと一致させることができますが、私はそれを行うことはできません。

私は、平等を導くためにthis libraryを使用しようとしました。私は厳しい陽性で問題に遭遇しているだけでなく、いくつかの一般的なエラーを取得するのはかなり難しいです。 The Agda Preludeにはこのためのいくつかの機能もありますが、かなり未熟で、標準ライブラリから必要なものが欠けています。

人々はどのように決定的な平等をどのように実践していますか？彼らはそれを吸うと100のすべての場合を書き込むか、または私は行方不明だトリックですか？これはちょうど言語の新しさが見える場所ですか？

Answer 1

あなたはリフレクションを使用しないよう、まだ例のリニア数で決定可能平等を証明したい場合は、次のアプローチを試みることができる：

1. は機能embed : Term → Nat（または平等を決定可能いる他のいくつかのタイプを定義します。ラベル付きツリーなどの証明が容易です）。
2. あなたの関数が実際に注入的であることを証明してください。
3. 関数が、結果の型に決定的な等価性を持ち、Termで決定可能な等価性を終えるために注入関数であるという事実を利用してください（例えば、標準ライブラリのRelation.Nullary.Decidableのvia-injection参照）。