Re: [isabelle] conversions for symmetric/commutative operators



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

> On 10 Nov 2021, at 16:57, Tobias Nipkow <nipkow at in.tum.de> wrote:
> 
> 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
> 
> On 09/11/2021 13:34, Peter Gammie wrote:
>> 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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.