Email Gateway (Aug 19 2022 at 12:00): Email Gateway (Aug 19 2022 at 12:00):From: Christoph LANGE <math.semantic.web@gmail.com>
Dear Isabelle users,
I made another interesting observation. According to earlier experience
I will not call it "strange" or "bug", but merely "interesting" ;-)
have "(0::nat) ∈ ℕ" by simp -- works
have "(1::nat) ∈ ℕ" by simp -- doesn't work
have "(1::nat) ∈ ℕ" by (rule Nat.semiring_1_class.Nats_1) -- works, but
interestingly Nats_1 _is_ a simp rule
have "1 ∈ ℕ" by simp -- works
have "(666::nat) ∈ ℕ" by simp -- works
So it seems that statements of this pattern work for all natural
numbers, when given explicit type information, except for 1.
Let me briefly explain the background of my work. Any feedback on
whether my approach is reasonable is most welcome. As a part of our
soundness verification of auctions
(http://www.cs.bham.ac.uk/research/projects/formare/code/auction-theory/#sound-verif,
http://arxiv.org/abs/1308.1779,
https://github.com/formare/auctions/tree/master/isabelle/Auction), I'd
like to prove that the functions that describe certain auctions (e.g.
that compute the price someone has to pay) are well-defined. At the
very least this means that the functions are total on the set of
possible inputs (i.e. bids that bidders place on goods). Now, in
Isabelle/HOL, functions are always total in a trivial sense, and I think
I don't want to use explicit partial functions.
So I thought the following approach should work: given a function
f::"nat ⇒ nat", I prove that for any concrete natural number (Is there a
better word than "concrete"?) the function returns a concrete value.
I.e. "⋀ x . x ∈ ℕ ⟹ f x ∈ ℕ", or, using the terminology of FuncSet, "f ∈
ℕ → ℕ".
Does this make sense?
Cheers, and thanks in advance,
Christoph
Email Gateway (Aug 19 2022 at 12:00):From: Tobias Nipkow <nipkow@in.tum.de>
You can prove "(n::nat) : Nats", which shows you that Nats is just the set of
all natural numbers. Nats is polymrphic and only becomes useful when it
describes the natural numbers as a subset of some other numeric type.
Your proof attempt will just lead to trivial goals that don't tell you anything:
any term n::nat is equal to some concrete natural number built up from 0 and Suc
simply because that is how nat is defined. What you probably have in mind is the
following: you want to prove that for any concrete n::nat you can prove "f n =
m" for some concrete m - and the proof should only use the equations defining f
and the functions it is based on. That is not possible, because you cannot
restrict deduction to some sublogic.
Tobias
Email Gateway (Aug 19 2022 at 12:00):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Christoph,
I'll add specific details of why `have "(1::nat) ∈ ℕ" by simp' doesn't work.
First, 0 and 1 are special, so you frequently have to do special things
to prove statements about 0 and 1.
I use this to look at all the typing in the output panel:
declare[[show_sorts=true]]
Along with this to see what simp rules are getting used:
declare[[simp_trace=true]]
For the formula "1 \<in> \<nat>", 1 is type 'a and \<nat> is ('a set),
so "1 \<in> \<nat>" is not the same statement as "(1::nat) \<in> \<nat>".
The simp trace for "(1::nat) \<in> \<nat>" by simp shows that the only
simp rule used is One_nat_def, which rewrites 1 as (Suc 0).
In Nat.thy, these two simp rules are on the following lines:
(Line 0186) One_nat_def [simp]: "1 = Suc 0"
(Line 1467) lemma Nats_1 [simp]: "1 ∈ ℕ"
The order that simp rules are declared is not always followed by the
simplifier. For example, permutative rewrite rules take precedence. But
much of the time, I've found that simp rules are applied in the order in
which they are declared.
So, One_nat_def converts 1 to "Suc 0" first. The simp rule Nats_1 is
then not applicable.
Try this:
theorem "(1::nat) \<in> \<nat>"
by(simp del: One_nat_def)
Regards,
GB
Email Gateway (Aug 19 2022 at 12:00):From: Christoph LANGE <math.semantic.web@gmail.com>
Thanks, Tobias and Gottfried!
Thanks, Tobias, for preventing me from wasting a lot of time proving
trivial results.
2013-09-12 13:48 Tobias Nipkow:
What you probably have in mind is the
following: you want to prove that for any concrete n::nat you can prove "f n =
m" for some concrete m - and the proof should only use the equations defining f
and the functions it is based on. That is not possible, because you cannot
restrict deduction to some sublogic.
Indeed that's what I had in mind. Luckily there are still other
interesting properties of my functions f, which I can and will prove.
2013-09-12 14:30 Gottfried Barrow:
I use this to look at all the typing in the output panel:
declare[[show_sorts=true]]Along with this to see what simp rules are getting used:
declare[[simp_trace=true]]
Thanks for pointing out, and for explaining the background!
Cheers,
Christoph
Email Gateway (Aug 19 2022 at 12:00):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Thanks for the info. One can make the wrong correlation about simple
things. If I look at the simp rules I've made, I'll probably see that I
usually create basic equivalencies first, and then more complex
equivalencies, which results in their order being followed.
To others, I should point out that many prefer the CNTL-hover method of
getting typing information for a term, and that
"declare[[show_sorts=true]" will interfere with the CNTL-hover method:
http://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-February/msg00002.html
I like to see all the typing at once for a complete formula, so I use
the "declare" method.
Regards,
GB
Last updated: Apr 19 2024 at 08:19 UTC