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

[Thorsten Altenkirch]

> A noteworthy thought is that you can detect some inconsistent
> constraints with your algorithm (the one I have also be aiming at),  
> but
> not all.  Consider the booleans with identity and negation defined by
> case distinction.  Then, the constraints
>
> id  x = true
> not x = true

I don't understand this, since "id x" is not normal, but if we reduce  
it it becomes x=true and hence not x reduces to false and this is  
inconsistent.

T.

>
>
> are inconsistent, but it goes unnoticed.  (A case distinction on x  
> would
> of course make it apparent.)  This is why I think that completeness of
> type checking is hard to achieve even in the presence of first order
> constraints.  However, of the three properties
>
> - - soundness
> - - completeness
> - - termination
>
> of type checking, completeness is the first to sacrifice.  A lack of
> completeness might involve some degree of frustration to the user, but
> it has to be weighted against the current frustration with "with".   
> The
> added convenience would imho compensate for incompleteness.
>
> @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.
>
> Cheers,
> Andreas
>
> Thorsten Altenkirch wrote:
>>>
>>> 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?
>
>
> - --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Theoretical Computer Science, University of Munich
> http://www.tcs.informatik.uni-muenchen.de/~abel/
> -----BEGIN PGP SIGNATURE-----
> Version: GnuPG v1.4.9 (GNU/Linux)
> Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org
>
> iEYEARECAAYFAkpOMKEACgkQPMHaDxpUpLNPfACfb+81kPM0wR04vjLPsnn9GIbL
> I+4An3EJms0F86rGOEpqONDj7iVU0+0t
> =oneB
> -----END PGP SIGNATURE-----


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.