8.5. 終端・非終端位置（Terminal vs Non-Terminal Positions）
メンテナンス可能な証明を書くためには、 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 のこのような使用は 非終端 simp （non-terminal simp）と呼ばれます。これはデフォルト 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.
only が指定されている場合、追加の補題はタクティクのその呼び出しに影響しません。実際には 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.
only で適切な呼び出しを生成することができます。ちょうど apply? や rw? が関連する補題の使用を提案するように、 simp? は正規形に到達するために使用された最小の simp セットでの 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.
only を伴ったより小さい simp を示唆します：
example (xs : Array Unit) : xs.size = 2 → xs = #[(), ()] := xs:Array Unit⊢ xs.size = 2 → xs = #[(), ()]
xs:Array Unita✝:xs.size = 2⊢ xs = #[(), ()]
xs:Array Unita✝:xs.size = 2⊢ xs.size = #[(), ()].size
xs:Array Unita✝:xs.size = 2⊢ xs.size = 2
All goals completed! 🐙
Try this: simp only [Array.size_toArray, List.length_cons, List.length_singleton, Nat.reduceAdd]
これはよりメンテナンス可能な証明になります：
example (xs : Array Unit) : xs.size = 2 → xs = #[(), ()] := xs:Array Unit⊢ xs.size = 2 → xs = #[(), ()]
xs:Array Unita✝:xs.size = 2⊢ xs = #[(), ()]
xs:Array Unita✝:xs.size = 2⊢ xs.size = #[(), ()].size
xs:Array Unita✝:xs.size = 2⊢ xs.size = [].length + 1 + 1
All goals completed! 🐙