8.5. Terminal vs Non-Terminal Positions🔗

To write maintainable proofs, avoid using simp without Lean.Parser.Tactic.simp : 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.
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

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.
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, 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

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.
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 Unitxs.size = 2 → xs = #[(), ()] xs:Array Unita✝:xs.size = 2xs = #[(), ()] xs:Array Unita✝:xs.size = 2xs.size = #[(), ()].size xs:Array Unita✝:xs.size = 2xs.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 Unitxs.size = 2 → xs = #[(), ()] xs:Array Unita✝:xs.size = 2xs = #[(), ()] xs:Array Unita✝:xs.size = 2xs.size = #[(), ()].size xs:Array Unita✝:xs.size = 2xs.size = [].length + 1 + 1 All goals completed! 🐙