昨日の記事「ヤシコフスキ／カリシュ／モンタギュー形式の証明： 人間可読・将来的機械可読」に挙げたヤシコフスキ／カリシュ／モンタギュー流証明の例題をもう一度載せます。$`\newcommand{\mrm}[1]{\mathrm{#1}}
\require{color}
\newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }
\newcommand{\letsShow}{\Keyword{lets show } }
\newcommand{\conclude}{\Keyword{conclude } }
\newcommand{\endBlock}{\Keyword{end } }
\newcommand{\assume}{\Keyword{assume } }
\newcommand{\Imp}{ \Rightarrow }`$
$`\letsShow ( (p \Imp q) \land (\lnot r \Imp \lnot q) )\Imp (p \Imp r)\\
\bullet (p \Imp q) \land (\lnot r \Imp \lnot q) \text{ を仮定して、 } (p \Imp r) \text{ を導く}\\
\quad \assume (p \Imp q) \land (\lnot r \Imp \lnot q) \:\cdots \text{(1)}\\
\qquad \letsShow p \Imp r\\
\qquad \bullet p \text{ を仮定して }r \text{ を導く}\\
\qquad\quad \assume p \:\cdots \text{(2)}\\
\qquad\qquad \downarrow \text{上の仮定を再掲}\\
\qquad\qquad (p \Imp q) \land (\lnot r \Imp \lnot q) \:\cdots \text{(3)}\\
\qquad\qquad \downarrow \text{すぐ上の連言の左側}\\
\qquad\qquad p \Imp q \:\cdots \text{(4)}\\
\qquad\qquad \downarrow \text{モーダスポネンスを適用}\\
\qquad\qquad q \:\cdots \text{(5)}\\
\qquad\qquad \downarrow \text{上の連言の右側}\\
\qquad\qquad \lnot r \Imp \lnot q \:\cdots \text{(6)}\\
\qquad\qquad \letsShow r\\
\qquad\qquad \bullet \text{背理法を使う}\\
\qquad\qquad\quad \assume \lnot r \:\cdots \text{(7)}\\
\qquad\qquad\qquad \downarrow\text{先の命題を再掲}\\
\qquad\qquad\qquad \lnot r \Imp \lnot q \:\cdots \text{(8)}\\
\qquad\qquad\qquad \downarrow \text{モーダスポネンスを適用}\\
\qquad\qquad\qquad \lnot q \:\cdots \text{(9)}\\
\qquad\qquad\qquad \downarrow\text{先に得られた命題を再掲}\\
\qquad\qquad\qquad q \:\cdots \text{(10)}\\
\qquad\qquad\qquad \downarrow\text{矛盾が生じる}\\
\qquad\qquad\qquad \bot\\
\qquad\qquad\quad \endBlock\\
\qquad\qquad \conclude r\\
\qquad\quad \endBlock\\
\qquad \conclude p \Imp r\\
\quad \endBlock\\
\conclude ( (p \Imp q) \land (\lnot r \Imp \lnot q) )\Imp (p \Imp r)
`$
これを、Lean 4（「プログラミング言語Lean 4の現状」参照）の宣言的証明記述〈declarative proof description〉*1にトランスパイルすることにします。現状、トランスパイラはこの世に存在してないので、手でやります。
入れ子になった証明をうまく記述する方法が分からなかったので、サブ証明は切り出して別な定理にします。上のコードの (7), (8), (9), (10) の番号が付いている部分が一つの定理になります。この定理に対して背理法を使って $`r`$ を示す部分もまた一つの定理にします。
主定理の最後の部分でサブ定理を呼び出すことにします。「呼び出す」なんて言ったのは、Lean 4では関数と定理の区別は特にないからです。カリー／ハワード／ランベック対応により、命題は型のことであり、証明は計算で、定理は関数です。
「背理法を使う」推論規則（Lean 4では推論規則と定理の区別もない）by_contradictionは、モジュールMathlib.Logic.Basicに入っているので、ソースファイル冒頭で当該モジュールをインポートする必要があります。Lean 4では前方参照が出来ないので、サブ証明の定理のほうを主定理より先に書かなくてはなりません。
import Mathlib.Logic.Basic
#check by_contradiction
section JKM_sample
variable {p q r : Prop}
-- (_5 : q) (_6: ¬r → ¬q) |- ¬r → False
theorem sub' (_5 : q) (_6: ¬r → ¬q) : ¬r → False :=
fun _7 : ¬r =>
-- ↓先の命題を再掲
have _8 : ¬r → ¬q := _6
-- ↓モーダスポネンスを適用
have _9 : ¬q := _8 _7
-- ↓先に得られた命題を再掲
have _10 : q := _5
show False from absurd _10 _9
#check sub'
-- lets show p → r∙
-- 背理法を使う
theorem sub (_5 : q) (_6: ¬r → ¬q) : p → r :=
fun _a : p =>
show r from by_contradiction (sub' _5 _6)
#check sub
-- lets show ((p → q)∧(¬r → ¬q)) → (p → r)
theorem sample : ((p → q)∧(¬r → ¬q)) → (p → r) :=
-- ((p → q)∧(¬r → ¬q)) を仮定して (p → r) を導く
fun _1 : (p →q)∧(¬r → ¬q) =>
-- p を仮定して r を導く
fun _2 : p =>
-- ↓上の仮定を再掲
have _3 : (p → q)∧(¬r → ¬q) := _1
-- ↓すぐ上の連言の左側
have _4 : p → q := And.left _3
-- ↓モーダスポネンスを適用
have _5 : q := _4 _2
-- ↓上の連言の右側
have _6 : ¬r → ¬q := And.right _3
-- サブ証明を呼び出す
show r from sub _5 _6 _2
#check sample
end JKM_sampleトランスパイルされたコードを見ると、もとのヤシコフスキ／カリシュ／モンタギュー形式とそんなに違うわけでもないです。
難しい、というか、従来のコンパイラ／トランスパイラと違うのは、自然言語を解釈しながら翻訳作業をする必要があるところです。手動トランスパイルは人間（僕）がやっているので、自然言語解釈は問題ありません（そりゃそうだ）が、自然言語処理とプログラミング言語処理が混じった翻訳系を作るのはチャレンジングかも知れません。いやっ、意外とアッサリできちゃうかも ‥‥？ どうだろ？ ウーン、よくわからんです。
*1:Lean 4の場合、Isabelle/Isarのような別言語があるわけではなくて、ラムダ式に対する薄いシンタックスシュガーが少数あるだけです。
