8.1. 単純化器の呼び出し（Invoking the Simplifier）🔗

8.1.1. パラメータ（Parameters）

単純化タクティクは以下のような文法を持ちます：

tactic ::= ...
    | The `simp` tactic uses lemmas and hypotheses to simplify the main goal target or
non-dependent hypotheses. It has many variants:
- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.
- `simp [h₁, h₂, ..., hₙ]` simplifies the main goal target using the lemmas tagged
  with the attribute `[simp]` and the given `hᵢ`'s, where the `hᵢ`'s are expressions.-
- If an `hᵢ` is a defined constant `f`, then `f` is unfolded. If `f` has equational lemmas associated
  with it (and is not a projection or a `reducible` definition), these are used to rewrite with `f`.
- `simp [*]` simplifies the main goal target using the lemmas tagged with the
  attribute `[simp]` and all hypotheses.
- `simp only [h₁, h₂, ..., hₙ]` is like `simp [h₁, h₂, ..., hₙ]` but does not use `[simp]` lemmas.
- `simp [-id₁, ..., -idₙ]` simplifies the main goal target using the lemmas tagged
  with the attribute `[simp]`, but removes the ones named `idᵢ`.
- `simp at h₁ h₂ ... hₙ` simplifies the hypotheses `h₁ : T₁` ... `hₙ : Tₙ`. If
  the target or another hypothesis depends on `hᵢ`, a new simplified hypothesis
  `hᵢ` is introduced, but the old one remains in the local context.
- `simp at *` simplifies all the hypotheses and the target.
- `simp [*] at *` simplifies target and all (propositional) hypotheses using the
  other hypotheses.
simp Configuration options for tactics. optConfig only? ([ ((The simp lemma specification `*` means to rewrite with all hypotheses simpStar | An erasure specification `-thm` says to remove `thm` from the simp set simpErase | A simp lemma specification is:
* optional `↑` or `↓` to specify use before or after entering the subterm
* optional `←` to use the lemma backward
* `thm` for the theorem to rewrite with
simpLemma)),* ] )? (Location specifications are used by many tactics that can operate on either the
hypotheses or the goal. It can have one of the forms:
* 'empty' is not actually present in this syntax, but most tactics use
  `(location)?` matchers. It means to target the goal only.
* `at h₁ ... hₙ`: target the hypotheses `h₁`, ..., `hₙ`
* `at h₁ h₂ ⊢`: target the hypotheses `h₁` and `h₂`, and the goal
* `at *`: target all hypotheses and the goal
at A hypothesis location specification consists of 1 or more hypothesis references
and optionally `⊢` denoting the goal.
term*)?

言い換えれば、単純化タクティクの呼び出しは以下の修飾子を順番に取ります。またこれらはすべて任意です：

• 設定オプション 、呼び出される単純化器が simp のバージョンか dsimp のバージョンであるかに応じて、 Lean.Meta.Simp.Config か Lean.Meta.DSimp.Config のフィールドでなければなりません。

• Lean.Parser.Tactic.simp : tacticThe `simp` tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses. It has many variants: - `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`. - `simp [h₁, h₂, ..., hₙ]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `hᵢ`'s, where the `hᵢ`'s are expressions.- - If an `hᵢ` is a defined constant `f`, then `f` is unfolded. If `f` has equational lemmas associated with it (and is not a projection or a `reducible` definition), these are used to rewrite with `f`. - `simp [*]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and all hypotheses. - `simp only [h₁, h₂, ..., hₙ]` is like `simp [h₁, h₂, ..., hₙ]` but does not use `[simp]` lemmas. - `simp [-id₁, ..., -idₙ]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`, but removes the ones named `idᵢ`. - `simp at h₁ h₂ ... hₙ` simplifies the hypotheses `h₁ : T₁` ... `hₙ : Tₙ`. If the target or another hypothesis depends on `hᵢ`, a new simplified hypothesis `hᵢ` is introduced, but the old one remains in the local context. - `simp at *` simplifies all the hypotheses and the target. - `simp [*] at *` simplifies target and all (propositional) hypotheses using the other hypotheses. only 修飾子はデフォルトの simp セットを除外し、代わりに空の 厳密には、再帰的なケースを除外するために、simp セットは常に eq_self と iff_self を含みます。 simp セットから開始します。

• 補題リストは simp セットに補題を追加したり削除したりします。補題リストで補題を指定する方法は3つあります：

  • *、これは証明状態にあるすべての仮定を simp セットに追加します

  • - に続く補題はその simp セットから取り除かれます

  • 補題指定子、これは以下の順番で構成されます：

    • 任意の ↓ または ↑ はそれぞれ部分項を入力する前後に補題を適用します（↑ がデフォルト）。単純化された引数はより多くの規則を適用できることが多いため、単純化器は通常、親の項を単純化する前に部分項を単純化します；↓ によって親の項が部分項の単純化よりも優先的に単純化されます。

    • 任意の ← は等式の補題を左から右へではなく、右から左へ使うようにします。

    • 必須の補題で、simp セット名・補題名・項のいずれでも良いです。項はあたかも新しい名前の補題であるかのように扱われます。

• Lean.Parser.Tactic.simp : tacticThe `simp` tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses. It has many variants: - `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`. - `simp [h₁, h₂, ..., hₙ]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `hᵢ`'s, where the `hᵢ`'s are expressions.- - If an `hᵢ` is a defined constant `f`, then `f` is unfolded. If `f` has equational lemmas associated with it (and is not a projection or a `reducible` definition), these are used to rewrite with `f`. - `simp [*]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and all hypotheses. - `simp only [h₁, h₂, ..., hₙ]` is like `simp [h₁, h₂, ..., hₙ]` but does not use `[simp]` lemmas. - `simp [-id₁, ..., -idₙ]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`, but removes the ones named `idᵢ`. - `simp at h₁ h₂ ... hₙ` simplifies the hypotheses `h₁ : T₁` ... `hₙ : Tₙ`. If the target or another hypothesis depends on `hᵢ`, a new simplified hypothesis `hᵢ` is introduced, but the old one remains in the local context. - `simp at *` simplifies all the hypotheses and the target. - `simp [*] at *` simplifies target and all (propositional) hypotheses using the other hypotheses. at で始まる位置指定子で、これは位置の列から構成されます。位置は次のいずれかになります：

• 仮定の名前、これはその型が単純化されるべきであることを示します

• アスタリスク *、すべての仮定と結論が単純化されることを示します

• ターンスタイル ⊢、結論を単純化する必要があることを示します

デフォルトでは結論だけが単純化されます。