Email Gateway (Aug 23 2022 at 09:00): Email Gateway (Aug 23 2022 at 09:00):From: Miguel Pagano <miguel.pagano@gmail.com>
On Fri, 1 May 2020 at 17:59, Miguel Pagano <miguel.pagano@gmail.com> wrote:
On Fri, 1 May 2020 at 17:58, Richard Waldinger <waldinger@ai.sri.com>
wrote:isn’t the “size” theorem true for any function, not just size? or am i
missing something?It shouldn't be true for non-injective functions.
I'm embarrased, please discard my stupid answer.
On May 1, 2020, at 1:51 PM, Manuel Eberl <eberlm@in.tum.de> wrote:
Firstly, I don't think these theorem is especially useful. You might
have planned to add this to the simplifier, but its term net doesn't do
any magic here. It will end up checking every term that matches "Cons x
xs = ys" for whether "xs" can match "ys". I'm not sure if that matching
is equality, alpha-equivalent or unifiable.I honestly never think /that/ much about the performance implications of
simp rules (as long as they're unconditional). At least for lists, by
the way, this is already a simp rule by default though, and lists are
probably by far the most prevalent data type in the Isabelle universe.But you're certainly right that it would make sense to keep a look at
this performance impact if one wanted to add these to the simp set for
all datatypes by default, and I agree that the rules are probably not
helpful /that/ often. Still, it might be nice to have them available
nonetheless.Secondly, you can prove these theorems by using this handy trivial
theorem : "size x ~= size y ==> x ~= y". Apparently that theorem has
the
name Sledgehammer.size_ne_size_imp_ne - presumably the sledgehammer
uses it to prove such inequalities.It's even easier to prove it by induction. Plus, in fact, the "size"
thing only works if the data type even has a sensible size function.
That is not always the case, e.g. when you nest the datatype through a
function.My main point however is that when you have a datatype with a dozen
binary constructors, there's quite a bit of copying & pasting involved
before you've proven all those theorems. Since it can (probably) be
automated very easily, why not do that? Whether or not these should be
simp lemmas by default is another question.Manuel
Email Gateway (Aug 23 2022 at 09:07):From: Richard Waldinger <waldinger@AI.SRI.COM>
isn’t the “size” theorem true for any function, not just size? or am i missing something?
Email Gateway (Aug 23 2022 at 09:08):From: Manuel Eberl <eberlm@in.tum.de>
Yes, it is true for any function (even if it isn't injective, although
then it's not an "if-and-only-if").
The point is that if you actually want it to use this to prove that two
lists (or data type values in general) are not equal, you need to plug
in a concrete function f. And "size" happens to be one that is good for
this particular case.
Sometimes less general theorems can achieve more because they guide the
automation more (and us humans, too!). That is particularly true for
induction rules.
Manuel
Email Gateway (Aug 23 2022 at 09:09):From: Manuel Eberl <eberlm@in.tum.de>
Hey, don't worry about it. I had to think for a few seconds to be sure
myself.
A colleague of mine who shall not be named once spent an embarrassingly
long time trying to prove that the "fst" function is injective. ;)
Happens to all of us!
Manuel
Email Gateway (Aug 23 2022 at 09:12):From: Miguel Pagano <miguel.pagano@gmail.com>
On Fri, 1 May 2020 at 17:58, Richard Waldinger <waldinger@ai.sri.com> wrote:
isn’t the “size” theorem true for any function, not just size? or am i
missing something?It shouldn't be true for non-injective functions.
On May 1, 2020, at 1:51 PM, Manuel Eberl <eberlm@in.tum.de> wrote:
Firstly, I don't think these theorem is especially useful. You might
have planned to add this to the simplifier, but its term net doesn't do
any magic here. It will end up checking every term that matches "Cons x
xs = ys" for whether "xs" can match "ys". I'm not sure if that matching
is equality, alpha-equivalent or unifiable.I honestly never think /that/ much about the performance implications of
simp rules (as long as they're unconditional). At least for lists, by
the way, this is already a simp rule by default though, and lists are
probably by far the most prevalent data type in the Isabelle universe.But you're certainly right that it would make sense to keep a look at
this performance impact if one wanted to add these to the simp set for
all datatypes by default, and I agree that the rules are probably not
helpful /that/ often. Still, it might be nice to have them available
nonetheless.Secondly, you can prove these theorems by using this handy trivial
theorem : "size x ~= size y ==> x ~= y". Apparently that theorem has the
name Sledgehammer.size_ne_size_imp_ne - presumably the sledgehammer
uses it to prove such inequalities.It's even easier to prove it by induction. Plus, in fact, the "size"
thing only works if the data type even has a sensible size function.
That is not always the case, e.g. when you nest the datatype through a
function.My main point however is that when you have a datatype with a dozen
binary constructors, there's quite a bit of copying & pasting involved
before you've proven all those theorems. Since it can (probably) be
automated very easily, why not do that? Whether or not these should be
simp lemmas by default is another question.Manuel
Last updated: Apr 25 2024 at 16:19 UTC