8.5. Terminal vs Non-Terminal Positions
To write maintainable proofs, avoid using The The simp
without Lean.Parser.Tactic.simp : tactic
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.-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
unless it closes the goal.
Such uses of simp
that do not close a goal are referred to as non-terminal simps.
This is because additions to the default simp set may make simp
more powerful or just cause it to select a different sequence of rewrites and arrive at a different simp normal form.
When Lean.Parser.Tactic.simp : tactic
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.-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
is specified, additional lemmas will not affect that invocation of the tactic.
In practice, terminal uses of simp
are not nearly as likely to be broken by the addition of new simp lemmas, and when they are, it's easier to understand the issue and fix it.
When working in non-terminal positions, The simp?
(or one of the other simplification tactics with ?
in their names) can be used to generate an appropriate invocation withLean.Parser.Tactic.simp : tactic
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.-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
.
Just as apply?
or rw?
suggest the use of relevant lemmas, simp?
suggests an invocation of simp
with a minimal simp set that was used to reach the normal form.
Using simp?
The non-terminal simp?
in this proof suggests a smaller simp
with Lean.Parser.Tactic.simp : tactic
only
:
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! 🐙
The suggested rewrite is:
Try this: simp only [Array.size_toArray, List.length_cons, List.length_singleton, Nat.reduceAdd]
which results in the more maintainable proof:
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! 🐙