Luna Flow
日本語

parser チュートリアル

このチュートリアルでは、parser パッケージでテキストから論理式、ゴール、定理スクリプトを読み取る。カーネル状態なしでパースして構造を調べ、テキストをカーネル項へローワリングし、元の入力の中でエラーの位置を特定し、証明スクリプトのステップ構造を読む。ここで使う定理スクリプトは回帰コーパスから取ったものである。

クイックスタート

moon.pkg でパッケージをインポートする。

import {
  "Luna-Flow/QED/kernel",
  "Luna-Flow/QED/logic",
  "Luna-Flow/QED/parser",
}

ゴールをパースしてカーネル項へローワリングする。

test "quick start" {
  let st = @logic.install_prop_prelude(@kernel.empty_kernel_state()).unwrap()
  let goal = @parser.parse_goal(st, "⊢ T").unwrap()
  inspect(@kernel.term_to_string(@parser.parsed_goal_concl(goal)), content="Const(T#1 : bool)")
  inspect(@parser.parsed_goal_hyps(goal).length(), content="0")
}

T は命題論理のプレリュードの定数であるため、状態には先に install_prop_prelude が必要である。

日常的な作業

論理式のまとまり方を確認する

parse_term_raw は状態を必要とせず、優先順位規則が生成する木を示す。

test "grouping" {
  // ∧ binds tighter than ∨, which binds tighter than ->
  let t = @parser.parse_term_raw("a ∧ b ∨ c -> d").unwrap()
  inspect(t is @parser.Infix("->", @parser.Infix("∨", @parser.Infix("∧", _, _), _), _), content="true")
  // -> associates to the right
  let r = @parser.parse_term_raw("a -> b -> c").unwrap()
  inspect(r is @parser.Infix("->", @parser.Name("a"), @parser.Infix("->", _, _)), content="true")
  // application is juxtaposition and binds tightest
  let app = @parser.parse_term_raw("f x ∧ y").unwrap()
  inspect(app is @parser.Infix("∧", @parser.App(_, _), @parser.Name("y")), content="true")
}

ASCII 入力を使う

\and、\or、\not、\imp、|- と入力できる。これらはパースの前に ∧、∨、¬、->、⊢ へ正規化される。

test "ascii" {
  let a = @parser.parse_goal_raw("p \\and q |- \\not r").unwrap()
  let b = @parser.parse_goal_raw("p ∧ q ⊢ ¬r").unwrap()
  inspect(a.concl is @parser.Prefix("¬", _) && b.concl is @parser.Prefix("¬", _), content="true")
  inspect(@parser.normalize_parser_input("p \\imp q").unwrap().text, content="p -> q")
}

ローカルを宣言して項をローワリングする

自由な名前はローカルか宣言済みの定数でなければならない。ローカルは parse_let または parse_env_push_local で宣言する。

test "locals" {
  let st = @logic.install_prop_prelude(@kernel.empty_kernel_state()).unwrap()
  let pre = @logic.default_prop_prelude()
  let env = @parser.parse_let(@parser.empty_parse_env(), "let p : bool").unwrap()
  let env = @parser.parse_let(env, "let q : bool").unwrap()
  let t = @parser.parse_term_with_env(st, env, "p ∧ q -> p").unwrap()
  let (lhs, rhs) = @logic.prop_dest_imp(st, pre, t).unwrap()
  inspect(@logic.prop_dest_and(st, pre, lhs) is Some(_), content="true")
  inspect(@kernel.term_to_string(rhs), content="Var(p : bool)")
  // without the declaration, `r` is unknown
  inspect(@parser.parse_term_with_env(st, env, "p ∧ r") is Err(@parser.Sig(@kernel.UnknownConst)), content="true")
}

エラーの位置を見つける

エラーのオフセットは、正規化で長さが変わった場合でも、渡したテキスト内の位置を指す。

test "error position" {
  let src = "p \\and"
  match @parser.parse_term_raw(src) {
    Err(e) => {
      inspect(e.code is @parser.UnexpectedEof, content="true")
      inspect(e.offset, content="6")
      inspect(e.detail, content="unexpected end while parsing atom")
    }
    Ok(_) => fail("expected a parse error")
  }
}

入力は 6 文字で \and の後で終わっているため、オフセット 6 は正規化後の p ∧ の終わりではなく、ユーザーが入力したものの終わりである。

定理スクリプトを読む

定理スクリプトは、ヘッダ、ゴール、位置付きのステップのリストへとパースされる。次は examples/demo_and.qed の demo_and スクリプトである。

test "script structure" {
  let src = "theorem demo_and (x : bool) : ⊢ x -> x ∧ x := by\n  intro h\n  split { exact h } { exact h }"
  let s = @parser.parse_theorem_script_raw(src).unwrap()
  inspect(s.name, content="demo_and")
  inspect(s.binders[0].src, content="(x : bool)")
  let steps = s.body.steps
  inspect(steps[0].step is @parser.Intro("h"), content="true")
  inspect(steps[1].src, content="split") // the step itself; its blocks are branches
  // the two branch blocks of split, each with one step
  let second = steps[1].branches[1]
  inspect(second.body.steps[0].step_index, content="4")
  assert_eq(second.body.steps[0].branch_path, [2])
}

ステップ番号は、分岐の内側も含め、すべてのステップを読む順に数える。intro が 1、split が 2、最初の exact が 3、2 番目が 4 である。prover はこれらの番号で失敗を報告する。

さらに進む

量化されたゴールをローワリングする。 forall はゴールの先頭で受け付けられ、定理ヘッダの束縛子としてローワリングされる。束縛された名前はゴールの自由変数になる。

test "forall goal" {
  let st = @logic.install_prop_prelude(@kernel.empty_kernel_state()).unwrap()
  let g = @parser.parse_goal(st, "⊢ forall (x : bool), x -> x").unwrap()
  let free = @kernel.free_vars(@parser.parsed_goal_concl(g))
  inspect(free.length() == 1 && free[0].0 == "x", content="true")
}

同一性を保つ。 parse_resolved_term と parse_resolved_goal_with_env は、定数の同一性が凍結された elab の項を返す。elab チュートリアルで説明するように、項を保存して後で検査する場合に使う。

テキストから関数を定義する。 parse_def_function(state, env, "def id(x : bool) : bool { x }") はカーネルを通じて定義を許容し、その定理を返す。parser API を参照。

スクリプトを実行する。 スクリプトをパースしても証明にはならない。ソーステキストを prover に渡すと、ゴールをローワリングし、tactics パッケージで各ステップを実行し、上で見たスパンで失敗を報告する。

よくある落とし穴

  • 古い結合子の綴り。 /\ と \/ は受け付けられない。∧、∨ または \and、\or を使うこと。
  • 連鎖した等号。 a = b = c は NonAssocChain エラーになる。括弧を付けること。
  • 項の中の量化子。 forall はゴールの先頭でのみ許される。parse_term はそれを Parse エラーで拒否する。
  • ターンスタイルの欠落。 ゴールには仮定がなくても ⊢ または |- が必要である。T ではなく ⊢ T と書くこと。
  • プレリュードなしの T と F。 これらはキーワードではなく定数であり、install_prop_prelude がなければ未知の名前である。
  • 命題でないものに対する結合子。 f : bool -> bool のとき f ∧ p はローワリング時に Logic(NotBoolTerm) で失敗する。

次のステップ