Re: [isabelle] Non-idempotence of datatype constructors



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.