[Agda] Rewrite rules for both Set and Prop

[Jesper Cockx]

Hi Filippo,

Matching rewrite rules is done up to definitional equality, so in your
example both foo and bar should typecheck. Since bar doesn't, it seems
you've found a bug in the implementation, congratulations! It's now fixed
in the development version of Agda, see
https://github.com/agda/agda/issues/4410. Thanks for the example.

-- Jesper

On Thu, Jan 30, 2020 at 2:33 PM Filippo Sestini <
Filippo.Sestini at nottingham.ac.uk> wrote:

> Hi Jesper,
>
> The problem as I see it is that even though all elements of a Prop are
> definitionally equal, there might be some other rewrite rules defined
> elsewhere that involve elements of a Prop as arguments, in a way that they
> are only triggered when such propositional arguments are of a certain
> shape. The "canonical" example would be when defining computation rules
> that only compute on canonical forms.
>
> Let me give a quick example. Suppose we have the following
>
> postulate
>   P : Prop
>   p : P
>   f : P -> P
>
>   g : {A : Set} -> P -> A -> A
>   eq : ∀{A} {x : A} -> g p x ≡ x
>
> {-# REWRITE eq #-}
>
> module _ {A : Set} {x : A} {y : P} where
>
>   foo : g p x ≡ x
>   foo = refl
>
>   bar : g (f y) x ≡ x
>   bar = refl
>
> Here, "foo" typechecks just fine, because the arguments of "g" in "g p x"
> match the rewrite rule "eq". However, "bar" doesn't because although "f y"
> is indeed definitionally equal to "p", it is still syntactically different
> from "p" so the previous rewrite rule doesn't get triggered. Of course Agda
> has no way to figure out that "p" is what is needed here, but I though that
> if we had a way to add the following rule
>
> postulate
>   f-eq : {x : P} -> f x ≡ p
>
> then the "bar" example above would work. Any thoughts?
>
> Cheers
> --
> Filippo
>
> On 1/30/20, 12:08 PM, "Jesper Cockx" <Jesper at sikanda.be> wrote:
>
>     Hi Filippo,
>
>
>     You're correct that you currently cannot do this, as there's no way to
> define types that are polymorphic over both Set and Prop (
> https://github.com/agda/agda/issues/3328), and you can only have one
>      rewriting relation. However, I don't understand why you would want
> rewrite rules to rewrite elements of a Prop, since they are anyway all
> equal?
>
>
>     -- Jesper
>
>
>
>     On Thu, Jan 30, 2020 at 12:31 PM Filippo Sestini <
> Filippo.Sestini at nottingham.ac.uk> wrote:
>
>
>     Hi all,
>
>     I'm trying to encode an equality type in Agda using rewrite rules.
>     I want the type to be a strict proposition, so I value it in the Prop
> universe.
>     However, this also means that among the equations that I want to
> encode as rewrite rules, some will end up being between elements of a Set
> (for example, when rewriting the eq type itself) and some will be between
> elements of a Prop (for example, the elements
>      of the identity type itself).
>
>     I'm struggling to find a way to do this with Agda's rewriting system.
> As far as I know there is no way to define an identity type that works for
> both types in Set and in Prop. One could define two different identity
> types for each, but unfortunately Agda doesn't
>      seem to allow declaring two different relations for BUILTIN REWRITE.
>
>     Am I missing something here? Does anybody know a way out of this?
>
>     Thank you
>     --
>     Filippo Sestini
>
>
>
>
>
>     This message and any attachment are intended solely for the addressee
>     and may contain confidential information. If you have received this
>     message in error, please contact the sender and delete the email and
>     attachment.
>
>     Any views or opinions expressed by the author of this email do not
>     necessarily reflect the views of the University of Nottingham. Email
>     communications with the University of Nottingham may be monitored
>     where permitted by law.
>
>
>
>
>     _______________________________________________
>     Agda mailing list
>     Agda at lists.chalmers.se
>     https://lists.chalmers.se/mailman/listinfo/agda
>
>
>
>
>
>
>
>
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please contact the sender and delete the email and
> attachment.
>
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email
> communications with the University of Nottingham may be monitored
> where permitted by law.
>
>
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200130/1c67fcbe/attachment.html>