8.4. simp 正規形（Simp Normal Forms）🔗

デフォルト simp セット には simp でマークされたすべての定理と単純化手続きが含まれます。式の simp 正規形 （simp normal form）は、 simp タクティクによってデフォルトの simp セットを適用できる規則がなくなるまで適用した結果です。式が simp 正規形であると、デフォルト simp セットに従って可能な限り簡約されているため、多くの場合証明で作業しやすくなります。

simp タクティクは 合流性を保証しません 。つまり式の simp 正規形はデフォルト simp セットの要素が適用される順番に依存する可能性があります。 simp 属性を設定する際に優先度を割り当てることで規則の適用順序を変更することができます。

Lean ライブラリを設計する際には、ライブラリの演算子の様々な組み合わせに対して適切な simp 正規形とは何かを考えることが重要です。これはライブラリがデフォルト simp セットに追加するべき規則を選択する際の指針になります。特に、simp の補題の右辺は simp 正規形であるべきです；これによって単純化が停止することの保証が促進されます。さらに、ライブラリの各概念はたとえ等価な表現方法が複数あったとしても、1つの simp 正規形を通して表現されるべきです。ある概念が異なる simp の補題で2つの異なる方法で記述されている場合、単純化器がそれらを結び付けずに望ましい単純化が行われないことがあります。

単純化では必ずしも合流性を満たす必要はありませんが、合流性に近づけようとすることはライブラリをより予測しやすくし、simp の補題の欠落や不適切な選択を明らかにする傾向があるため有益です。デフォルト simp セットはライブラリがエクスポートする定数の型シグネチャと同様に、ライブラリのインタフェースの一部です。

ライブラリは、そのライブラリで定義されている少なくとも1つの定数に言及しない規則をデフォルト simp セットに追加すべきではありません。そうでなければ、ライブラリをインポートすることで無関係なライブラリの simp の挙動が変わってしまう可能性があります。ライブラリが他のライブラリからの定義や宣言に対する追加の単純化規則に依存している場合、カスタム simp セットを作成し、それを使用するようにユーザに指示するか、専用のタクティクを提供してください。