Email Gateway (Aug 19 2022 at 15:52): Email Gateway (Aug 19 2022 at 15:52):From: Gottfried Barrow <igbi@gmx.com>
Dmitriy (and Andreas),
On 14-09-02 01:01, Dmitriy Traytel wrote:
primrec has the option nonexhaustive, which hides the warning (works
for datatype_new only). Thus, we should add it to this declaration of
last. Thanks for reminding us.
And from your "Re: [isabelle] selector name in datatype_new causes proof
failure":
if no selector is specified for datatypes, there will be none
generated (a recent policy change)...
With "nonexhaustive", and with being able to define selector's in the
datatype definition, those two will get rid of most warnings that can
come from using underspecified functions. I switched my use of a "fun"
to an "abbreviation", which doesn't warn me about "the None", so that
gives me another way to get rid of warnings.
I kept using the query panel to try and find the "getter" functions for
a datatype, but I didn't see anything, so your comment above was useful,
and in going to look at "the" again, as an underspecified function, I
saw that it is now defined in the datatype defintion, which showed me
how to define a getter.
Andreas,
On 14-09-02 01:17, Andreas Lochbihler wrote:
Technically, you do not change the internal construction at all if you
add the missing cases with undefined on the right-hand side. The
function package does the same internally. With primrec, it is
slightly different, because primrec internally abstracts over the
other parameters and then uses undefined with a function type rather
than the parameters. So, if you pay attention to this, you do not
change what you can prove in Isabelle about your definitions.
I don't exactly know what "pay attention to this" means in regards to
"primrec", but I guess it means if I'm having proof problems when using
"primrec" and "undefined", then I can try to see if switching to "fun"
helps, since "fun" is doing what I'm doing".
However, from a modelling perspective, it can make a difference.
Modelling and semantics learning always stays at the end of the line,
but I worked through your example, and it reminded me how "undefined" is
concrete, in regards to existence and uniqueness for a particular type.
Thanks to the both of you,
GB
Email Gateway (Aug 19 2022 at 16:01):From: Gottfried Barrow <igbi@gmx.com>
Hi,
The canonical way in the HOL sources, when there's no need for a total
function, is to not cover all the cases, like "last", which is not
covered for []:
primrec last :: "'a list => 'a" where
"last (x # xs) = (if xs = [] then x else last xs)"
I've been doing that kind of thing, but it occurred to me that I could
put "undefined" to good use, to get rid of the warnings, like this:
datatype fooD = Bar | BarC "nat option"
fun BarC_get :: "fooD => nat" where
"BarC_get Bar = undefined"
|"BarC_get (BarC None) = undefined"
|"BarC_get (BarC (Some n)) = n"
Instead of like the above:
fun BarC_get2 :: "fooD => nat" where
"BarC_get2 (BarC (Some n)) = n"
Is there some, good, mysterious reason why I shouldn't do this to get
rid of the warnings?
Thanks,
GB
Email Gateway (Aug 19 2022 at 16:02):From: Dmitriy Traytel <traytel@in.tum.de>
Hi Gottfried,
On 02.09.2014 05:11, Gottfried Barrow wrote:
Hi,
The canonical way in the HOL sources, when there's no need for a total
function, is to not cover all the cases, like "last", which is not
covered for []:primrec last :: "'a list => 'a" where
"last (x # xs) = (if xs = [] then x else last xs)"
primrec has the option nonexhaustive, which hides the warning (works for
datatype_new only). Thus, we should add it to this declaration of last.
Thanks for reminding us.
I've been doing that kind of thing, but it occurred to me that I could
put "undefined" to good use, to get rid of the warnings, like this:datatype fooD = Bar | BarC "nat option"
fun BarC_get :: "fooD => nat" where
"BarC_get Bar = undefined"
|"BarC_get (BarC None) = undefined"
|"BarC_get (BarC (Some n)) = n"Instead of like the above:
fun BarC_get2 :: "fooD => nat" where
"BarC_get2 (BarC (Some n)) = n"Is there some, good, mysterious reason why I shouldn't do this to get
rid of the warnings?
No, I don't know one. At first I thought that in the latter case
"BarC_get Bar = BarC_get (BarC None)" would not be provable, but
Sledgehammer helped me out: by (metis BarC_get.elims fooD.distinct(1)
fooD.inject option.distinct(1)).
However, Nitpick also reported a non-spurious counterexample (empty
assignment), so I'm cc'ing Jasmin.
Dmitriy
Email Gateway (Aug 19 2022 at 16:03):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Gottfried,
Technically, you do not change the internal construction at all if you add the missing
cases with undefined on the right-hand side. The function package does the same
internally. With primrec, it is slightly different, because primrec internally abstracts
over the other parameters and then uses undefined with a function type rather than the
parameters. So, if you pay attention to this, you do not change what you can prove in
Isabelle about your definitions.
However, from a modelling perspective, it can make a difference. Say, you write the
following definition:
fun nth :: "nat => 'a list => 'a" where
"nth 0 (x # xs) = x"
| "nth (Suc n) (x # xs) = nth n xs"
| "nth n [] = undefined"
Then the last equation is part of the specification that fun exports for regular usage.
From a modelling point of view, all your theorems about nth then only apply to the real
world if whenever you access a list (think array) beyond its end, you get the same back no
matter how far you reach beyond the end. If you want to model array access in memory, this
is clearly unrealistic. Instead, if you omit the last equation (and do not pierce the veil
of abstraction that fun provides you - but there is currently no way to express this in
Isabelle), then you don't have this assumption about nth in your model.
Best,
Andreas
Last updated: Apr 25 2024 at 20:15 UTC