[Agda] Absurd pattern; convincing Agda

[Andreas Abel]

In Coq, if you just use CIC syntax and write the match-tree directly 
yourself, the reduction behavior is apparent.  However, it is too 
painful if you want dependent pattern matching...

I'd be happy if Agda would give me feedback about which of the equations 
actually hold definitionally.  E.g. by underlying them with a 
light-green background or warning me about those that do not hold 
definitionally.

Another take would be that I as user mark the equations that I want 
definitively to hold, and if Agda does not manage to construct a 
case-tree accordingly, it will give an error.

Cheers,
Andreas

On 12.06.12 5:00 PM, Daniel Peebles wrote:
> 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
> <mailto: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 <mailto: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 <mailto: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 <mailto: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/