Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] conversions for symmetric/commutative operators

Email Gateway (Nov 09 2021 at 12:34):

From: Peter Gammie <peteg42@gmail.com>
Hello,

I find myself with a sea of conversions of the form exhibited by filter_empty_conv. HOL.List is missing its obvious friend:

lemma empty_filter_conv:
shows "([] = filter P xs) = (\<forall>x\<in>set xs. \<not> P x)"
by (induct xs) simp_all

which could also be derived via a rule of the form:

(x = y) = z ==> (y = x) = z

(and so forth for other symmetric or commutative operators such as inf and sup).

One could imagine defining an attribute symconv like symmetric to handle this:

lemmas empty_filter_conv = filter_empty_conv[symconv]

But in my ideal world I wouldn’t need to type this out and make up another name, but would instead bind both theorems to the same name, e.g.

lemma empty_filter_conv[symconv]:
shows "([] = filter P xs) = (\<forall>x\<in>set xs. \<not> P x)”
…

thm empty_filter_conv

([] = filter P xs) = (\<forall>x\<in>set xs. \<not> P x)
(filter P xs = []) = (\<forall>x\<in>set xs. \<not> P x)

However AIUI attributes map a single theorem to a single theorem, so this isn’t going to work.

All I can think of is to create another keyword like lemma that does a bit of post-processing before the binding is made. This feels a bit heavyweight.

Has anyone got a better solution? It might help to make these sorts of lemma pairs more systematic in the distribution.

cheers,
peter

Email Gateway (Nov 09 2021 at 13:28):

From: Peter Lammich <lammich@in.tum.de>
I second Peter that having attributes that create more than one lemma as
output may be a useful thing. I also often write things like [simp, THEN xxx,
simp], to register two simp rules derived from the same lemma.

Peter

Email Gateway (Nov 10 2021 at 07:27):

From: Tobias Nipkow <nipkow@in.tum.de>
Peter,

This is really funny, I was in the middle of implementing the first part of what
you suggested. There is now the lemma eq_iff_swap: (x = y) = P ==> (y = x) = P
and I have simplified a number of proofs in List as a result. I have also added
a handful of lemmas that were missing. Strangely enough, I missed your
empty_filter_conv. Or maybe I tried and it did more harm than good - it took a
couple of iterations to smooth things out. I'll double-check.

Note that one should not apply eq_iff_swap blindly: one may want to swap some
equations in P as well.

Tobias
smime.p7s

Email Gateway (Nov 13 2021 at 23:41):

From: Peter Gammie <peteg42@gmail.com>
Tobias,

Thanks for doing that. I’ll reiterate my concern that things aren’t particularly systematic. For instance we have this pair:

filter_eq_Cons_iff
Cons_eq_filter_iff

and this pair:

take_eq_Nil
take_eq_Nil2

Can we settle on:

• suffix _iff vs _conv vs nothing
• suffix 2 vs flipping the constant names around _eq_
• ...

As I remarked before, it’d be great if we could just have a single name for each of these pairs as the common case is that you just want to use whatever works (which in my case would give more robust proofs as I rework the foundations of things). In the rarer case that you need just one or the other I think e.g. filter_eq_Cons_iff(1) is not so bad.

Perhaps this is not typically an issue once the relevant simpset is sufficiently mature.

cheers,
peter

Email Gateway (Nov 14 2021 at 20:18):

From: Tobias Nipkow <nipkow@in.tum.de>
Peter,

I amy fine tune these names when I feel really bored, but not at this point in time.

Best
Tobias
smime.p7s

Last updated: Jul 15 2022 at 23:21 UTC