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

[Andreas Abel]

On Jul 3, 2009, at 8:02 PM, Ulf Norell wrote:

> @Nisse:  Surely, Agda expressions could not be translated to core
> anymore, but their typing derivations could.  For instance, into a
> language with explicit proofs of definitional equality everywhere, as
> suggested by Freek Wiedijk.
>
> "With" is easily explainable as a local function, and Agda generates  
> and type checks this function when checking a with.

I know, but apparently it is not so intuitive for the user.

Anyway, more theoretical work is needed before a "smart case" could be  
integrated into Agda.

Also, case is not a substitute for with, since it does not refine  
function arguments as "with" does, so it can't replace "with" for  
inductive families.  However, a strengthening of with by rewriting  
would be desirable.
Such a "strong with" would be explained by a local recursive function  
which is used only once, applied to arguments.

Taking the example from your tutorial (p.13)

   equal? : (n m : Nat) -> Equal? n m
   ...
   equal? (suc n) (suc m) with equal? n m
   equal? (suc n) (suc .n) | eq refl = bla
   ...

This could be translated to

   equal? (suc n) (suc m) =
      (local aux : (n0 m0 : Nat) -> Equal? n0 m0 -> Equal (suc n0)  
(suc m0)
                 aux n0 .n0 (eq refl) = bla
                ...)  n m (equal? n m)

While checking bla we have the rewrites

   n --> n0
   m --> m0
   equal? n m --> eq refl

Cheers,
Andreas