ラムダ式にシンタックスシュガー

Lean 半形式証明スクリプト

λ(x:Int, y:Int).(x*x + y :Int) を次にように書く。

assume x: Int, y: Int
providing z: Int, return z + y of Int
where z: Int := x*x

もっと証明っぽく：

we assume x: Int and y: Int
it suffices to prove z: Int
 because the result comes from z + y
so try z
 we showed Int from x*x

演算子＝関数 をルールっぽく書くと：

we assume x: Int and y: Int
it suffices to prove z: Int
 because the result comes from add z y
so try z
 we showed Int from mul x x

日本語：

x: Int and y: Int と仮定する
z: Int を示せば十分である
 なぜなら add z y から結果は得られるから
では z を示そう
 我々は mul x x により Int を示せた

同義語や表記の揺れを認める。

  • により ＝ から
  • 証明すれば ＝ 提示すれば ＝ 示せば
  • を示そう ＝ に挑戦しよう ＝ を証明しよう
  • 我々は 省略可能
  • 示せた ＝ 示した ＝ 証明した
  • 結果 ＝ 結論 ＝ 目標

証明項の全体

<<証明|
  x: Int 、 y: Int と仮定する
  z: Int を示せば十分である
   なぜなら add z y から結果は得られるから
  では z を示そう
   我々は mul x x により Int を示せた
>>

Literate Programming と Verifiable Writing が双対だがほぼ同じこと。