絵図とテキスト形式

問題は、絵図で自明なことをどうやってテキストエンコードするか？

• 論理絵図＝横棒図〈バー図〉
• 圏論絵図＝ストリング図

テキスト	論理絵図	圏論絵図
命題	命題	ワイヤー・ラベル
証拠ラベル	バー・ラベル	ノード・ラベル
証明項	横棒図	ストリング図
公理	上段空白横棒	入力ワイヤー無しノード

順行リーズニング：

テキスト	論理絵図	圏論絵図
結合や適用	カット	ワイヤー接続
ラムダ抽象	含意導入	ワイヤー曲げ
デカルトペア	連言導入	コピーと接続

variables A B : Prop
variable h : A ∧ ¬ B

#check And.intro (And.right h) (And.left h)

ここで、

And.intro (And.right h) (And.left h) ≡ (And.intro ◁ (And.right h)) ◁ (And.left h)

だが、意味的に、

And.intro∪( (And.right∪(h)),  (And.left∪(h))

と解釈してから、次の絵を描く。

テキスト	横棒図	ストリング図
And.intro∪	上段2項目バー	2入力ワイヤー・ノード
And.right∪	上段1項目バー	1入力ワイヤー・ノード
And.left∪	上段1項目バー	1入力ワイヤー・ノード
()	横棒図のスタック	ストリング図の接続
( , )	横棒図の横並べとスタック	ストリング図の横並べと接続

絵から先に見ると：

1. 絵
2. 絵から素直なテキスト化、結合には括弧を使う
3. フルカリー化して、結合の代わりに適用だけを使う。
4. Lean記法に直す。

圏論的な図、古典的な関数記法、フルカリー化と適用への変換、構文変換というけっこう長い道のりがある。

道のりは長いが、https://leanprover.github.io/logic_and_proof/propositional_logic_in_lean.html の説明法はいいと思う。例えば：

-- 素材の準備
variable (A B : Prop)
variable (h : A ∧ ¬ B)

-- 項として組み立てる
#check And.left h
#check And.right h
#check And.intro (And.right h) (And.left h)