The `ring` expression types

Stream: mathlib4

[Bolton Bailey]

I have a quick question about this line description in the ring tactic documentation. Is it the case that the mutually inductive datatype itself is enforcing the normalization? Or is it technically possible to write something that will produce unnormalized ExSum/ExProd and it's just the case that the eval_... functions below never do this?

[Bolton Bailey]

@Mario Carneiro @Anne Baanen

[Bolton Bailey]

It seems to me like I could just apply the add constructor in various orders and get different ExSums for things that ring should prove equal, so I am confused.

[Mario Carneiro]

While it is possible to lie with the QQ types, if you follow the types as specified ExProd et al will enforce most (but not all) of the normalization rules. For example ExSum ensures that it is a right-associated sum with 0 at the end and no internal + in each term (except in ExBase). An example of a normalization invariant not ensured by the types is that ExProd.const should not be zero.