Re: [isabelle] Non-idempotence of datatype constructors



Two quick comments on this.


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.


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.


Best regards,

    Thomas.

________________________________
From: cl-isabelle-users-bounces at lists.cam.ac.uk <cl-isabelle-users-bounces at lists.cam.ac.uk> on behalf of Manuel Eberl <eberlm at in.tum.de>
Sent: Friday, May 1, 2020 1:11:42 PM
To: Andrew Butterfield
Cc: cl-isabelle-users at lists.cam.ac.uk
Subject: Re: [isabelle] Non-idempotence of datatype constructors

Hello,

we're talking about Isabelle datatypes here, which are always finite
(final algebras is the categorial interpretation). The Haskell
interpretation is actually a codatatype (the final coalgebra) and
calling them "datatypes" is, in my opinion, actually a bit non-standard.
But it makes sense given the lazy semantics of Haskell.

Manuel


On 01/05/2020 12:59, Andrew Butterfield wrote:
> Hi Manuel,
>
> it depends on how you interpret a datatype declaration
>
> In Haskell, the data type
>
> List = Null | Cons Int List
>
> is interpreted as defining an "arrow"  List ->  Null +  Cons (Int,List)
>
> This admits infinite structures and supports laziness in that language
>
> So the the following Haskell definition is fine
>
> one = Cons 1 one
>
> and is implemented with a loop from the one component to the Cons.
>
> Those more used to the ML flavour of FP will interpret the above datatype as
>
> Null -> List   and  (Int,List) -> List
>
> This allows only finite structures, and here it is not possible to
> define 'ones' as above.
>
>
>> On 1 May 2020, at 11:24, Manuel Eberl <eberlm at in.tum.de
>> <mailto:eberlm at in.tum.de>> wrote:
>>
>> This is one for our datatype experts:
>>
>> I just noticed that theorems like
>>
>> Cons x xs ≠ xs
>>
>> are not automatically provided by the datatype package although they
>> should clearly hold for any datatype. To be more precise, I am talking
>> about theorems of the form
>>
>> C x1 … xn ≠ x1
>> …
>> C x1 … xn ≠ xn
>>
>> for any n-ary datatype constructor C (and of course also the flipped
>> variant).
>>
>> I'm not sure how useful something like this is in practice and it's
>> fairly easy to prove these by hand when needed. I just ran into a
>> situation where I had an assumption of the form "C a b ≠ b" and was
>> surprised that the simplifier didn't take care of it automatically.
>>
>> I realise that the datatype package already provides an absurd number of
>> theorems and one should be careful to blow it up even more, but seeing
>> as the number of theorems to be generated is linear in the number of
>> constructors and they're probably very easy to prove, one could consider
>> it. Or perhaps at least as an optional plugin or standalone tool.
>>
>> Manuel
>>
>>
>>
>
> --------------------------------------------------------------------
> Andrew Butterfield     Tel: +353-1-896-2517     Fax: +353-1-677-2204
> Lero@TCD, Head of Software Foundations & Verification Research Group
> School of Computer Science and Statistics,
> Room G.39, O'Reilly Institute, Trinity College, University of Dublin
>                          http://www.scss.tcd.ie/Andrew.Butterfield/
> --------------------------------------------------------------------
>




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