<div dir="ltr"><div>Hi Filippo,</div><div></div><div><div><br></div><div>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 <a href="https://github.com/agda/agda/issues/4410">https://github.com/agda/agda/issues/4410</a>. Thanks for the example.<br></div><div><br></div><div>-- Jesper<br></div></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Jan 30, 2020 at 2:33 PM Filippo Sestini <<a href="mailto:Filippo.Sestini@nottingham.ac.uk">Filippo.Sestini@nottingham.ac.uk</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Hi Jesper,<br>
<br>
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.<br>
<br>
Let me give a quick example. Suppose we have the following<br>
<br>
postulate<br>
  P : Prop<br>
  p : P<br>
  f : P -> P<br>
<br>
  g : {A : Set} -> P -> A -> A<br>
  eq : ∀{A} {x : A} -> g p x ≡ x<br>
<br>
{-# REWRITE eq #-}<br>
<br>
module _ {A : Set} {x : A} {y : P} where<br>
<br>
  foo : g p x ≡ x<br>
  foo = refl<br>
<br>
  bar : g (f y) x ≡ x<br>
  bar = refl<br>
<br>
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<br>
<br>
postulate<br>
  f-eq : {x : P} -> f x ≡ p<br>
<br>
then the "bar" example above would work. Any thoughts?<br>
<br>
Cheers<br>
-- <br>
Filippo <br>
<br>
On 1/30/20, 12:08 PM, "Jesper Cockx" <<a href="mailto:Jesper@sikanda.be" target="_blank">Jesper@sikanda.be</a>> wrote:<br>
<br>
    Hi Filippo,<br>
<br>
<br>
    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 (<a href="https://github.com/agda/agda/issues/3328" rel="noreferrer" target="_blank">https://github.com/agda/agda/issues/3328</a>), and you can only have one<br>
     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?<br>
<br>
<br>
    -- Jesper<br>
<br>
<br>
<br>
    On Thu, Jan 30, 2020 at 12:31 PM Filippo Sestini <<a href="mailto:Filippo.Sestini@nottingham.ac.uk" target="_blank">Filippo.Sestini@nottingham.ac.uk</a>> wrote:<br>
<br>
<br>
    Hi all,<br>
<br>
    I'm trying to encode an equality type in Agda using rewrite rules.<br>
    I want the type to be a strict proposition, so I value it in the Prop universe.<br>
    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<br>
     of the identity type itself).<br>
<br>
    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<br>
     seem to allow declaring two different relations for BUILTIN REWRITE.<br>
<br>
    Am I missing something here? Does anybody know a way out of this?<br>
<br>
    Thank you<br>
    -- <br>
    Filippo Sestini<br>
<br>
<br>
<br>
<br>
<br>
    This message and any attachment are intended solely for the addressee<br>
    and may contain confidential information. If you have received this<br>
    message in error, please contact the sender and delete the email and<br>
    attachment. <br>
<br>
    Any views or opinions expressed by the author of this email do not<br>
    necessarily reflect the views of the University of Nottingham. Email<br>
    communications with the University of Nottingham may be monitored <br>
    where permitted by law.<br>
<br>
<br>
<br>
<br>
    _______________________________________________<br>
    Agda mailing list<br>
    <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
    <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br>
<br>
<br>
<br>
<br>
<br>
<br>
<br>
This message and any attachment are intended solely for the addressee<br>
and may contain confidential information. If you have received this<br>
message in error, please contact the sender and delete the email and<br>
attachment. <br>
<br>
Any views or opinions expressed by the author of this email do not<br>
necessarily reflect the views of the University of Nottingham. Email<br>
communications with the University of Nottingham may be monitored <br>
where permitted by law.<br>
<br>
<br>
<br>
<br>
</blockquote></div>