10

Isabelle 理論ファイルでは、次のような単純な 1 行の戦術を書くことができます。

apply (clarsimp simp: split_def split: prod.splits)

しかし、証明を自動化し、ML オブジェクトを生成するために ML コードを書き始めるとtactic、これらのワンライナーはかなり冗長になります。

clarsimp_tac (Context.proof_map (
    Simplifier.map_ss (fold Splitter.add_split @{thms prod.splits})
    #> Simplifier.map_ss (fn ss => ss addsimps [@{thm split_def}]))
  @{context}) 1

Isabelle/ML レベルで単純な 1 行の戦術を記述する簡単な方法はありますか?

たとえば、反引用のようなもの: @{tactic "clarsimp simp: split_def split: prod.splits"}type の関数を生成するcontext -> tacticことは理想的な解決策です。

4

3 に答える 3

5

さまざまな可能性があると思いますが、それはアプリケーションのコンテキストによって最適なものが少し異なります。一般に、自動化された証明のための個々の ML コードは、非常に古い時代には一般的でしたが、今日では比較的まれであることに注意してください。たとえば、かなり小規模なHOL-Bali (1997 年に開始) のカスタム戦術の量と、AFP の大規模なJinjaThreads (2007 年に開始し、最近まで継続) を比較してください。

ML 反引用符を入れ子@{tactic}にすることは、原則として機能しますが、定理の引数が再び Isar または ML ソースである必要がある場合はどうなるかなど、さらなる疑問にすぐに遭遇します。

ML で戦術構築ブロックをアンチクォートする代わりに、より基本的なアプローチは、次のような通常のメソッド構文を与えることで、Isar で証明手順を引用することです。

ML {*
  (*foo_tac -- the payload of what you want to do,
    note the dependency on ctxt: Proof.context*)
  fun foo_tac ctxt =
    let
      val my_ctxt =
        ctxt |> Simplifier.map_simpset
         (fold Splitter.add_split @{thms prod.splits} #>
          Simplifier.add_simp @{thm split_def})
    in ALLGOALS (clarsimp_tac my_ctxt) end
*}

method_setup foo = {*
  (*concrete syntax like "clarsimp", "auto" etc.*)
  Method.sections Clasimp.clasimp_modifiers >>
    (*Isar method boilerplate*)
    (fn _ => fn ctxt => SIMPLE_METHOD (CHANGED (foo_tac ctxt)))  
*}

ここでは、最初foo_tacに Isabelle/ML で従来の定義を作成し、それを証明方法として通常の Isar の方法でラップしました。後者はSIMPLE_METHOD、「チェインされた事実」を目標状態にプッシュCHANGEDし、Isar メソッドが確実に進行するようにするようなラッパーがあることを意味します (simpまたはのようにauto)。

このfoo_tac例では、コンテキスト (またはその simpset) の変更が固定の分割ルールによって一定であると想定しています。そこにさらにパラメーターが必要な場合は、具体的なメソッド構文に含めることができます。Method.sectionsこの点に関しては、すでに非常に洗練されていることに注意してください。より基本的な引数パーサーは、 isar-refマニュアルの「証明方法の定義」セクションに記載されています。method_setupまた、 (Isabelle/IsarMethod.setupで) または (Isabelle/ML で)のソースを検索して、既存の例を調べる必要があります。

具体的なメソッド構文の代わりに ML の反引用符を使用したい場合は、次の@{context}ような修飾子を許可するバリアントを試すことができます。

@{context simp add: ...}

これは少し推測的で、その場で発明されたものであり、悪い習慣になる可能性があります。前述したように、ML は Isabelle フレームワークの不可欠な部分ですが、Isabelle でのきめ細かい戦術プログラミングは近年少し使われなくなりました。より多くのアプリケーション コンテキストを使用してより具体的な質問を提示する場合は、反引用のアプローチを再検討できます。

于 2013-03-05T18:51:38.613 に答える
3

他の回答に加えて、Isabelle2015 のEisbachと呼ばれる新しい高レベルの戦術/証明方法構築言語 (Coq の Ltac に似ています) があることに言及する価値があると思います。これは、理解しやすく維持しやすいことを目的としています。

于 2016-01-03T21:03:50.480 に答える
1

このクラスは、次のようMethodに a を介して戦術を抽出するのに十分なインターフェイスを提供しているようです。cases_tactic

(*
 * Generate an ML tactic object of the given Isar string.
 *
 * For example,
 *
 *   mk_tac "auto simp: field_simps intro!: ext" @{context}
 *
 * will generate the corresponding "tactic" object.
 *)
fun mk_tac str ctxt =
let
  val parsed_str = Outer_Syntax.scan Position.start str
      |> filter Token.is_proper
      |> Args.name
  val meth = Method.method (Proof_Context.theory_of ctxt)
      (Args.src (parsed_str, Position.start)) ctxt
in
  Method.apply (K meth) ctxt [] #> Seq.map snd
end

または代わりに反引用として：

(*
 * Setup an antiquotation of the form:
 *
 *    @{tactic "auto simp: foo intro!: bar"}
 *
 * which returns an object of type "context -> tactic".
 *
 * While this doesn't provide any benefits over a direct call to "mk_tac" just
 * yet, in the future it may generate code to avoid parsing the tactic at
 * run-time.
 *)
val tactic_antiquotation_setup =
let
  val parse_string =
    ((Args.context -- Scan.lift Args.name) >> snd)
      #>> ML_Syntax.print_string
      #>> (fn s => "mk_tac " ^ s)
      #>> ML_Syntax.atomic
in
  ML_Antiquote.inline @{binding "tactic"} parse_string
end

次のように理論​​ファイルに設定します。

setup {*
  tactic_antiquotation_setup
*}

これは次のように使用できます。

lemma "(a :: nat) * (b + 1) = (a * b) + a"
  by (tactic {* @{tactic "metis Suc_eq_plus1 mult_Suc_right nat_add_commute"} @{context} *})

望んだ通りに。

于 2013-03-11T03:39:29.110 に答える