proof - リーンプルーフアシスタントにおける可換環の冪等

Question

こんにちは、リーン証明アシスタントで数学を実行して、それがどのように機能するかを確認しようとしています。私は、可換環の冪等性で遊ぶのは楽しいはずだと判断しました。これが私が試したことです：

variables (A : Type) (R : comm_ring A)
definition KR : Type := \Sigma x : A, x * x = x

その後、エラーが発生します

failed to synthesize placeholder
A : Type,
x : A
⊢ has_mul A

リーンは A が環であることを忘れていたようですね?

たとえば、定義を次のように変更すると、

definition KR (A : Type) (R : comm_ring A) :  Type := Σ x : A , x = x * x

その後、すべてが順調です。しかし、これは余分な簿記データを持ち歩かなければならないことを意味します。簿記を維持する必要性を回避するために変数を使用する方法はありますか。

score 2 · Accepted Answer

デフォルトでは、Lean はセクション変数とパラメーターを実際に使用する定義にのみ含めます。includeこれは、コマンドとコマンドでオーバーライドできますomit。しかし、comm_ringは型クラスであるため、クラス推論パラメーターとして宣言することをお勧めします。

variables (A : Type) [comm_ring A]

このようにパラメーターの名前を省略すると、デフォルトですべての定義に含まれるため、その定義で機能するはずです。

1 に答える 1