Normalization/simplification function

[mortberg]

I want a function similar to what we call "normal" in cubicaltt. The purpose of this function is to normalize/simplify terms as far as possible, this means that it has to go under binders, unfold all definitions and compute all coe/hcom's as far as possible.

This is very useful for seeing how complicated definitions really are. I've found many things in cubicaltt that look innocent on the surface but once you start unfolding things you see that they are really complicated because they contain coe/hcom's in complicated types that unfold to a lot more hcom/coe's.

Another very useful thing with this kind of function is that they can be used to debug the system. If I have a term t : T in cubicaltt I can normalize/simplify it to get t', I can then ask the typechecker if t' : T. If this fails then I know that there is a bug somewhere and we managed to find a lot of bugs this way by doing this for the term inhabiting the type of the univalence axiom. In RedPRL we can probably not do exactly the same, but it might be that the heuristics are powerful enough to see that "t' : T" in many cases?

Note that it might be necessary for such a normalization/simplification function to be type-directed in RedPRL in order for things like (@ p 0) to reduce.

[cangiuli]

I think it would be nice to expose some sort of Eval Foo. (for non-stable closed-term evaluation) and Reduce Foo. (for stable reduction under binders) at the top level. Currently you can use the reduce tactic to play around with this inside a proof.

Some of what you are saying is not possible:

1. auto cannot always prove t : T, so it certainly cannot always prove t' : T for the value t' of t.
2. Types are not unique so you can't really have a type-directed simplification procedure. I think what you have in mind is reduce plus some fragment of auto. For example, given (@ p 0), p might be a variable of line type, in which case we know nothing about (@ p 0); a variable of type (path [_] a m n), in which case it is equal to m in a but might not be equal to m in some other type; or it could even be a variable of function type but we are inside the body of a function (-> void a) so the code is "dead."

[jonsterling]

We will hopefully be able to address this once we have a worked out theory of computational equivalence.