tactics API リファレンス

tactics パッケージ（Luna-Flow/QED/tactics）は、証明を後ろ向きに実行する。ProofState はルートゴールと保留中のサブゴールのリストを保持する。各 TacticStep は先頭の保留中ゴールを変換し、最後のゴールが閉じると、パッケージは記録されたステップを logic とカーネルの規則を通して前向きにリプレイし、定理を構築する。ps_qed は、その定理がルートゴールをちょうど証明している場合にのみ、それを返す。このパッケージは kernel と logic に依存する。

ステップとカーネル規則の関係はtactics の設計で説明する。tactics のチュートリアルではゴールを一歩ずつ証明する。証明スクリプトを書くユーザーは、prover を通じてこのパッケージを利用する。

ゴール

`Goal`

Goal は証明すべきシーケントであり、仮定と結論からなり、すべて命題である。

pub struct Goal {
  hyps : Array[@kernel.Term]
  concl : @kernel.Term
}

ゴール内の結合子は、パーサが生成するとおり、logic ビルダーの基底項である。

`mk_goal`、`goal_hyps`、`goal_concl`、`goal_hyp_count`

これらの関数はゴールを構築し、読み取る。goal_hyps はコピーを返す。

pub fn mk_goal(Array[@kernel.Term], @kernel.Term) -> Goal
pub fn goal_hyps(Goal) -> Array[@kernel.Term]
pub fn goal_concl(Goal) -> @kernel.Term
pub fn goal_hyp_count(Goal) -> Int

ステップ

`TacticStep`

TacticStep は後ろ向き証明の一ステップである。

pub enum TacticStep {
  Intro(String)
  Exact(String)
  Apply(String)
  Assumption
  Split
  Left
  Right
}

ステップ	現在のゴール	新しいゴール	閉じる根拠
`Intro(h)`	$\Gamma \vdash a \Rightarrow b$	$\Gamma, a \vdash b$ （ローカル `h : a` を伴う）	含意導入
`Intro(x)`	$\Gamma \vdash (\lambda y.\,P) = (\lambda y.\,\top)$	$\Gamma \vdash P[x/y]$ （`x` は fresh）	DEDUCT_ANTISYM_RULE と ABS
`Exact(n)`	$\Gamma \vdash c$	なし	ローカル `n`、または `exact` モードのカタログ定理 `n`
`Apply(n)`	$\Gamma \vdash b$	$\Gamma \vdash a$	`n : a ⇒ b` による含意除去
`Assumption`	$\Gamma \vdash c$ （ $c \in \Gamma$ ）	なし	その仮定
`Split`	$\Gamma \vdash a \wedge b$	$\Gamma \vdash a$ 、次に $\Gamma \vdash b$	連言導入
`Left`	$\Gamma \vdash a \vee b$	$\Gamma \vdash a$	選言導入
`Right`	$\Gamma \vdash a \vee b$	$\Gamma \vdash b$	選言導入

Apply(n) は n を次の順に解決する。帰結がゴールであるローカルの含意。規則名 imp_elim（仮定とローカルの中からそのような含意を探す）、imp_intro（隠れたローカルを伴う Intro と同様）、and_intro（Split と同様）。その後、apply モードではカタログ名。規則名は tactics レベルの便宜であり、証明スクリプトで使うと文書化されている定理名はユーザーマニュアルに一覧がある。hole のステップはない。hole は prover が扱う。

`step_intro`、`step_exact`、`step_apply`、`step_assumption`、`step_split`、`step_left`、`step_right`

これらの関数は、対応する TacticStep 値を構築する。

pub fn step_intro(String) -> TacticStep
pub fn step_exact(String) -> TacticStep
pub fn step_apply(String) -> TacticStep
pub fn step_assumption() -> TacticStep
pub fn step_split() -> TacticStep
pub fn step_left() -> TacticStep
pub fn step_right() -> TacticStep

証明状態

`ProofState`

ProofState は後ろ向き証明の抽象状態である。ルートゴール、リプレイに必要なデータを伴う順序付きの保留中ゴール、そして定理が得られた後はその最終定理を保持する。

type ProofState

状態は不変であり、どの操作も新しい状態を返す。

`ps_init` と `ps_enter_frame`

ps_init(goal) は、保留中ゴールを一つ持つ goal の証明を開始する。ps_enter_frame は同じ操作であり、prover が分岐フレームを開くときに使う名前である。

pub fn ps_init(Goal) -> ProofState
pub fn ps_enter_frame(Goal) -> ProofState

`ps_apply` と `ps_apply_script`

ps_apply(state, prelude, ps, step) は、先頭の保留中ゴールに対してステップを一つ実行する。ps_apply_script はステップのリストを実行し、最初のエラーで停止する。

pub fn ps_apply(@kernel.KernelState, @logic.PropPrelude, ProofState, TacticStep) -> Result[ProofState, TacticExecError]
pub fn ps_apply_script(@kernel.KernelState, @logic.PropPrelude, ProofState, Array[TacticStep]) -> Result[ProofState, TacticExecError]

新しいゴールは残りのゴールの前に置かれるため、Split の最初のサブゴールが次に処理される。ゴールを閉じるステップは、その根拠をただちにカーネルでリプレイする。リプレイが失敗すれば、そのステップは失敗する。

`ps_qed` と `ps_close_frame`

ps_qed は、完了した証明の定理を返す。ps_close_frame は分岐フレームに対する同じ操作である。

pub fn ps_qed(ProofState) -> Result[@kernel.Thm, TacticExecError]
pub fn ps_close_frame(ProofState) -> Result[@kernel.Thm, TacticExecError]

ゴールが保留中の間は UnsolvedGoals で失敗する。定理は最後のゴールが閉じたときに検査済みである。β 正規化の後、その仮定はルートゴールの仮定と一対一で一致し、その結論は α 同値の範囲でルートの結論に等しくなければならない。そうでなければ、閉じるステップは ProofSynthesisUnavailable で失敗している。

`ps_close_current_with_th`

ps_close_current_with_th(state, prelude, ps, th) は、与えられた定理が、そのゴールの仮定のうち高々それらだけから、ゴールの結論を証明していることを検査したうえで、先頭の保留中ゴールをその定理で閉じる。

pub fn ps_close_current_with_th(@kernel.KernelState, @logic.PropPrelude, ProofState, @kernel.Thm) -> Result[ProofState, TacticExecError]

定理が適合しない場合は GoalShapeMismatch で、何も保留中でない場合は NoGoals で失敗する。

`ps_isolate_pending_at`

ps_isolate_pending_at(ps, i) は、保留中ゴール i をルートゴールとする、元の状態のリプレイコンテキストを持たない新しい証明状態を返す。i が範囲外なら None を返す。

pub fn ps_isolate_pending_at(ProofState, Int) -> ProofState?

prover はこれを使って、分岐ブロックを独自のフレームで実行し、分岐内の失敗が兄弟に影響しないようにする。

test "proof state" {
  let st = @logic.install_prop_prelude(@kernel.empty_kernel_state()).unwrap()
  let pre = @logic.default_prop_prelude()
  let env = @parser.parse_env_push_local(@parser.empty_parse_env(), "p", @kernel.bool_ty())
  let env = @parser.parse_env_push_local(env, "q", @kernel.bool_ty())
  let g = @parser.parse_goal_with_env(st, env, "⊢ p ∧ q -> q ∧ p").unwrap()
  let ps = @tactics.ps_init(@tactics.mk_goal(@parser.parsed_goal_hyps(g), @parser.parsed_goal_concl(g)))
  let ps = @tactics.ps_apply_script(st, pre, ps, [
    @tactics.step_intro("h"),
    @tactics.step_split(),
  ]).unwrap()
  inspect(@tactics.ps_goal_count(ps), content="2")
  inspect(@tactics.ps_qed(ps) is Err(@tactics.UnsolvedGoals), content="true")
  let ps = @tactics.ps_apply_script(st, pre, ps, [
    @tactics.step_exact("and_elim_r"),
    @tactics.step_exact("and_elim_l"),
  ]).unwrap()
  let th = @tactics.ps_qed(ps).unwrap()
  inspect(@kernel.thm_hyp_count(th), content="0")
  // nothing is left to do
  inspect(@tactics.ps_apply(st, pre, ps, @tactics.step_split()) is Err(@tactics.NoGoals), content="true")
}

証明の観察

`ps_goal_count`、`ps_current_goal`、`ps_pending_goal_at`

ps_goal_count は保留中ゴールの数である。ps_current_goal は先頭のゴールを、ps_pending_goal_at は指定インデックスのゴールを返す。

pub fn ps_goal_count(ProofState) -> Int
pub fn ps_current_goal(ProofState) -> Goal?
pub fn ps_pending_goal_at(ProofState, Int) -> Goal?

`ps_root_goal`

ps_root_goal は証明を開始したゴールを返す。

pub fn ps_root_goal(ProofState) -> Goal

`LocalHyp`、`local_hyp_name`、`local_hyp_term`

LocalHyp は、ユーザーから見たとおり Intro が導入する名前付き仮定である。

type LocalHyp

pub fn local_hyp_name(LocalHyp) -> String
pub fn local_hyp_term(LocalHyp) -> @kernel.Term

`ps_current_local_hyps` と `ps_current_branch_path`

これらの関数は、先頭の保留中ゴールのローカルと分岐パスを返す。分岐パスは、ルートから順に、各 Split でどちらのサブゴールを取ったか（1 または 2）と、Left または Right（常に 1）を並べたものである。

pub fn ps_current_local_hyps(ProofState) -> Array[LocalHyp]
pub fn ps_current_branch_path(ProofState) -> Array[Int]

`ProofGoalView`、`ps_current_focus`、`ps_pending_focus_at`

ProofGoalView は、保留中ゴールをそのローカルと分岐パスとともにまとめたものである。二つの関数は、先頭の保留中ゴール、または指定インデックスのゴールのビューを返す。

type ProofGoalView

pub fn ps_current_focus(ProofState) -> ProofGoalView?
pub fn ps_pending_focus_at(ProofState, Int) -> ProofGoalView?
pub fn proof_goal_view_goal(ProofGoalView) -> Goal
pub fn proof_goal_view_locals(ProofGoalView) -> Array[LocalHyp]
pub fn proof_goal_view_branch_path(ProofGoalView) -> Array[Int]

`ProofStateSnapshot` と `ps_snapshot`

ps_snapshot は、ルートゴール、保留中ゴールの数、現在のフォーカスを一つの値に捕捉する。診断用である。

type ProofStateSnapshot

pub fn ps_snapshot(ProofState) -> ProofStateSnapshot
pub fn proof_state_snapshot_root_goal(ProofStateSnapshot) -> Goal
pub fn proof_state_snapshot_pending_goal_count(ProofStateSnapshot) -> Int
pub fn proof_state_snapshot_current(ProofStateSnapshot) -> ProofGoalView?

test "observe" {
  let st = @logic.install_prop_prelude(@kernel.empty_kernel_state()).unwrap()
  let pre = @logic.default_prop_prelude()
  let env = @parser.parse_env_push_local(@parser.empty_parse_env(), "p", @kernel.bool_ty())
  let g = @parser.parse_goal_with_env(st, env, "⊢ p -> p ∧ p").unwrap()
  let ps = @tactics.ps_init(@tactics.mk_goal(@parser.parsed_goal_hyps(g), @parser.parsed_goal_concl(g)))
  let ps = @tactics.ps_apply_script(st, pre, ps, [@tactics.step_intro("h"), @tactics.step_split()]).unwrap()
  assert_eq(@tactics.ps_current_local_hyps(ps).map(@tactics.local_hyp_name), ["h"])
  assert_eq(@tactics.ps_current_branch_path(ps), [1])
  let second = @tactics.ps_pending_focus_at(ps, 1).unwrap()
  assert_eq(@tactics.proof_goal_view_branch_path(second), [2])
  let snap = @tactics.ps_snapshot(ps)
  inspect(@tactics.proof_state_snapshot_pending_goal_count(snap), content="2")
}

リプレイコンテキスト

これらの列挙型は、保留中ゴールが閉じるときにどのようにリプレイされるかを記述する。保留中ゴールがこれらを保持するため、インターフェースに現れる。呼び出し側が構築するものではない。

`PendingRefine`

PendingRefine は、前向きに取り消すべき後ろ向きステップを記録する。ローカルの含意項の apply（ImpBackwardTerm）、含意定理の apply（ImpBackwardTheorem）、または量化されたゴールに対する intro（ユーザーの束縛子と新しいリプレイ用束縛子を伴う）（AbsBackwardTerm）である。

pub enum PendingRefine {
  ImpBackwardTerm(@kernel.Term)
  ImpBackwardTheorem(@kernel.Thm)
  AbsBackwardTerm(@kernel.Term, @kernel.Term)
}

`SplitRole`

SplitRole は、ゴールを Split の左半分か右半分かとして印付ける。右半分は、閉じるときに左半分の定理を受け取る。

pub enum SplitRole {
  SplitNone
  SplitLeft(@kernel.Term)
  SplitRight(@kernel.Term, @kernel.Thm?)
}

`OrContext`

OrContext は、Left または Right が生成したゴールを、完全な選言ともう一方の分岐とともに印付ける。

pub enum OrContext {
  OrNone
  OrPendingLeft(@kernel.Term, @kernel.Term)
  OrPendingRight(@kernel.Term, @kernel.Term)
}

エラー

`TacticExecError`

TacticExecError は、ステップまたは ps_qed の失敗である。

pub enum TacticExecError {
  UnknownName(String)
  GoalShapeMismatch(String)
  ApplyMismatch(String)
  NoGoals
  UnsolvedGoals
  ProofSynthesisUnavailable(String)
  Logic(@kernel.LogicError)
}

コンストラクタ	意味
`UnknownName(n)`	`n` はローカルでもカタログ名でもない。
`GoalShapeMismatch(msg)`	ゴールがステップの必要とする形をしていない、または `exact` に、ゴールを閉じないウィットネスが与えられた。
`ApplyMismatch(msg)`	`apply` に、ゴールで終わる含意ではないものが与えられた。
`NoGoals`	完了した証明にステップが適用された。
`UnsolvedGoals`	ゴールが保留中なのに `ps_qed` が呼ばれた。
`ProofSynthesisUnavailable(msg)`	リプレイがルートゴールの定理を構築できなかった。
`Logic(e)`	リプレイ中にカーネルまたは logic の規則が失敗した。

`tactic_goal_shape_mismatch` と `tactic_no_goals`

これらの関数は、パッケージ外の呼び出し側が自ら送出する二つのエラーを構築する。prover は、分岐ブロックがゴールに適合しないときにこれらを使う。

pub fn tactic_goal_shape_mismatch(String) -> TacticExecError
pub fn tactic_no_goals() -> TacticExecError

test "errors" {
  let st = @logic.install_prop_prelude(@kernel.empty_kernel_state()).unwrap()
  let pre = @logic.default_prop_prelude()
  let env = @parser.parse_env_push_local(@parser.empty_parse_env(), "p", @kernel.bool_ty())
  let g = @parser.parse_goal_with_env(st, env, "⊢ p -> p").unwrap()
  let ps = @tactics.ps_init(@tactics.mk_goal(@parser.parsed_goal_hyps(g), @parser.parsed_goal_concl(g)))
  let ps = @tactics.ps_apply(st, pre, ps, @tactics.step_intro("h")).unwrap()
  // `truth` is a catalog name, but not an implication
  inspect(@tactics.ps_apply(st, pre, ps, @tactics.step_apply("truth")) is Err(@tactics.ApplyMismatch(_)), content="true")
  inspect(@tactics.ps_apply(st, pre, ps, @tactics.step_exact("nope")) is Err(@tactics.UnknownName("nope")), content="true")
  inspect(@tactics.ps_apply(st, pre, ps, @tactics.step_split()) is Err(@tactics.GoalShapeMismatch(_)), content="true")
  inspect(@tactics.ps_apply(st, pre, ps, @tactics.step_assumption()) is Ok(_), content="true")
}

tactics API リファレンス

ゴール

Goal

mk_goal、goal_hyps、goal_concl、goal_hyp_count

ステップ

TacticStep

step_intro、step_exact、step_apply、step_assumption、step_split、step_left、step_right

証明状態

ProofState

ps_init と ps_enter_frame

ps_apply と ps_apply_script

ps_qed と ps_close_frame

ps_close_current_with_th

ps_isolate_pending_at

証明の観察

ps_goal_count、ps_current_goal、ps_pending_goal_at

ps_root_goal

LocalHyp、local_hyp_name、local_hyp_term

ps_current_local_hyps と ps_current_branch_path

ProofGoalView、ps_current_focus、ps_pending_focus_at

ProofStateSnapshot と ps_snapshot