[Agda] Absurd pattern; convincing Agda

[Andreas Abel]

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

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


-- 
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/