付録アイデア: 直観主義論理の決定タクティク自作

1. 直観主義論理の命題を示すアルゴリズム

目標は

Γ ⊢ A

（仮定 Γ から命題 A を示す）

を自動で解くことである。

古典論理の tauto のように真理値表を使うのではなく、証明探索 (proof search) を行う。

⸻

基本規則

仮定にあれば成功

A ∈ Γ

Γ ⊢ A

対応する Lean タクティク：

assumption

⸻

False があれば成功

False ∈ Γ

Γ ⊢ A

対応：

contradiction

または

exact False.elim h

⸻

ゴールが含意なら intro

Γ, A ⊢ B

Γ ⊢ A → B

対応：

intro h

⸻

ゴールが連言なら constructor

Γ ⊢ A
Γ ⊢ B

Γ ⊢ A ∧ B

対応：

constructor

⸻

ゴールが選言なら left/right

Γ ⊢ A

Γ ⊢ A ∨ B

または

Γ ⊢ B

Γ ⊢ A ∨ B

対応：

left

または

right

ここはバックトラックが必要。

⸻

仮定の分解

連言仮定

A ∧ B ∈ Γ

なら

Γ, A, B

へ展開する。

対応：

cases h

または

rcases h with ⟨ha, hb⟩

⸻

選言仮定

A ∨ B ∈ Γ

なら場合分け。

Γ, A ⊢ C
Γ, B ⊢ C

Γ ⊢ C

対応：

cases h

⸻

含意仮定の利用

仮定に

A → B

があり、ゴールが

B

なら

apply h

して

⊢ A

へ帰着する。

⸻

探索アルゴリズム

擬似コード：

prove(Γ, goal):
if goal ∈ Γ:
success
if False ∈ Γ:
success
if goal = True:
success
if goal = A → B:
intro
prove(Γ ∪ {A}, B)
if goal = A ∧ B:
prove(Γ, A)
prove(Γ, B)
if goal = A ∨ B:
try left
if fail:
try right
if Γ contains A ∧ B:
destruct it
if Γ contains A ∨ B:
split into branches
if Γ contains A → goal:
apply it
fail

⸻

例：¬¬(P ∨ ¬P)

直観主義論理で証明可能。

探索は：

⊢ ¬¬(P ∨ ¬P)
intro h
h : ¬(P ∨ ¬P)
⊢ False
apply h
⊢ P ∨ ¬P
right
⊢ ¬P
intro hp
hp : P
h : ¬(P ∨ ¬P)
⊢ False
apply h
⊢ P ∨ ¬P
left
⊢ P
assumption

これで閉じる。

⸻

注意

探索はループする可能性がある。

例：

h : P → P
⊢ P

に対して

apply h
⊢ P

を無限に繰り返せる。

したがって実装では

• 深さ制限
• visited state

のどちらかが必要。

今回は深さ制限を採用した。

⸻

2. Lean 実装

概念的には：

partial def intuitionCore :
Nat → TacticM Unit

を作る。

引数：

depth : Nat

は探索深さ。

⸻

メインループ

partial def intuitionCore : Nat → TacticM Unit
| 0 =>
throwError "depth limit reached"
| depth + 1 => do
if ← tryAssumptionLike then return
if ← tryIntro depth then return
if ← tryConstructor depth then return
if ← tryOrGoal depth then return
if ← tryCasesHyp depth then return
if ← tryApplyHyp depth then return
throwError "proof search failed"

⸻

assumption/trivial

partial def tryAssumptionLike : TacticM Bool := do
tryOrRestore do
evalTactic (← `(tactic| assumption))

⸻

intro

ゴールが

A → B

なら

intro

する。

partial def tryIntro : Nat → TacticM Bool

で実装。

⸻

constructor

ゴールが

A ∧ B

なら

constructor

する。

⸻

left/right

ゴールが

A ∨ B

なら

left

を試し、

失敗したら

right

を試す。

⸻

仮定の分解

ローカルコンテキストを走査：

let lctx ← getLCtx

各仮定について

A ∧ B

または

A ∨ B

なら

cases h

を実行。

⸻

apply 仮定

ローカル仮定を順に

apply h

してみる。

成功したら再帰。

⸻

補助関数

状態保存

バックトラックのため：

let s ← saveState
...
s.restore

を使う。

ラッパ：

tryOrRestore :
TacticM Unit → TacticM Bool

⸻

サブゴール解決

solveAllGoals depth

を定義して、

生成されたサブゴール全部に対して

intuitionCore depth

を再帰適用する。

⸻

利用例

example (P Q : Prop) :
P ∧ Q → Q ∧ P := by
intuition_prop

⸻

example (P Q R : Prop) :
(P → Q) → (Q → R) → P → R := by
intuition_prop

⸻

example (P Q : Prop) :
P ∧ ¬ P → Q := by
intuition_prop

⸻

example (P : Prop) :
¬¬(P ∨ ¬ P) := by
intuition_prop

成功する。

⸻

一方、

example (P : Prop) :
P ∨ ¬ P := by
intuition_prop

は失敗する。

なぜなら実装は

by_cases
Classical.em
by_contra

を使わず、純粋に直観主義論理の導入・除去規則だけで探索しているからである。

Start by reviewing the proposed intuitionCore entry point and its helpers: tryAssumptionLike, tryIntro, tryConstructor, tryOrGoal, tryCasesHyp, tryApplyHyp, and solveAllGoals. Exercise the listed intuition_prop examples, including the expected failure for P ∨ ¬P; the work is done when the successful examples close without classical reasoning and depth limits prevent looping.