Lean4のType*で迷ったのでメモ

Lean4とMathlib4の勉強中にType*というワードに出会いました。初歩的な事かもしれませんが、この意味を調べるのに手間取ったので備忘録としてメモを残そうと思います。

バージョン

leanprover/lean4:v4.13.0-rc3

Type*について

Type*には以下のページで遭遇しました。

Lean4にはType 1やType 2、Type 3といった型があるので、Type*はこれらを一般化した型だと予想できそうです。
この詳細を調べようと思ったのですが、そのままType*と検索しても記号の*がワイルドカードとして扱われてしまうのでほしい結果が得られません。

一応、"Lean Type star"とか"Lean Type asterisk"で検索してみましたが、見つかりませんでした。

もう少し広く"Lean Type"で検索してみると、ようやくそれらしいドキュメントがありました。

Type 1やType 2の一般化で大体合っているようです。

constantについて

ただ、こちらのドキュメントは内容が古いようで、掲載されているサンプルコードをローカルで試してみてもエラーとなってしまいました。

サンプルコード

constant α : Type _
#check α

constant β : Type*
#check β

Lean Infoview

All Messages (4)
Temp.lean:1:0
unexpected identifier; expected command
Temp.lean:2:7
unknown identifier 'α'
Temp.lean:4:11
unexpected token ':'; expected command
Temp.lean:5:7
unknown identifier 'β'

constantはLean3のキーワードで、Lean4では削除されたようです。
この辺の違いが、Lean初学者にとっては難しいですね。

代わりにaxiomを使えと書いてあるので、そのように書き換えてみます。

サンプルコード（修正後）

axiom α : Type _
#check α

axiom β : Type*
#check β

Lean Infoview

All Messages (3)
Temp.lean:2:0
α.{u_1} : Type u_1
Temp.lean:4:15
unexpected token '#check'; expected term
Temp.lean:5:7
unknown identifier 'β'

ダメなんかい。

最初にType*と出会ったコードを参考に確認用のコードを作ってみます。

import Mathlib.Topology.Algebra.Valued.ValuedField
variable (Fq F : Type*) [Field Fq] [Field F]
#check Fq

Lean Infoview

All Messages (1)
temp.lean:3:0
Fq : Type u_1

これはうまく動きました。
Type*だけではダメなようです。

Mathlib.Tactic.TypeStarについて

頑張って色々調べてみたところ、Mathlib.Tactic.TypeStarがimportされている必要があるようです。

"Type star"では検索に出ませんでしたが、"TypeStar"だと出ました……。

上の例ではMathlib.Topology.Algebra.Valued.ValuedFieldの中でMathlib.Tactic.TypeStarがimport済みだったので、エラーが出なかったようです。

改めてサンプルコードを修正して確認してみます。

サンプルコード（修正後その2）

import Mathlib.Tactic.TypeStar

axiom α : Type _
#check α

axiom β : Type*
#check β

Lean Infoview

All Messages (2)
temp.lean:4:0
α.{u_1} : Type u_1
temp.lean:7:0
β.{u_1} : Type u_1

エラーは発生せず、無事にβの型を確認できました。