[Agda] Rewriting in general

[Owen]

I'm pretty new to Agda, so I apologize for this newbie question.

I think it's pretty cool how Agda can rewrite parts of the AST (I suppose
these are "terms"? But I think of it as the AST) using the basic rules of
evaluation and normalization. That is, pattern matching on _≡_ introduces
new definitional equalities that cause the LHS to reduce to the RHS,
without introducing any new machinery. That's very neat.

I am, however, wondering if it is necessary. Supposing I had a "macro" (I
put "macro" in quotes because I do not mean a standard Agda macro. If I
understand correctly, standard Agda macros operate on normalized (open)
terms, whereas I mean a procedure that operates on potentially unnormalized
(open) terms) that substituted part of the current AST with another part,
using a substitution that happened to be available as an equality of some
sort.

What I have in my head is a graphical utility that would show you the
current AST as a tree. First, you could direct the utility to perform some
reductions (as desired), but not necessarily a full normalization. Then,
you could then click on a subtree, and say "replace this with an equivalent
expression", and it would do that (assuming you had access to a proof of
that equivalence). My motivation for thinking about this kind of utility
are the various hoops that are sometimes required (eg inspect) to convince
Agda to rewrite just the part of the AST that is desired. Also, Aaron
Stump's latest post makes it seem like directing rewrites towards
particular terms is sometimes a little tricky.

I am wondering if there are any obvious contradictions or weird behaviors
that would turn up as a result of a more general rewrite facility that
wasn't based on reductions. In other words, is there something about
handling propositional equalities via reduction that avoids potential
pitfalls? Or, put another way, is the principle that "equals may be
substituted for equals" generally true in Agda, or does Agda take special
care through normalization to make sure that that stays true?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160127/edabc832/attachment.html