Useful proof principles and strategies

• Heuristic. To prove P == Q, transform P == Q to a known theorem, transform P to Q, or transform Q to P.
  
  
• Heuristic. The operators that appear in an expression and the shape of its subexpressions focus the choice of theorems to be used in manipulating it. Therefore, in developing the next step of a proof, identify applicable theorems by matching theorems with the structure of the subexpressions of the current expression.
  
  
• Heuristic of Operator Elimination. To prove a theorem about an operator, first eliminate the operator using its definition, then manipulate, and finally reintroduce the operator (if necessary).
  
  
• Heuristic. To prove P == Q, transform the side with the most structure (either P or Q) into the other.
  
  
• Principle. Structure proofs to minimize the number of rabbits pulled out of a hat --make each step seem obvious, based on the structure of the expression and the goal of manipulation.
  
  
• Principle. Lemmas can provide structure, bring to light interesting facts, and ultimately shorten a proof.
  
  
• Heuristic. Exploit the ability to parse theorems like Golden rule, p /\ q == p == q == p \/ q, in many different ways (using associativity and symmetry transparently).