[Agda] Help with understanding REWRITE

[Jesper Cockx]

Hi Andrew,

This seems to be an unfortunate interaction between --rewriting and an
optimization performed by Agda, the detection of "projection-like"
functions. Agda detects that the function `Cset` is projection-like, which
allows it to erase the first argument. Unfortunately this means the
argument is no longer available for the rewrite rule either.

If you want, you can turn off the optimization using the
`--no-projection-like` flag. I'm not sure if there's currently an option to
turn it off on a case-by-case basis.

-- Jesper

On Sun, Oct 4, 2020 at 3:07 PM Andrew M. Pitts <amp12 at cam.ac.uk> wrote:

> I’m struggling to understand an aspect of --rewriting in Agda (2.6.1) and
> wonder if someone can help?
>
> The following artificial example illustrates my problem (which is more
> complicated and less artificial).
>
> ---
> {-# OPTIONS --rewriting #-}
>
> open import Agda.Builtin.Equality
> open import Agda.Builtin.Equality.Rewrite
>
> data C (S : Set) : Set₁ where
>   mkC :
>     (A : Set)
>     (e : A ≡ S)
>     → ---------
>     C S
>
> Cset : (S : Set) → C S → Set
> Cset S (mkC A e) = A
>
> Cequ : (S : Set)(c : C S) → Cset S c ≡ S
> Cequ S (mkC A e) = e
>
> {-# REWRITE Cequ #-} — this is not accepted!
>
> ——
>
> Given S : Set, the datatype C S contains values given by a set A and a
> proof that A equals S. Can we make that proof definitional rather than
> propositional, using a REWRITE? Apparently not — if you check the above
> Agda code, Agda 2.6.1 complains
>
> -- Cequ is not a legal rewrite rule, since the following variables are
> -- not bound by the left hand side: S
> -- when checking the pragma REWRITE Cequ
>
> The “left-hand side” it refers to is Cset S c, which certainly contains an
> occurrence of S. Why is S not “bound by” this left-hand side? I declared
> the type of Cequ to be
>
> (S : Set)(c : C S) → Cset S c ≡ S
>
> bu Agda 2.6.1 reports it to be
>
> (S : Set) (c : C S) → Cset _ c ≡ S
>
> Note the underscore. Presumably this is why REWRITE Cequ is not accepted.
>
> Where did that underscore come from? And is there some way to avoid it and
> have the REWRITE accepted?
>
> Andy
>
>
>
>
>
>
> _______________________________________________
> 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/20201005/4403b0ba/attachment.html>