rewrite and issue 1692 [Re: [Agda] aggressive with, VFPiA]

[Aaron Stump]

Dear Andreas,

Thanks for your fast, gracious, and also funny reply.  Sorry I did not 
manage to check on this earlier when you called for comments on the new 
"with".  I should have done that.  I really appreciate that you agree to 
do something to change the funny new behavior of rewrite.  I'll watch 
for an update about this once the decision has been reached on the exact 
fix.

Cheers,
Aaron



On 01/27/2016 02:16 PM, Andreas Abel wrote:
> Dear Aaron,
>
> thanks for your message and alerting us of more breakage.  The change 
> of `with` was triggered by
>
>   https://github.com/agda/agda/issues/1692
>
> where `rewrite` failed to meet the expectations.  The new with/rewrite 
> fails to meet yours and is apparently not backwards compatible. 
> However, this unfortunately only surfaced after the merge.  It would 
> have been helpful if you had responded to my earlier message
>
>   https://lists.chalmers.se/pipermail/agda/2015/008202.html
>
> where I asked for feedback on the new with.  Moreover, the plans to 
> change with/rewrite "have been on display at your local planning 
> department in Alpha Centauri for fifty of your Earth years so you’ve 
> had plenty of time to lodge any formal complaints and its far too late 
> to start making a fuss about it now." :) [D. Adams]
>
> More seriously, you complaint is a reasonable one and something has to 
> be done about this.  It seems to be easiest to change the rewrite 
> tactic such that
>
>   lemma f a p rewrite p = p
>
> behaves like
>
>   data Protect {a} {A : Set a} : A → Set where
>     protect : ∀ x → Protect x
>
>   lemma : ∀ {A : Set} (f : A → A) (a : A) (p : f a ≡ a) → f (f a) ≡ a
>   lemma f a p with protect p | f a | p
>   ... | _ | _ | refl = p
>
> which works around the more aggressive with with the just invented 
> Protect Pattern (TM) (C) Andreas Abel, Gothenburg University, 2016.
>
> This change would unfix issue 1692 but hopefully fix both your book 
> and Wolfram Kahl's code.
>
> Comments, anyone?
>
> Cheers,
> Andreas
>
> On 27.01.2016 19:52, Aaron Stump wrote:
>> Dear Agda developers,
>>
>> Starting in Agda version 2.4.2.5, the abstraction performed by "with"
>> has (as the CHANGELOG tells us) become more aggressive.  I am sure you
>> have good reasons for this change, but are you aware that you have made
>> it impossible to rewrite with the same assumption twice? Consider this
>> self-contained example:
>>
>> module test where
>>
>> data _≡_ {ℓ} {A : Set ℓ} (x : A) : A → Set ℓ where
>>    refl : x ≡ x
>>
>> {-# BUILTIN EQUALITY _≡_ #-}
>> {-# BUILTIN REFL refl #-}
>>
>> lemma : ∀ {A : Set}(f : A → A)(a : A) → f a ≡ a → f (f a) ≡ a
>> lemma f a p rewrite p = p
>>
>> With previous versions of Agda, this would be fine.  But starting with
>> 2.4.2.5, this does not type check.  If we put a hole on the right-hand
>> side of the sole equation for lemma, we will see this goal:
>>
>> Goal: f a ≡ a
>> ————————————————————————————————————————————————————————————
>> p  : a ≡ a
>>
>> The "rewrite p" directive has actually been applied to rewrite the type
>> of p itself, rendering it trivial and hence useless.  This is a real
>> problem.  I have maybe 25 places in the Iowa Agda Library that have been
>> broken by this.  I don't mind fixing them, but I think this is a major
>> flaw in the new way "with" works.  One should be able to reuse
>> assumptions.  For the particular example above, I actually am struggling
>> to find any workaround.  How would you prove this?  Maybe inspect on
>> steroids is supposed to be used?  For what I have done, usually inspect
>> has been enough.  But being able to apply an assumption twice with
>> rewrite seems pretty fundamental.  This is not linear logic!
>>
>> There is a second issue I want to raise.  As you know (since Jesper and
>> Ulf wrote me very helpful and quite detailed reviews), I am bringing
>> out, with ACM Books, a textbook called "Verified Functional Programming
>> in Agda" (VFPiA) this year.  The book is in the very last stages of
>> proofs.  In the book, I refer readers to Agda 2.4.2.2 and IAL release 
>> 1.2:
>>
>> svn co --username=guest --password=guest
>> https://svn.divms.uiowa.edu/repos/clc/projects/agda/ial-releases/1.2
>>
>> So, certainly the book is usable.  But this release does not check with
>> Agda 2.4.2.5.  Furthermore, some of what I say in the book is
>> invalidated by the fact that we cannot rewrite twice with the same
>> assumption.
>>
>> Of course, whether the book is successful or not is not your
>> responsibility, though by reviewing it for me, Ulf and Jesper have made
>> some investment in its success.  But if you want to take advantage of my
>> efforts here to help spread Agda to new users, it would be really a good
>> idea if releases of Agda were compatible with IAL version 1.2. I do not
>> do anything very exotic.  If there are changes to compiler pragmas, that
>> is fine.  And of course, I hardly expect you to limit yourself to back
>> compatibility with my library. But if you could at least consider
>> whether changes you make are breaking this library (and hence, to some
>> extent, breaking VFPiA), I would appreciate it, and I hope it would help
>> the broader Agda community.
>>
>> Best wishes,
>> Aaron
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>
>