Re: [isabelle] Non-idempotence of datatype constructors



True, but after your suggestion, I realised that the solution with the
"proper subexpression" relation (or, alternatively, the size function)
combined with a simproc that produces these theorems on the spot is
actually the superior approach in every respect. It's simpler, more
general, and probably more performant.

I can try to come up with a proof-of-concept implementation using the
size function approach, since that needs no additional new features from
the BNF package.

Manuel


On 02/05/2020 16:16, Tobias Nipkow wrote:
> A first version which only deals with depth 1 would already cover most
> of the practical cases.
> 
> Tobias
> 
> On 02/05/2020 15:50, Manuel Eberl wrote:
>> That sounds like a good idea.
>>
>> However, if such a simproc is to work for any nesting of
>> constructors,having pre-proven theorems for every constructor will not
>> be enough.Instead, I suppose one would have to introduce a
>> "proper-subexpression"relation for datatypes (e.g. xs < Cons x xs) along
>> with a proof thatthis relation has the obvious properties (irreflexive,
>> asymmetric,transitive).
>>
>> I guess that is something that only a datatype package plugin similar
>> tothe one for the "size" function could provide. Having looked at the
>> codebriefly, I think only the people who wrote the BNF package could (or
>> atleast should) implement that.
>>
>> Alternatively, one could just use the size function (as someone
>> alreadysuggested in this thread) to get pretty much the same thing,
>> except thatit won't work for all datatypes (e.g. infinitely branching
>> ones).
>>
>> Manuel
>>
>>
>> On 02/05/2020 15:36, Tobias Nipkow wrote:
>>> I do think such rules are useful, esp if they are there by default. I
>>> suggest they are best handled by a simproc that is triggered by any
>>> "(=)" but that checks immediately if the two argumenst are of the
>>> appropriate type and form. That can be done very quickly (there are
>>> similar simprocs already). The simproc should work for any datatype and
>>> any degree of nesting of the constructors.
>>>
>>> Tobias
>>>
>>>
>>> On 01/05/2020 22:51, Manuel Eberl 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
>>>>
>>>
>>
> 




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