Possibly support more flexible parens on chains of symmetric, associative operators

[NicMcPhee]

Currently we require full parenthesization of expressions like p ∧ q ∧ r; as is this will generate an "Error in input" message, so we have to do something like (p ∧ q) ∧ r instead. Technically this isn't necessary because ∧ is associative and symmetric all orderings and parenthesizations are equivalent.

In a recent demo/feedback sessions there were varying opinions on what, if anything, we should do about this.

Several people (especially students) eventually came to the conclusion that we should continue to require full parenthesization as it forces students to be clear about their intentions and the relationships between operators. Personally, I'm actually quite sympathetic to this position.

@elenam felt that we should instead allow students to enter expressions like p ∧ q ∧ r and the system should then rewrite their expression to include the parentheses as they are being interpreted by the system, e.g., (p ∧ q) ∧ r or p ∧ (q ∧ r) depending on whether we're assuming ∧ is left or right associative. I have some qualms about this, the largest being that it seems like a bit of a UI nightmare. Having the system change what they entered without them necessarily being aware of it or understanding exactly what is happening seems like a mess waiting to happen. Alternatively you could display both their version and the interpreted version in the proof, but that seems cluttered. Or you could have a dialog pop up that says "You typed this – are you OK if we interpret it as that?" or some such, but that potentially adds a lot of distracting dialogs.

Unsure, TBH.

Another option would be to have several options/levels that are user selectable. That's probably a different issue or even an epic, though.