Isabelle中常规代数恒等式自动化验证的问题咨询

Let’s dive into your questions about getting Isabelle to automatically prove basic algebraic identities—this is a super common sticking point when you’re first learning the tool, so you’re not alone here.

Why simp Fails for n*(n+1) = n^2 + n #

The simp tactic only uses rules from its predefined simpset—a curated list of rewrite rules that Isabelle applies to simplify terms. By default, this set doesn’t include power2_eq_square, the rule that turns n^2 into n*n.

Your lemma has n^2 on the right-hand side, which the default simpset doesn’t automatically expand to multiplication. When you add power2_eq_square, you’re giving Isabelle the missing piece: once n^2 becomes n*n, the distributive rules already in the simpset kick in to rewrite n*(n+1) to n*n + n, making both sides match.

The Head-Scratching Difference Between n*(n+2) and n*(n+3) #

This one is tricky, but it boils down to how Isabelle’s default simpset handles small numerals vs. larger ones:

• For n*(n+2), the built-in simplifications recognize the pattern and apply distributivity implicitly—this is part of Isabelle’s optimized handling of common linear arithmetic cases with small constants.
• For n*(n+3), the default simpset doesn’t trigger distributivity automatically. You need to explicitly include distrib_left (or use a tactic that calls it) to get the rewrite to happen.

Think of it like this: the default simpset is built to be fast first, powerful second. Enabling every possible algebraic rule by default would slow down simplification for more complex proofs, so it only includes the most universally useful rules out of the box.

Can We Automate These Identities? #

Absolutely—you just need to use the right tactics or tweak your simpset:

• Use specialized arithmetic tactics: Instead of relying on simp, try arith or algebra (from the HOL-Algebra library). These are purpose-built to handle basic ring/field arithmetic automatically. For example:

  lemma fixes n::nat shows "n*(n+1) = n^2 + n" by arith
  lemma fixes n::nat shows "n*(n+3) = n*n + n*3" by arith
  

• Extend the simpset explicitly: If you want simp to handle these cases by default, you can add the necessary rules to your simpset for a single proof or globally. For a one-off proof:

  lemma fixes n::nat shows "n*(n+1) = n^2 + n" 
    using [[simproc add: power2_eq_square distrib_left]] by simp
  

  To make these rules permanent (note: be careful with this—overloading the simpset can cause unexpected behavior in complex proofs):

  declare power2_eq_square [simp]
  declare distrib_left [simp]
  

Why Isn’t This Automatic Out of the Box? #

There are a few key technical reasons Isabelle doesn’t enable all these rules by default:

• Efficiency: The simpset is a balance between power and speed. Loading every possible algebraic rule would make simplification slower, especially for large or nested terms. Isabelle prioritizes rules that give the most bang for the buck without adding excessive overhead.
• Type specificity: Algebraic rules behave differently across types (e.g., natural numbers vs. integers vs. reals). The default simpset can’t assume you want all ring rules enabled for every type—you need to tailor the rules to your specific context.
• Avoiding infinite loops: Some rewrite rule pairs can cause circular simplifications. For example, if you enabled both power2_eq_square (turning n^2 to n*n) and its reverse (turning n*n to n^2), the simp tactic could loop forever. The default simpset avoids such pairs to prevent this kind of chaos.

内容的提问来源于stack exchange，提问作者Ignorabimus