Discussion:
rewriting before defining
(too old to reply)
Thorsten Altenkirch
2018-02-28 18:07:23 UTC
Permalink
Hi,

I am mutually defining an equality and some other things. To be able to type check the other things I need the equality as a rewriting rule but agda doesn't let me.

That is I get the error
Rewrite rule from function Skm-∘ cannot be added before the function definition
when checking the pragma REWRITE Skm-∘
when checking the attached file.

I know that I am cheating but I want to do it. Can I tell it that I am a doctor and I know what I am doing. Otherwise I shouldn't be allowed to use Rewrite anyway.

Yes, I can replace it by a postulate but that misses the point.

Cheers,
Thorsten




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.
Andreas Abel
2018-03-01 09:30:42 UTC
Permalink
Well, the doctor could perform some surgery on Agda, take out the
cancerous error message and see what happens. ;-)

I wash my hands in innocence. For me, the intended use of REWRITE was
to add a proven propositional equality to definitional equality; if you
go beyond it, you have to worry about the semantics yourself.

Cheers,
Andreas
Post by Thorsten Altenkirch
Hi,
I am mutually defining an equality and some other things. To be able to
type check the other things I need the equality as a rewriting rule but
agda doesn't let me.
That is I get the error
Rewrite rule from function  Skm-∘  cannot be added before the function
definition
when checking the pragma REWRITE Skm-∘
when checking the attached file.
I know that I am cheating but I want to do it. Can I tell it that I am a
doctor and I know what I am doing. Otherwise I shouldn't be allowed to
use Rewrite anyway.
Yes, I can replace it by a postulate but that misses the point.
Cheers,
Thorsten
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
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

***@gu.se
http://www.cse.chalmers.se/~abela/
Thorsten Altenkirch
2018-03-01 10:02:33 UTC
Permalink
Post by Andreas Abel
Well, the doctor could perform some surgery on Agda, take out the
cancerous error message and see what happens. ;-)
I was hoping that a surgeon who is better versed with the Agda source would do this for me. :-) In particular I don’t really want to use a non-standard version of Agda.
Post by Andreas Abel
I wash my hands in innocence. For me, the intended use of REWRITE was
to add a proven propositional equality to definitional equality; if you
go beyond it, you have to worry about the semantics yourself.
You are right. Basically REWRITE is a limited form of equality reflection. I do prove this equality only I am proving it mutually with its use. This you can certainly do when you have full equality reflection. I shouldn’t need to introduce postulates here.

This particular instance enables me to define semisimplicial types without using a 2-level theory (the 2-level approach was described in our CSL 2016 paper http://www.cs.nott.ac.uk/~psztxa/publ/csl16.pdf). The rewrite version is both better from a pragmatic view (easier to use - I think) and from a semantic point (there are interpretations or type theory that model semisimplical types but not a (strong) 2-level theory where Nat is fibrant - at least that is what Mike Shulman told me).

In this setting we certainly do not want to have full equality reflection because it would destroy proof relevance and hence it is in this form incompatible with univalence. However, I claim that this instance of equality reflection is harmless (this is a conjecture).

We know that REWRITE can destroy soundness - so no difference here.

Thorsten
Post by Andreas Abel
Cheers,
Andreas
Post by Thorsten Altenkirch
Hi,
I am mutually defining an equality and some other things. To be able to
type check the other things I need the equality as a rewriting rule but
agda doesn't let me.
That is I get the error
Rewrite rule from function Skm-∘ cannot be added before the function
definition
when checking the pragma REWRITE Skm-∘
when checking the attached file.
I know that I am cheating but I want to do it. Can I tell it that I am a
doctor and I know what I am doing. Otherwise I shouldn't be allowed to
use Rewrite anyway.
Yes, I can replace it by a postulate but that misses the point.
Cheers,
Thorsten
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
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
http://www.cse.chalmers.se/~abela/
_______________________________________________
Agda mailing list
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.
Jesper Cockx
2018-03-05 14:04:10 UTC
Permalink
The problem is that if we allow a rewrite rule to be added before its
definition, then you could just prove it using refl (since it is now
reflexive, by virtue of adding the rewrite rule). So this doesn't actually
give you any more guarantees than just postulating the rewrite rule
outright. So I don't think it makes sense to allow this. If you can come up
with a way to use a rewrite rule for other definitions but not for defining
the rule itself, let us know (or even better: implement it and send us a
pull request ;) ).

-- Jesper

On Thu, Mar 1, 2018 at 11:02 AM, Thorsten Altenkirch <
On 01/03/2018, 09:30, "Agda on behalf of Andreas Abel" <
Post by Andreas Abel
Well, the doctor could perform some surgery on Agda, take out the
cancerous error message and see what happens. ;-)
I was hoping that a surgeon who is better versed with the Agda source
would do this for me. :-) In particular I don’t really want to use a
non-standard version of Agda.
Post by Andreas Abel
I wash my hands in innocence. For me, the intended use of REWRITE was
to add a proven propositional equality to definitional equality; if you
go beyond it, you have to worry about the semantics yourself.
You are right. Basically REWRITE is a limited form of equality reflection.
I do prove this equality only I am proving it mutually with its use. This
you can certainly do when you have full equality reflection. I shouldn’t
need to introduce postulates here.
This particular instance enables me to define semisimplicial types without
using a 2-level theory (the 2-level approach was described in our CSL 2016
paper http://www.cs.nott.ac.uk/~psztxa/publ/csl16.pdf). The rewrite
version is both better from a pragmatic view (easier to use - I think) and
from a semantic point (there are interpretations or type theory that model
semisimplical types but not a (strong) 2-level theory where Nat is fibrant
- at least that is what Mike Shulman told me).
In this setting we certainly do not want to have full equality reflection
because it would destroy proof relevance and hence it is in this form
incompatible with univalence. However, I claim that this instance of
equality reflection is harmless (this is a conjecture).
We know that REWRITE can destroy soundness - so no difference here.
Thorsten
Post by Andreas Abel
Cheers,
Andreas
Post by Thorsten Altenkirch
Hi,
I am mutually defining an equality and some other things. To be able to
type check the other things I need the equality as a rewriting rule but
agda doesn't let me.
That is I get the error
Rewrite rule from function Skm-∘ cannot be added before the function
definition
when checking the pragma REWRITE Skm-∘
when checking the attached file.
I know that I am cheating but I want to do it. Can I tell it that I am a
doctor and I know what I am doing. Otherwise I shouldn't be allowed to
use Rewrite anyway.
Yes, I can replace it by a postulate but that misses the point.
Cheers,
Thorsten
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
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
http://www.cse.chalmers.se/~abela/
_______________________________________________
Agda mailing list
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.
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
Thorsten Altenkirch
2018-03-05 16:32:29 UTC
Permalink
Hi Jesper,

Yes, Paolo Capritti already pointed this out to me (I was going to write an update). Basically I should not be able to use the rewriting rule on the right hand side of a recursive definition but this certainly goes beyond the abilities of Agda’s rewrite mechanism (or only for structurally smaller indices).

Cheers,
Thorsten

From: Agda <agda-***@lists.chalmers.se> on behalf of Jesper Cockx <***@sikanda.be>
Date: Monday, 5 March 2018 at 14:04
To: Thorsten Altenkirch <***@exmail.nottingham.ac.uk>
Cc: "***@gu.se" <***@gu.se>, Agda mailing list <***@lists.chalmers.se>, Nicolai Kraus <***@gmail.com>
Subject: Re: [Agda] rewriting before defining

The problem is that if we allow a rewrite rule to be added before its definition, then you could just prove it using refl (since it is now reflexive, by virtue of adding the rewrite rule). So this doesn't actually give you any more guarantees than just postulating the rewrite rule outright. So I don't think it makes sense to allow this. If you can come up with a way to use a rewrite rule for other definitions but not for defining the rule itself, let us know (or even better: implement it and send us a pull request ;) ).
-- Jesper
Post by Andreas Abel
Well, the doctor could perform some surgery on Agda, take out the
cancerous error message and see what happens. ;-)
I was hoping that a surgeon who is better versed with the Agda source would do this for me. :-) In particular I don’t really want to use a non-standard version of Agda.
Post by Andreas Abel
I wash my hands in innocence. For me, the intended use of REWRITE was
to add a proven propositional equality to definitional equality; if you
go beyond it, you have to worry about the semantics yourself.
You are right. Basically REWRITE is a limited form of equality reflection. I do prove this equality only I am proving it mutually with its use. This you can certainly do when you have full equality reflection. I shouldn’t need to introduce postulates here.

This particular instance enables me to define semisimplicial types without using a 2-level theory (the 2-level approach was described in our CSL 2016 paper http://www.cs.nott.ac.uk/~psztxa/publ/csl16.pdf). The rewrite version is both better from a pragmatic view (easier to use - I think) and from a semantic point (there are interpretations or type theory that model semisimplical types but not a (strong) 2-level theory where Nat is fibrant - at least that is what Mike Shulman told me).

In this setting we certainly do not want to have full equality reflection because it would destroy proof relevance and hence it is in this form incompatible with univalence. However, I claim that this instance of equality reflection is harmless (this is a conjecture).

We know that REWRITE can destroy soundness - so no difference here.

Thorsten
Post by Andreas Abel
Cheers,
Andreas
Post by Thorsten Altenkirch
Hi,
I am mutually defining an equality and some other things. To be able to
type check the other things I need the equality as a rewriting rule but
agda doesn't let me.
That is I get the error
Rewrite rule from function Skm-∘ cannot be added before the function definition
when checking the pragma REWRITE Skm-∘
when checking the attached file.
I know that I am cheating but I want to do it. Can I tell it that I am a
doctor and I know what I am doing. Otherwise I shouldn't be allowed to
use Rewrite anyway.
Yes, I can replace it by a postulate but that misses the point.
Cheers,
Thorsten
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
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
http://www.cse.chalmers.se/~abela/
_______________________________________________
Agda mailing list
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.




_______________________________________________
Agda mailing list
***@lists.chalmers.se<mailto:***@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.

Loading...