Posting a question/answer with the TA regarding order of operations in Coq.
QUESTION:
Hi Jeehoon,
Do you have time to answer a quick question for me? I've reduced a proof in assignment 2 to this: p + (n' * p + m * p) = p + n' * p + m * p. I'm trying to figure out how mult and plus will be executed, but I'm confused about the order of operations and want to check with you that my understanding is correct. You mentioned yesterday that by default Coq evaluates expressions from left to right, so here is my guess about how the terms are evaluated:
Starting on the left-hand side of the equation, Coq first evaluates the terms inside the parentheses by multiplying n' and p and m and p and adding the results. The p outside the parentheses is then added to the unified term inside the parentheses. On the left-hand side, the multiplication is evaluated first, then, moving from left to right p is added to the result of n' * p and the result of that is added to m * p.
I hope that by understanding the order of operations I can get rid of the parentheses! It's so frustrating to have them keeping the proof from going through.
Thank you,
Adam
ANSWER:
Your interpretation seems right. p + (n' * p + m * p) means p + ((n' * p) + (m * p)), and p + n' * p + m * p means (p + (n' * p)) + (m * p).
Sorry for confusion I made; (1) * is more privileged than +, and (2) left +/* is more privileged than right +/*. (1) was missing in my explanation yesterday.
It would be helpful to use the issue tracker for this kind of general questions :-) Would you please make an issue for the interpretation of operators? Thanks.
Posting a question/answer with the TA regarding order of operations in Coq.
QUESTION: Hi Jeehoon,
Do you have time to answer a quick question for me? I've reduced a proof in assignment 2 to this: p + (n' * p + m * p) = p + n' * p + m * p. I'm trying to figure out how mult and plus will be executed, but I'm confused about the order of operations and want to check with you that my understanding is correct. You mentioned yesterday that by default Coq evaluates expressions from left to right, so here is my guess about how the terms are evaluated:
Starting on the left-hand side of the equation, Coq first evaluates the terms inside the parentheses by multiplying n' and p and m and p and adding the results. The p outside the parentheses is then added to the unified term inside the parentheses. On the left-hand side, the multiplication is evaluated first, then, moving from left to right p is added to the result of n' * p and the result of that is added to m * p.
I hope that by understanding the order of operations I can get rid of the parentheses! It's so frustrating to have them keeping the proof from going through.
Thank you,
Adam
ANSWER:
Your interpretation seems right. p + (n' * p + m * p) means p + ((n' * p) + (m * p)), and p + n' * p + m * p means (p + (n' * p)) + (m * p).
Sorry for confusion I made; (1) * is more privileged than +, and (2) left +/* is more privileged than right +/*. (1) was missing in my explanation yesterday.
Jeehoon