theorem-proving - Idris のカスタム証明者戦術

Question

私がそれを正しく理解していれば (主にapplyTactic関数の存在から)、Idris で定理証明用のカスタム タクティクスを作成することが可能です。その方法を学ぶために使用できる例は何 (またはどこ) ですか?

Answer 1

Idris でカスタム タクティクスを記述するためのメカニズムには、高レベルと低レベルのリフレクションの 2 つがあります。

高レベルのリフレクションを使用して、評価されたデータではなく構文で実行される関数を作成します。引数は削減されません。これらの関数は、Idris の既存の戦術を使用して定義された新しい戦術を返します。証明項を直接返したい場合は、いつでも を使用できますExact。この種の反射の例はエフェクト ライブラリにあります。高レベルのリフレクション戦術はbyReflection、証明モードで使用して呼び出されます。

低レベルのリフレクションでは、Idris のコア型理論から引用された用語を直接操作します。タクティックはTT -> List (TTName, TT) -> Tactic、最初の引数がゴールの型で、2 番目の引数がローカル証明コンテキストであり、返される結果が高レベルのリフレクションと同じである関数です。これは、上記にリンクされている loladelicです。これらはapplyTactic、プルーフ モードで使用して呼び出されます。