[Agda] Absurd pattern; convincing Agda

[Daniel Peebles]

Do other systems have better solutions to this problem? I vaguely remember
coming across a huge flamewar on the epigram mailing list a while back
about something very similar to this. Has there been any progress in
avoiding unnecessary implicit case splits while still having a sound
backing?

Thanks,
Dan

On Tue, Jun 12, 2012 at 10:54 AM, Andreas Abel <andreas.abel at ifi.lmu.de>wrote:

> Hi Paul,
>
> this is how to convince Agda.  Just split one level deeper:
>
>  withoutEQ (def f (x ∷ [])) () | no ¬p
>  withoutEQ (def f (x ∷ x₁ ∷ xs)) () | no ¬p
>
> Now the unsolved meta is gone.
>
> The problem was that the equations given for a match do not always hold
> literally.  In you case, this equation does not reduce:
>
>  outerIsEq (def f (x ∷ xs)) | no ¬p = false
>
> This is because internally, Agda decided it wants to split on xs before
> reducing.  I'd consider this unwanted behavior on the side of Agda. See:
>
>  http://code.google.com/p/agda/**issues/detail?id=408<http://code.google.com/p/agda/issues/detail?id=408>
>
> In a simple case, consider the equations
>
>  and : Bool -> Bool -> Bool
>  and false x = false
>  and y false = false
>  and _ _     = true
>
> One of
>
>  and false x
>  and y false
>
> will not reduce to false, since Agda converts this definition into a case
> tree, so it will either match on the first (likely) or the second argument.
>  So you will likely get the equations
>
>  and false x    = false
>  and true false = false
>  and true true  = true
>
> and the type
>
>  and y false == false
>
> will not be empty.
>
> Why in your specific case you do not get the equations you specified, I
> cannot tell.
>
> Hope that helps.
>
> Cheers,
> Andreas
>
>
> On 12.06.2012 14:36, Paul van der Walt wrote:
>
>> Dear all,
>>
>> I asked this question on IRC, but it was rather quiet there, so
>> maybe someone here could help me out.
>>
>> I am using the Reflection API, and I'd like to manipulate a
>> value of type Term which is returned by quoteTerm. I have a
>> function which only works for Terms of the form (something ==
>> true), and this function should return the LHS if the Term has
>> this form. To make this function total, I also have a
>> predicate (validity of input checker) which only returns true
>> for the cases I want to take care of. See the functions here:
>> http://hpaste.org/69846 (excuse the formatting)
>>
>> The problem is, one of the absurd patterns is accepted by Agda,
>> but remains yellow. This causes problems when trying to use the
>> module elsewhere. I can clearly see that this case can never be
>> reached (order of patterns matters here), but Agda doesn't
>> believe me.
>>
>> Does anyone know how I can solve this? Maybe my approach is
>> really ugly?
>>
>> Thanks in advance, I hope my question is clear enough.
>>
>> Cheers,
>> Paul van der Walt
>>
>>
>>
>> ______________________________**_________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/**mailman/listinfo/agda<https://lists.chalmers.se/mailman/listinfo/agda>
>>
>
>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Theoretical Computer Science, University of Munich
> Oettingenstr. 67, D-80538 Munich, GERMANY
>
> andreas.abel at ifi.lmu.de
> http://www2.tcs.ifi.lmu.de/~**abel/ <http://www2.tcs.ifi.lmu.de/~abel/>
> ______________________________**_________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/**mailman/listinfo/agda<https://lists.chalmers.se/mailman/listinfo/agda>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20120612/50ce4c3e/attachment.html