Why do I have to use "numeral_nat" or "numeral.simps" when proving a simple computable equality of naturals in Isabelle

user_14656198 0
Viewed 80

Take this standard definition for the factorial function:

primrec factorial :: "nat ⇒ nat"
  where
    "factorial 0 = 1"
  | "factorial (Suc n) = (Suc n) * (factorial n)"

If we ask for value "factorial 3", Isabelle will predictably give us 6. However, if we try to make that a lemma, it'll fail:

lemma "factorial (3::nat) = (6::nat)"
  by simp
(* Failed to apply initial proof method *)

simp, auto, and even arith fail to find a solution. However, if we add numeral_nat or numeral.simps, simp can solve it:

lemma "factorial (3::nat) = (6::nat)"
  by (simp add: numeral_nat)

lemma "factorial (3::nat) = (6::nat)"
  by (simp add: numeral.simps)

Funnily enough, in both of these proofs Isabelle gives the warning "Ignoring duplicate rewrite rule", which means that it should already know about these. Furthermore, Isabelle has no problem proving that "3*2*1 = 6", which puzzles me even more about how these lemmas are being used.

So, if this is such a simple and easily computable equality - so much so that Isabelle can compute it with the value command - and these rules were apparently already present, why can't Isabelle solve the lemma without them?

isabelle
1 Answers

numeral_nat contains 7 lemmas:

thm numeral_nat
(*
  Numeral1 = Suc 0
  numeral (num.Bit0 ?n) = Suc (numeral (Num.BitM ?n))
  numeral (num.Bit1 ?n) = Suc (numeral (num.Bit0 ?n))
  Num.BitM num.One = num.One
  Num.BitM (num.Bit0 ?n) = num.Bit1 (Num.BitM ?n)
  Num.BitM (num.Bit1 ?n) = num.Bit1 (num.Bit0 ?n)
  1 = Suc 0
*)

while simp complains about 4 of them:

Ignoring duplicate rewrite rule:
Num.BitM num.One ≡ num.One 
Ignoring duplicate rewrite rule:
Num.BitM (num.Bit0 ?n1) ≡ num.Bit1 (Num.BitM ?n1) 
Ignoring duplicate rewrite rule:
Num.BitM (num.Bit1 ?n1) ≡ num.Bit1 (num.Bit0 ?n1) 
Ignoring duplicate rewrite rule:
1 ≡ Suc 0

Therefore, there are 7-4=3 new theorems. Tracing (see simp_trace) shows that numeral_nat(2,3) are the useful lemmas.

The idiomatic way is (numeral_eq_Suc is a bad simp rule in general):

lemma "factorial (3::nat) = (6::nat)"
  by (simp add: numeral_eq_Suc)

You might wonder why the expansion from 3 to Suc (Suc (Suc 0))) is actually necessary, because the definition is factorial (Suc n) = .... The answer in Isabelle is: only for 1. This is sufficient for most recursive functions and avoids a blow-up of the goal. Try

lemma "factorial (6::nat) = A" 
  apply (simp add: numeral_nat(2,3))

to see a blown-up goal.

Now value works very differently. It has three modes:

  1. value or value [code] (eval tactic) generated the Standard ML code and executes it. You trust the code equations and the compiler.
  2. value [nbe] (normalization tactic) is normalization by evaluation (also uses codes generation). "The stack of code to be trusted is considerable" (https://isabelle.in.tum.de/dist/Isabelle2021/doc/codegen.pdf)
  3. value [simp] (code_simp tactic) uses the simplifier. Fully trustable.

Even in the last case, the simplifier is called with specific parameters and theorems, not the default ones, like you did. Hence the difference.

user_128242070
Related