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

[Andreas Abel]

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


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/