Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] 2 is Suc (Suc 0)?


view this post on Zulip Email Gateway (Feb 24 2022 at 01:32):

From: Li Yongjian <lyj238@gmail.com>
Dear experts:

I define a simple function add,

primrec add::"nat ⇒nat ⇒nat" where
"add x 0= x" |
"add x (Suc y) =Suc (add x y)"

But I can't prove the following lemmas.

lemma "add 5 2= 7"

lemma "add 7 2000= 2007"

So I want to ask what is the definition of a natural number 3, 2000?

regards
lyj

view this post on Zulip Email Gateway (Feb 24 2022 at 03:09):

From: Alex Weisberger <alex.m.weisberger@gmail.com>
Hello,

It looks to me like primrec doesn't add the function definition to the set
of simplification rules (many people refer to this as the "simp set").
Therefore the definition can't be used to find a proof by simplification.

You can add it explicitly in a couple of different ways depending on your
preference:

lemma "add 5 2 = 7"
by (simp add: add_def)

or

lemma "add 5 2 = 7" unfolding add_def by simp

An alternative is to use "fun" to define the function instead of "primrec"
since that will automatically add some simplification rules for this
function definition:

fun add::"nat ⇒nat ⇒nat" where
"add x 0= x" |
"add x (Suc y) = Suc (add x y)"

Surprisingly, that doesn't allow a proof by "auto" or "simp" directly. A
little sledgehammering and searching for relevant lemmas led to this:

lemma "add 5 2 = 7"
by (simp add: eval_nat_numeral)

I'm still not sure why auto or simpl wouldn't work directly in this case if
anyone can shed some light on that.

view this post on Zulip Email Gateway (Feb 24 2022 at 05:59):

From: Tobias Nipkow <nipkow@in.tum.de>
Numerals (2, 3, ...) are not Suc-terms but more efficient binary representations
that need to be converted into Suc-form first before equations that
pattern-match on Suc apply. The recommened rewrite rules for this conversion are
eval_nat_numeral or numeral_eq_Suc.
(In general it is not a good idea to unfold internal definitions like add_def if
add was defined by some other means than `definition').

Tobias
smime.p7s

view this post on Zulip Email Gateway (Feb 24 2022 at 07:42):

From: Li Yongjian <lyj238@gmail.com>
By my learning experience in Isabelle, primrec def should be unfolded
automatically?

Is it ture?

view this post on Zulip Email Gateway (Feb 24 2022 at 15:43):

From: Alex Weisberger <alex.m.weisberger@gmail.com>
I thought so as well. For what it's worth, the proof with the addition of
eval_nat_numeral works for the primrec definition as well:

lemma "add 5 2 = 7"
by (simp add: eval_nat_numeral)

So my initial suggestion about unfolding might have worked for a different
reason, the unfolding isn't required.

view this post on Zulip Email Gateway (Feb 24 2022 at 16:04):

From: Manuel Eberl <manuel@pruvisto.org>
Yes, "fun" and "primrec" both add the "simps" rules to the simpset
automatically. These (roughly) correspond to the equations that you
right down in your invocation of the "fun"/"primrec" command.

Technically, these are not the definition of the constant in HOL. A
definition is always a single equation of the form "myconst = …". For
"primrec", the definition is in terms of the underlying datatype's
primitive recursion combinator and is somewhat readable. For "fun", the
definition is fairly technical and inaccessible with "normal" means for
good reason.

The problem here is, as was already said in similar words, that your
"simp" rules proceed by recursion on natural numbers with the
constructors "Suc" and "0". But if the argument is not in that form,
those rules cannot apply so the simplifier does nothing.

There are a number of solutions here:

  1. bring the argument into the "successor notation" form, e.g. by adding
    something like eval_nat_numeral to the simpset.

  2. prove alternative simplification rules that apply to your situation
    as well, e.g.

y > 0 ⟹ add x y = Suc (add x (y - 1))

or, specifically tailored to numerals,

lemma "add x (numeral y) = Suc (add x (pred_numeral y))"
  by (simp add: numeral_eq_Suc)

(see addendum below for explanation of this)

  1. use something like the "code_simp" tactic to evaluate your term. (not
    100% sure whether this uses any unverified code internally, but I don't
    think it does – unlike the similar and much more performant "eval" tactic)

lemma "add 5 2 = 7"
  apply code_simp

Manuel

To understand this, you have to know how numerals work in Isabelle. I'm
not sure if this is actually documented anywhere. You can look at the
HOL.Num theory – the basic idea is fairly simple: we have a datatype
"num" representing positive binary numbers (with constructors One, Bit0,
Bit1), and the "numeral" function converts between "num" and e.g.
natural numbers. Some parsing/printing magic then makes things so that
you can write "5" in HOL and what's actually there is "numeral (Bit1
(Bit0 One))"

The only remaining ingredient here is that there is a function
"pred_numeral :: num ⇒ 'a" that works like "numeral" except that it
gives you the predecessor. So "numeral n = 1 + pred_numeral n" holds
unconditionally. Of course, just writing "numeral n - 1" would also work
I think.

On 24/02/2022 16:43, Alex Weisberger wrote:

I thought so as well. For what it's worth, the proof with the addition
of eval_nat_numeral works for the primrec definition as well:

lemma "add 5 2 = 7"
  by (simp add: eval_nat_numeral)

So my initial suggestion about unfolding might have worked for a
different reason, the unfolding isn't required.

On Thu, Feb 24, 2022 at 2:42 AM Li Yongjian <lyj238@gmail.com> wrote:

By my learning experience in Isabelle, primrec def should be
unfolded automatically?

Is it ture?

On Thu, Feb 24, 2022 at 11:09 AM Alex Weisberger
<alex.m.weisberger@gmail.com> wrote:

Hello,

It looks to me like primrec doesn't add the function
definition to the set of simplification rules (many people
refer to this as the "simp set"). Therefore the definition
can't be used to find a proof by simplification.

You can add it explicitly in a couple of different ways
depending on your preference:

lemma "add 5 2 = 7"
  by (simp add: add_def)

or

lemma "add 5 2 = 7" unfolding add_def by simp

An alternative is to use "fun" to define the function instead
of "primrec" since that will automatically add some
simplification rules for this function definition:

fun add::"nat ⇒nat ⇒nat" where
"add x 0= x" |
"add x (Suc y) = Suc (add x y)"

Surprisingly, that doesn't allow a proof by "auto" or "simp"
directly. A little sledgehammering and searching for relevant
lemmas led to this:

lemma "add 5 2 = 7"
  by (simp add: eval_nat_numeral)

I'm still not sure why auto or simpl wouldn't work directly in
this case if anyone can shed some light on that.

On Wed, Feb 23, 2022 at 8:32 PM Li Yongjian <lyj238@gmail.com>
wrote:

Dear experts:
I define a simple function add,

primrec add::"nat ⇒nat ⇒nat" where
"add x 0= x" |
"add x (Suc y) =Suc (add x y)"

But I can't prove the following lemmas.

lemma "add 5 2= 7"

lemma "add 7 2000= 2007"

So I want to ask what is the definition of a natural
number 3,  2000?

regards
lyj


Last updated: Mar 28 2024 at 12:29 UTC