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

[Andreas Abel]

Let me add my 5 cent to this discussion.

It seems that the "naive" user (for instance, me) expects that Agda  
"knows" that "bla = true" in "anotherthing" when writing

something with bla
...  | true = anotherthing

The "magic with" meets this expectation partially by rewriting the  
current goal.  However, the equation "bla = true" may be needed not  
only in the goal, but otherwhere as well.  The inspect pattern  
provides this equation as a proof which can be manipulated explicitly,  
yet inspect is complicated to use, in the general case you have to  
apply Josh Ko's pattern.  It is desirable that Agda considers "bla"  
and "true" as definitionally equal.

I have played with idea by adding rewriting to MiniAgda

   http://www.tcs.ifi.lmu.de/~abel/miniagda/

While type checking "anotherthing", the rewrite rule "bla --> true"  
may fire.

For example, this enables a simple proof of  f = f . f . f  for  
boolean functions f in MiniAgda.

data Bool : Set
{ true  : Bool
; false : Bool
}

data Id (A : Set)(a : A) : A -> Set
{ refl : Id A a a
}

-- Lemma: f x = f (f (f x))  for all f : Bool -> Bool
-- Proof by cases on x, f true, and f false
fun tripleF : (f : Bool -> Bool) -> (x : Bool) -> Id Bool (f x) (f (f  
(f x)))
{ tripleF f true = case f true
   { true -> refl Bool true
   ; false -> case f false
     { true  -> refl Bool false
     ; false -> refl Bool false
     }
   }
; tripleF f false = case f false
   { true -> case f true
     { true -> refl Bool true
     ; false -> refl Bool true
     }
   ; false -> refl Bool false
   }
}

The same proof cannot be done with "magic with", since, the equations  
like "f true = true" have to be used more than once in the goal.  [A  
proof with inspect would certainly be possible.]

Case is limited to inductive /types/ at the moment, for inductive  
families one would need a combination of "with" and rewriting.

Another example: Insertion into sorted lists.  Here I need to compare  
n and m with leq n m and in case true, I need to embed a proof of leq  
n m == true into my sorted list structure by passing it as an argument  
to scons. Since this equation holds definitionally, the proof is  
"triv"ial.  Here is an excerpt, I include the full code.

data SList : Nat -> Set
{ snil  : SList zero
; scons : (m : Nat) -> (n : Nat) -> True (leq n m)  -> SList n ->  
SList m
}

fun insert : (m : Nat) -> (n : Nat) -> SList n -> SList (max n m)
{ insert m .zero snil = scons m zero triv snil
; insert m .n (scons n k p l) = case leq n m
   { true  -> scons m n triv (scons n k p l)
   ; false -> scons n (max k m) (maxLemma k m n p (leFalse n m triv'))
                    (insert m k l)
   }
}

Adding rewriting could make Agda's with more "magic" (and more  
intuitive).  Certainly, this must have been discussed, and there are  
reasons why it has not been implemented.

Conor? Ulf?

Are there theoretical obstacles (non-termination?) or is it too  
complicated/inefficient?

Cheers,
Andreas


-------------- next part --------------
A non-text attachment was scrubbed...
Name: caseSList.ma
Type: application/octet-stream
Size: 1404 bytes
Desc: not available
Url : https://lists.chalmers.se/mailman/private/agda/attachments/20090703/e527ed5d/caseSList.obj
-------------- next part --------------



On Jun 25, 2009, at 6:40 PM, Ana Bove wrote:

> Hi,
>
> I must say I am confuse as well....
>
> let us simply consider the case were we want to insert x in (y ::  
> ys) and comp x y = Lt
>
> Then the insert function simply returns x :: y :: ys and in that eq.  
> of the sorted-insert we need to simply give a proof that Sorted  
> (x :: y :: ys).
>
> Now, if in this equation I write
>
> ......
> sorted-insert x (y ? ys) prf with Order.comp o x y
> sorted-insert x (y ? ys) prf | Lt =
> let q : Sorted (x ? y ? ys)
> q = ?
> in q
> ......
>
> then I can type check.
>
> However, if I try to do the same in the sorted-insert2 it does not!
>
> ......
> sorted-insert2 x (y ? ys) prf with inspect (Order.comp o x y)
> sorted-insert2 x (y ? ys) prf | Lt with-? p =
> let q : Sorted (x ? y ? ys)
> q = ?
> in q
> ......
>
> I get the error
>
> x ? y ? ys != insert x (y ? ys) | Order.comp o x y of type List  
> A
> when checking that the expression q has type
> Sorted (insert x (y ? ys) | Order.comp o x y)
>
> q should be the term
> sorted-cons2 x y ys prf (biimply-fwd (Order.isLtComp o x y) (symm p))
> (well, the whole let of course should not be used)
>
> And I must say I do not understand why. I never used inspect before  
> but I thought the difference with inspect was that not only gave me  
> the result I would get without inspect but also the "evidence" of  
> that result.
> But otherwise it should not matter.