[Agda] The joys and sorrows of abstraction

[Philip Wadler]

Ulf,

Thank you for taking the time to produce your simple example. Indeed, that
makes it clear why stability under substitution may be too much to hope for.

Martin,

Thank you for sketching your preferred subset. I must admit that 'with' and
implicits are two of my favourite features. In place of `with`, do you
simply use auxiliary functions? I thought that `with` and auxiliary
functions were meant to be equivalent?

Cheers, -- P

.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

On 16 May 2018 at 16:35, Ulf Norell <ulf.norell at gmail.com> wrote:

> In your case the reason the proof fails without `abstract` is that the
> `rewrite` doesn't trigger.
> Here's a simpler example exhibiting the same behaviour:
>
> module _ where
>
> open import Agda.Builtin.Nat
> open import Agda.Builtin.Bool
> open import Agda.Builtin.Equality
>
> module WithAbstract where
>
>   abstract
>     f : Nat → Nat
>     f zero    = zero
>     f (suc n) = suc (f n)
>
>     lem : ∀ n → f n ≡ n
>     lem zero    = refl
>     lem (suc n) rewrite lem n = refl
>
>   thm : ∀ m n → f (suc m) + n ≡ suc (m + n)
>   thm m n rewrite lem (suc m) = refl
>   -- Works.
>
> module WithoutAbstract where
>
>   f : Nat → Nat
>   f zero    = zero
>   f (suc n) = suc (f n)
>
>   lem : ∀ n → f n ≡ n
>   lem zero    = refl
>   lem (suc n) rewrite lem n = refl
>
>   thm : ∀ m n → f (suc m) + n ≡ suc (m + n)
>   thm m n rewrite lem (suc m) = refl
>   -- Fails since rewrite doesn't trigger:
>   --   lem (suc m)  : suc (f m)     ≡ suc m
>   --   goal         : suc (f m + n) ≡ suc (m + n)
>
> In general I think it's optimistic to expect tactics (of which rewrite is
> an example) to be stable under substitution.
>
> / Ulf
>
>
> On Wed, May 16, 2018 at 9:24 PM, Philip Wadler <wadler at inf.ed.ac.uk>
> wrote:
>
>> Thanks, Martin. So which fragment do you recommend? Cheers, -- P
>>
>> .   \ Philip Wadler, Professor of Theoretical Computer Science,
>> .   /\ School of Informatics, University of Edinburgh
>> .  /  \ and Senior Research Fellow, IOHK
>> . http://homepages.inf.ed.ac.uk/wadler/
>>
>> On 16 May 2018 at 16:03, Martin Escardo <m.escardo at cs.bham.ac.uk> wrote:
>>
>>>
>>>
>>> On 16/05/18 20:37, Philip Wadler wrote:
>>>
>>>> Thanks for following up. It is the latter case. But I don't understand
>>>> why it should be ok for that to fail. Removing abstract should just replace
>>>> some abstract terms by their concretions, which have already been type
>>>> checked. Everything that was provably equal before should still be equal,
>>>> so why is it ok for the proof of equality to now fail? Doesn't this violate
>>>> stability under substitution? Cheers, -- P
>>>>
>>>
>>> It is because of things such as this that I prefer to restrict my usage
>>> of Agda to a fragment corresponding to a well-understood type theory.
>>>
>>> This may be limiting in terms of expressivity, conciseness, and
>>> efficiency, but at least one can tell whether something is a bug or not,
>>> rather than a bug or a feature.
>>>
>>> :-)
>>> Martin
>>>
>>>
>>
>> The University of Edinburgh is a charitable body, registered in
>> Scotland, with registration number SC005336.
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180516/358de6a7/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180516/358de6a7/attachment.ksh>