このようなコードをLean Proverで検査しようとすると、補題test2でエラーが出る。1
いくら考えても原因がわからなかったのでGitHubのレポジトリにバグとして報告したところ、バグではなく仕様である、という返答を頂いた。 github.com
ここに書いてあることを要約する。constant t: Sort uと宣言すると、宇宙uごとに型t.{u}: Sort uができ、constant f: t -> tという宣言によって、 宇宙のペアu,vそれぞれに対しf.{u v}: t.{u} -> t.{v}ができる。
この状態でf x = f xという式の型付けおよび型検査を行うと、もっとも一般的な型付けは@eq.{v} t.{v} (f.{u1 v} x.{u1}) (f.{u2 v} x.{u2})である(v,u1,u2は宇宙、返答にあるものとは名前を変えている)。等式の左右で型が等しいという条件はあるが、中身の関数およびその引数の型が等しいという条件はないことに注意。変数f, xのパラメータとなる宇宙が違うため、両辺が構文的に等しくなくなってしまい、reflexivity tacticが失敗したのである。(補題testではreflexivityが成功するが、これはx = xの型付けを行うと@eq.{u} t.{u} x.{u} x.{u}となるためである。)
この問題の解決法は2種類ある。1つ目はissueの返答にも書いてあるように、universe polymorphismを使うのをやめ、t: Typeと宣言することである。もう一つは、universe polymorphismを使うが、問題となる全ての変数について、それのパラメータとなっている宇宙を指定することである。例えば以下のコードは正しく検査される。
gist.github.com
なお、この手の問題を解決するには、pretty printingの設定を変えるのが有効である。set_option pp.all trueを実行すれば、エラーメッセージやgoalの表示などで詳細な情報を表示してくれる。
-
実は
lemmaではなくexampleとして証明するとエラーが出ない。原因は不明である。set_option pp.all trueを使ってもよく分からない。↩
