Smart Case [Re: [Agda] A puzzle with "with"]

[Thorsten Altenkirch]

>>> Consider the booleans with identity and negation defined by case
>>> distinction. Then, the constraints
>>>
>>> id  x = true
>>> not x = true
>> I don't understand this, since "id x" is not normal, but if we  
>> reduce it it becomes x=true and hence not x reduces to false and  
>> this is inconsistent.
>
> I think you should read Andreas' statement as "(identity and negation)
> defined by case distinction", not "identity and (negation defined by
> case distinction)".

Yes, we discussed this already offline. Here is the relevant part of  
our exchange:

>> I meant identity also defined by cases,
>>
>> id true = true
>> id false = false
>>
>> Then, id x is neutral.
>
> Yes, but then the inconsistency is not derivable unless you assume  
> strong equality for coproducts.
>
> So what is the problem?
>>
>> Or take something more complicated like
>>
>> prime n = true
>> composite n = true
>>
>> Agda cannot know that a number cannot be both prime and composite.
>>
>> In the complicated case, it is sufficiently clear to the user that  
>> Agda can't do magic.  In the simple case above it might not be so  
>> clear, but that is just tough luck.
>
> I think the spec is quite clear (see our paper). We use the usual  
> rules of lambda calculus to derive consequences from the equational  
> assumptions. But already this is quite difficult.
>
>> Did you do any models for type theory with constraints which can be  
>> used to prove termination?
>
> We were looking at algorithms to handle constraints using big step  
> normalisation. Basically, when you get stuck on a neutral term you  
> check whether it matches any of your constraints (which are always  
> of the form neutral -> constructor) using equality. To prove  
> normalisation will be tricky but we were most interested in  
> completeness which is already quite difficult.
>

This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.