<h1 id="lean%E3%81%A8%E3%81%AF">
<a class="header-anchor-link" href="#lean%E3%81%A8%E3%81%AF" aria-hidden="true"></a> Leanとは</h1>
<p>Leanは普通の関数型言語であり、なおかつ定理証明支援系でもある大変パワフルな言語です。つまり原理上実行前にわかる性質は、型に埋め込んだり、頑張って自分で証明したりすることができます。そう考えるとワクワクしてきますね！<br>
またコンパイラフロントエンドのAPIを自由にユーザーが使えるので、標準の文法や意味論とまったく同じレベルで自分の拡張を安全に仕込むことができるという、強力な拡張性を持つおもしろい言語でもあります。<br>
今回紹介するLeanの環境構築は、lean4とよばれているバージョンのもので、lean3という古いバージョンとは異なります。</p>
<h1 id="elan">
<a class="header-anchor-link" href="#elan" aria-hidden="true"></a> elan</h1>
<p>開発環境の構築には<a href="https://leanprover.github.io/lean4/doc/setup.html#setting-up-lean" target="_blank" rel="nofollow noopener noreferrer">Lean Manualのセットアップ</a>にしたがって、開発環境管理コマンドである<a href="https://github.com/leanprover/elan" target="_blank" rel="nofollow noopener noreferrer">elan</a>のインストールから始めます。</p>
<div class="code-block-container"><pre><code>curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
</code></pre></div><p><code>elan</code>はRustでいうrustup、Haskellでいうghcupで、<code>lake</code>などの必要なコマンドのインストール・アップデートを担当します。（ちなみにelanはrustupのforkだそうで、rustupを使っているなら見慣れたプロンプトが表示されると思います）<br>
LinuxやmacOSでは上記のコマンドですが、Windowsやbrew、Nixでは別途インストール方法があるようです。</p>
<p>また、VSCodeではlean4の拡張をインストールするときに、<a href="https://leanprover.github.io/lean4/doc/quickstart.html" target="_blank" rel="nofollow noopener noreferrer">Install Lean using Elanボタンを押すだけ</a>で裏でelanが走ってくれるようです。</p>
<h1 id="lake">
<a class="header-anchor-link" href="#lake" aria-hidden="true"></a> lake</h1>
<p><code>lake</code>はプロジェクト管理コマンドで、プロジェクトを新規作成したりビルドしてくれたりします。Rustでいうcargo、Haskellでいうstackやcabalです。</p>
<div class="code-block-container"><pre><code>$ lake new leanhello
</code></pre></div><p>でプロジェクトの新規作成ができ、</p>
<div class="code-block-container"><pre><code>$ tree
.
├── Leanhello.lean # ライブラリのソースコード
├── Main.lean # 実行ファイルのソースコード
└── lakefile.lean # 依存や設定など、このプロジェクトを管理するファイル

0 directories, 3 files
</code></pre></div><p>このようにプロジェクトを初期化できます。試しに<code>Main.lean</code>をのぞいてみると、</p>
<div class="code-block-container"><pre><code>import Leanhello

def main : IO Unit :=
  IO.println s!"Hello, {hello}!"
</code></pre></div><p>このようにHello worldと、プロジェクトのライブラリ（<code>Leanhello</code>）をインポートするコードが書いてあります。</p>
<h1 id="%E3%82%A8%E3%83%87%E3%82%A3%E3%82%BF%E3%81%AE%E3%82%BB%E3%83%83%E3%83%88%E3%82%A2%E3%83%83%E3%83%97">
<a class="header-anchor-link" href="#%E3%82%A8%E3%83%87%E3%82%A3%E3%82%BF%E3%81%AE%E3%82%BB%E3%83%83%E3%83%88%E3%82%A2%E3%83%83%E3%83%97" aria-hidden="true"></a> エディタのセットアップ</h1>
<p>leanのコンパイラはLSPをしゃべるので、原理上どのエディタでもセットアップは簡単で、同じ機能がつかえます。（定義ジャンプやエラー一覧の表示とジャンプ、補完など）</p>
<p>VSCodeでは、最初に拡張を入れた時点でセットアップは終わるのでやることはないです。</p>
<p>筆者はEmacsを使うため、<a href="https://github.com/leanprover/lean4-mode" target="_blank" rel="nofollow noopener noreferrer">lean4-mode</a>をインストールしました。（<code>lean-mode</code>というのがmelpaにありますが、古いlean3用なので使いません）</p>
<div class="code-block-container">
<div class="code-block-filename-container"><span class="code-block-filename">init.el</span></div>
<pre><code>(leaf lean4-mode
  :el-get "leanprover/lean4-mode"
  )
</code></pre>
</div><p>VSCodeに出るものと同様のInfoView（カーソル位置に該当する証明途中のゴールや型が表示されるパネル）は<code>C-c TAB</code>か<code>C-c C-i</code>で表示されます。</p>
<p>またNeovim用には<a href="https://github.com/Julian/lean.nvim/" target="_blank" rel="nofollow noopener noreferrer">lean.nvim</a>があり、開発も活発なようです。</p>
<h1 id="%E7%B5%82%E3%82%8F%E3%82%8A%E3%81%AB">
<a class="header-anchor-link" href="#%E7%B5%82%E3%82%8F%E3%82%8A%E3%81%AB" aria-hidden="true"></a> 終わりに</h1>
<p>ここまでで環境構築は終わりです。興味のある<a href="https://leanprover.github.io/documentation/" target="_blank" rel="nofollow noopener noreferrer">公式ドキュメント</a>を読みながらコードを書いたり証明を書いたりすると楽しいと思います。</p>
<ul>
<li>
<a href="https://leanprover.github.io/theorem_proving_in_lean4/" target="_blank" rel="nofollow noopener noreferrer">Theorem Proving in Lean 4</a>
<ul>
<li>例題つきのチュートリアルで、定理証明をやってみたい人によさそう</li>
<li>依存型、命題と証明、証明の記述方法、Leanの文法（型クラスなど）</li>
<li>有志の方々による<a href="https://aconite-ac.github.io/theorem_proving_in_lean4_ja/introduction.html" target="_blank" rel="nofollow noopener noreferrer">非公式日本語版</a>もある</li>
</ul>
</li>
<li>
<a href="https://leanprover.github.io/lean4/doc/" target="_blank" rel="nofollow noopener noreferrer">Lean Manual</a>
<ul>
<li>言語の概観を知るための資料</li>
<li>基本的な文法に加えて、言語拡張などのちょっと込み入った機能や、FAQ、開発者むけガイドなどもある</li>
</ul>
</li>
<li>
<a href="https://leanprover.github.io/functional_programming_in_lean/" target="_blank" rel="nofollow noopener noreferrer">Functional Programming in Lean</a>
<ul>
<li>普通にプログラミング言語としての使い方が書いてある</li>
<li>言語の概観やHello World、モナドトランスフォーマー、依存型を使ったプログラミング、パフォーマンスに関する話など</li>
</ul>
</li>
<li>
<a href="https://leanprover-community.github.io/mathematics_in_lean/index.html" target="_blank" rel="nofollow noopener noreferrer">Mathematics in Lean</a>
<ul>
<li>普通の数学を対象に、Leanで定理証明をする資料</li>
<li>最近lean3からlean4への対応が完了しており、<code>Theorem Proving in Lean 4</code>よりも分量がある</li>
</ul>
</li>
<li>
<a href="https://github.com/leanprover-community/lean4-metaprogramming-book" target="_blank" rel="nofollow noopener noreferrer">A Lean 4 Metaprogramming Book</a>
<ul>
<li>Lean4はElaborationという強力なメタプログラミングの機能があり、コンパイラフロントエンド自体が大体このElaborationを使ってかかれている。この記事はその概略が書いてある</li>
<li>似たようなものを知らない人にとっては読むのがすごく大変と思われる</li>
</ul>
</li>
</ul>
<p>また、<a href="https://haruhisa-enomoto.github.io/lean-math-workshop" target="_blank" rel="nofollow noopener noreferrer">数学系のためのLean勉強会</a>というイベントも2023/9/3に開催され <s>るようです。GitHubで資料も公開されるようなので、数学に興味のある方はこちらに参加するのもいいかもしれません。</s> ました。リンク先にLeanのインストール方法や、Leanの基礎の解説スライドへのリンク、演習資料などがまとまっています。</p>
<h1 id="%E4%BB%96%E3%81%AElean%E3%81%AE%E8%A8%98%E4%BA%8B">
<a class="header-anchor-link" href="#%E4%BB%96%E3%81%AElean%E3%81%AE%E8%A8%98%E4%BA%8B" aria-hidden="true"></a> 他のLeanの記事</h1>
<ul>
<li>
<a href="https://m-hiyama.hatenablog.com/entry/2022/12/31/183948" target="_blank" rel="nofollow noopener noreferrer">プログラミング言語Lean 4の現状</a>
<ul>
<li>この記事の半年前に書かれており、より詳しく書いてある</li>
</ul>
</li>
</ul>


関数型言語”兼”定理証明支援系Leanの環境構築

Discussion