Re: [isabelle] Datatype definition can be slow



> "constructor_num x != constructor_num y ==> x != y"

That works in this very simple case where your datatype is just an
"enum"-like type. But in general, it should probably be something like

"constructor_num x != constructor_num y ==> x a b c != y d e"

because constructors, of course, can take parameters.


In any case, I don't think that works because you cannot really quantify
over constructors like this. In general, the constructors may not even
have the same type.

What I had in mind was that the simproc unfolds the internal
construction that the datatype uses and then proves the inequality from
that. I am not familiar with the details of that; there is probably a
little bit of overhead involved, but probably not too much.

Manuel



On 13/04/2021 18:06, Dominique Unruh wrote:
>> Somebody once voiced the possibility of making it possible to switch off
>> the simplification lemmas (e.g. for constructor distinctness, of which
>> there are quadratically many) and replace them by a simproc that proves
>> them ad-hoc whenever one of them is needed.
>> This would make applying the theorems slightly more expensive, but
>> eliminate the need to prove all of them beforehand.
>>
>> Not sure if this becomes enough of a problem to be worth it or if the
>> existing construction is fast enough for any reasonably-sized datatype.
> 
> Maybe the following approach would be nice:
> 
> Instead of generating pairwise inequalities, a function constructor_num
> is generated with the simp-rules "constructor_num A00 = 1"
> "constructor_num A01 = 2" "constructor_num A03 = 3" etc. (Where
> "constructor_num" is an overloaded function like size.)
> 
> Then we additionally add the simp-rule "constructor_num x !=
> constructor_num y ==> x != y". (For each datatype one instances because
> the generic one would loop. Or alternatively, have a no-assumptions type
> class for which that rule holds is added to the simplifier.)
> 
> Now I believe that this would be enough to decide inequalities the same
> way as simp can do now. (Haven't tested this.)
> 
> To avoid unnecessary simplifications, maybe add a cong-rule that forbids
> simplifications in the argument of constructor_num.
> 
> (Sorry if this is obvious and anyway what you had in mind for the inner
> workings of the simproc.)
> 
> Best wishes,
> Dominique.
> 
> 

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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