14.1. カスタム演算子（Custom Operators）🔗

Lean はカスタムの中置・前置・後置演算子をサポートしています。新しい演算子はどの Lean ライブラリでも追加することができ、新しい演算子は言語の一部である演算子と同等の地位を持ちます。新しい演算子にはそれぞれ関数としての解釈が割り当てられ、演算子の使用は関数の使用に変換されます。演算子の関数呼び出しへの変換は 展開 （expansion）と呼ばれます。この関数が 型クラス の メソッド である場合、そのクラスのインスタンスを定義することで、結果の演算子をオーバーロードすることができます。

すべての演算子は 優先順位 （precedence）を持ちます。演算子の優先順位は括弧を持たない式の演算順序を決定します：乗算は加算よりも優先順位が高いため、 2 + 3 * 4 は 2 + (3 * 4) と同値であり、 2 * 3 + 4 は (2 * 3) + 4 と同値です。中置演算子はさらに 結合性 （associativity）を持ち、同じ優先順位を持つ演算子の連鎖の意味を決定します：

左結合 （Left-associative）

これらの演算子は左に入れ子になります。加算は左結合であるため、 2 + 3 + 4 + 5 は ((2 + 3) + 4) + 5 と同値です。

右結合 （Right-associative）

これらの演算子は右に入れ子になります。直積型は右結合であるため、 Nat × String × Unit × Option Int は Nat × (String × (Unit × Option Int)) と同値です。

非結合 （Non-associative）

これらの演算子を連鎖させると構文エラーになります。明示的な括弧が必要です。等式は非結合であるため、以下はエラーになります：

1 + 2 = 3 expected end of input= 2 + 1

The parser error is:

<example>:1:10: expected end of input
前置・中置演算子の優先順位

命題 ¬A ∧ B は ¬ が ∧ よりも優先順位が高いため (¬A) ∧ B と同値です。∧ は = よりも優先順位が高く、また右結合であるため、 ¬A ∧ B = (¬A) ∧ B は ¬A ∧ ((B = ¬A) ∧ B) と同値です。

Lean は新しい演算子を定義するためのコマンドを提供しています：

syntax

非結合中置演算子は Lean.Parser.Command.mixfix : commandinfix で定義されます：

command ::= ...
    | A `docComment` parses a "documentation comment" like `/-- foo -/`. This is not treated like
a regular comment (that is, as whitespace); it is parsed and forms part of the syntax tree structure.

A `docComment` node contains a `/--` atom and then the remainder of the comment, `foo -/` in this
example. Use `TSyntax.getDocString` to extract the body text from a doc string syntax node. docComment?
      attributes?
      `attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`. attrKind infix:prec ((name := ident))? ((priority := prio))? str => term

左結合中置演算子は Lean.Parser.Command.mixfix : commandinfixl で定義されます：

command ::= ...
    | A `docComment` parses a "documentation comment" like `/-- foo -/`. This is not treated like
a regular comment (that is, as whitespace); it is parsed and forms part of the syntax tree structure.

A `docComment` node contains a `/--` atom and then the remainder of the comment, `foo -/` in this
example. Use `TSyntax.getDocString` to extract the body text from a doc string syntax node. docComment?
      attributes?
      `attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`. attrKind infixl:prec ((name := ident))? ((priority := prio))? str => term

右結合中置演算子は Lean.Parser.Command.mixfix : commandinfixr で定義されます：

command ::= ...
    | A `docComment` parses a "documentation comment" like `/-- foo -/`. This is not treated like
a regular comment (that is, as whitespace); it is parsed and forms part of the syntax tree structure.

A `docComment` node contains a `/--` atom and then the remainder of the comment, `foo -/` in this
example. Use `TSyntax.getDocString` to extract the body text from a doc string syntax node. docComment?
      attributes?
      `attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`. attrKind infixr:prec ((name := ident))? ((priority := prio))? str => term

前置演算子は Lean.Parser.Command.mixfix : commandprefix で定義されます：

command ::= ...
    | A `docComment` parses a "documentation comment" like `/-- foo -/`. This is not treated like
a regular comment (that is, as whitespace); it is parsed and forms part of the syntax tree structure.

A `docComment` node contains a `/--` atom and then the remainder of the comment, `foo -/` in this
example. Use `TSyntax.getDocString` to extract the body text from a doc string syntax node. docComment?
      attributes?
      `attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`. attrKind prefix:prec ((name := ident))? ((priority := prio))? str => term

後置演算子は Lean.Parser.Command.mixfix : commandpostfix で定義されます：

command ::= ...
    | A `docComment` parses a "documentation comment" like `/-- foo -/`. This is not treated like
a regular comment (that is, as whitespace); it is parsed and forms part of the syntax tree structure.

A `docComment` node contains a `/--` atom and then the remainder of the comment, `foo -/` in this
example. Use `TSyntax.getDocString` to extract the body text from a doc string syntax node. docComment?
      attributes?
      `attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`. attrKind postfix:prec ((name := ident))? ((priority := prio))? str => term

これらのコマンドの前には documentation comments と attributes を付けることができます。ドキュメントコメントはユーザが演算子の上にマウスを置くと表示され、属性は他の宣言と同様に任意のメタプログラムを呼び出すことができます。 inherit_doc 属性は演算子を実装する関数のドキュメントを演算子自身に再利用させます。

演算子は属性と同じように、 セクションスコープ と相互作用します。デフォルトでは、記法はそれが確立されたモジュールをインポートした任意のモジュールで遷移的に利用可能です。しかし、scoped または local と宣言することで、それぞれ現在の名前空間が開かれているコンテキストか、現在の セクションスコープ に限定することができます。

カスタム演算子には、コロンに続く 優先順位 指定子が必要です。カスタム演算子にはデフォルトの優先順位はありません。

演算子には明示的に名前を付けることができます。この名前は Lean の構文の拡張を表し、主にメタプログラミングに使用されます。名前が明示的に与えられない場合、Lean は演算子に基づいて名前を生成します。この名前の割り当ての特定に頼るべきではありません。なぜなら内部的な名前の割り当てアルゴリズムは変更される可能性があり、また上流の依存関係で似たような演算子が導入されると衝突する可能性があるからです。このような場合、Lean は名前が一意になるまで名前の割り当てを変更します。

演算子の名前の割り当て

この中置演算子に対して：

infix:90 " ⤴ " => Option.getD

内部的な名前 «term_⤴_» が結果のパーサ拡張に割り当てられます。

演算子名の提供

この中置演算子に対して：

infix:90 (name := getDOp) " ⤴ " => Option.getD

結果のパーサ拡張は getDOp と命名されます。

ドキュメントの継承

この中置演算子に対して：

@[inherit_doc] infix:90 " ⤴ " => Option.getD

結果のパーサ拡張は Option.getD と同じドキュメントを持ちます。

同じ構文を持つ演算子が複数定義されている場合、Lean のパーサはそのすべてを試行します。複数の演算子が成功した場合、最も多くの入力を使用したものが選択されます。これは ローカル最長一致規則 （local longest-match rule）と呼ばれます。場合によっては、複数の演算子のパースが成功し、すべての演算子が同じ入力範囲をカバーすることがあります。この場合、演算子の 優先度 を使用して適切な結果が選択されます。最後に、同じ優先度を持つ複数の演算子が最長一致で並んだ場合、パーサはすべての結果を保存し、エラボレータは順番にそれぞれを試行し、そのうちの正確に1つのみがエラボレーションに成功しなかった場合失敗します。

あいまいな演算子と優先度

Or としての + の代替実装を定義するには中置演算子宣言だけが必要です。

infix:65 " + " => Or

この宣言によって、Lean は HAdd.hAdd の組み込み構文と Or の新しい構文の両方を使用して加算をエラボレートしようと試みます：

True + False : Prop#check True + False 
True + False : Prop
2 + 2 : Nat#check 2 + 2 
2 + 2 : Nat

しかし、新しい演算子は結合的ではないため、 ローカル最長一致規則 から HAdd.hAdd だけが括弧を用いない3引数バージョンに適用されることが導かれます：

#check failed to synthesize HAdd Prop Prop ?m.38 Additional diagnostic information may be available using the `set_option diagnostics true` command.True + False + True 
failed to synthesize
  HAdd Prop Prop ?m.38
Additional diagnostic information may be available using the `set_option diagnostics true` command.

中置演算子が高い優先度で宣言された時、Lean はあいまいなケースで組み込みの HAdd.hAdd 演算子を試行しません：

infix:65 (priority := high) " + " => Or True + False : Prop#check True + False 
True + False : Prop
sorry + sorry : Prop#check failed to synthesize OfNat Prop 2 numerals are polymorphic in Lean, but the numeral `2` cannot be used in a context where the expected type is Prop due to the absence of the instance above Additional diagnostic information may be available using the `set_option diagnostics true` command.2 + failed to synthesize OfNat Prop 2 numerals are polymorphic in Lean, but the numeral `2` cannot be used in a context where the expected type is Prop due to the absence of the instance above Additional diagnostic information may be available using the `set_option diagnostics true` command.2 
failed to synthesize
  OfNat Prop 2
numerals are polymorphic in Lean, but the numeral `2` cannot be used in a context where the expected type is
  Prop
due to the absence of the instance above
Additional diagnostic information may be available using the `set_option diagnostics true` command.

新しい演算子は結合的ではないため、 ローカル最長一致規則 から HAdd.hAdd だけが括弧を用いない3引数バージョンに適用されることが導かれます：

#check failed to synthesize HAdd Prop Prop ?m.20 Additional diagnostic information may be available using the `set_option diagnostics true` command.True + False + True 
failed to synthesize
  HAdd Prop Prop ?m.20
Additional diagnostic information may be available using the `set_option diagnostics true` command.

実際の演算子は文字列リテラルによって指定されます。新しい演算子は以下の要件を満たす必要があります：

  • 最低1文字を含む

  • 演算子が '' でない限り、最初の文字はシングル・ダブルクォート（' または "）であってはなりません。

  • バックティック（​`​）で始まり、その後に quote された名前として有効な接頭辞である文字を続けてはなりません。

  • 数値から始まってはいけません。

  • 内部に空白を含んではいけません。

演算子の文字列リテラルはスペースで開始・終了することがあります。これらは演算子の一部ではないため、スペースがあっても演算子の使用時にスペースを入れる必要はありません。しかし、スペースがあると、Lean は演算子をユーザに表示する際にスペースを挿入します。スペースを省略すると、演算子の引数が演算子のすぐ隣に表示されます。

最後に、演算子の意味を Lean.Parser.Command.mixfix : command=> で区切って指定します。これは Lean のどんな項でも構いません。演算子の使用は提供された項が関数の位置にある関数適用に脱糖されます。前置・後置演算子は明示的な引数として、その項を単一の引数に適用します。中置演算子は引数を左右の順に項を適用します。各呼び出し位置で引数を受け付けること以外に項に課される特別な要件はありません。演算子は関数を構築することができるため、項は演算子よりも多くのパラメータを期待することができます。暗黙と インスタンス暗黙 のパラメータは各適用位置で解決されるため、演算子は 型クラス の メソッド で定義することができます。

項がグローバル環境からの名前か、そのような名前を1つ以上の引数に適用したものである場合、Lean は自動的に演算子に unexpander を生成します。これは 証明状態 ・エラーメッセージ・その他の Lean からの出力にて、マッチする関数適用項が表示される場合に表示されます。Lean はもとの項がその演算子で使われていたかどうかを追跡しません；これは Lean の出力にていたるところで用いられます。

Lean の出力におけるカスタム演算子

関数 perhapsFactorial はあまり大きくない数値に対して階乗を計算します。

def fact : Nat → Nat | 0 => 1 | n+1 => (n + 1) * fact n def perhapsFactorial (n : Nat) : Option Nat := if n < 8 then some (fact n) else none

後置するインテロバング演算子を使って表現することができます。

postfix:90 "‽" => perhapsFactorial

∀ n, n ≥ 8 → (perhapsFactorial n).isNone を証明しようとすると、たとえそのように書かなかったとしても最初の証明状態では新しい演算子が使われます：

⊢ ∀ (n : Nat), n ≥ 8 → n‽.isNone = true