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

[Thorsten Altenkirch]

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

Precisely!!!

We tried to do this in the original PiSigma paper: http://www.cs.nott.ac.uk/~txa/publ/pisigma.pdf
but decided that dealing with constraint in general seems to be too  
heavy for a core language. However, I think it would be a desirable  
feature for a high level langauge like Agda. Nisse asks the right  
question - and I think such a translation is possible but not trivial.

Basically we allowed to assume certain equalities (constraints) in the  
context. It is not completely trivial to make sure that transitivity  
of equality still holds. In our implementation we always tried to  
maintain that all the constraint are normal wrt to each other.

If I remember correctly one issue was closure under xi, because this  
leads to undecidability due to having to deal with universally  
quantified constraints.

Cheers,
Thorsten




On 3 Jul 2009, at 10:13, Andreas Abel wrote:

> 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
>
>
> <caseSList.ma>
>
>
> 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.
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.