I. Calculational Style Proofs
 A. proof formats with equality
------------------------------------------
    CALCULATIONAL STYLE PROOFS

Why?




General Format

   A
 ==  {hint why A == B}
   B
 ==  {hint why B == C}
   C

This establishes that A == C
because it shows
     (A == B) /\ (B == C)
If C is true, then this proves A

------------------------------------------
  1. proof formats with implication
------------------------------------------
          STANDARD PROOF OUTLINES

To show: A ==> D

    A
==>  {hint why A ==> B}
    B
 ==  {hint why B == C}
    C
==>  {hint why C ==> D}
    D

Another way:

    D
<==  {hint why C ==> D}
    C
 ==  {hint why B == C}
    B
<==  {hint why A ==> B}
    A

------------------------------------------      
    What's the logical formula that these are equivalent to?
 B. rules and strategies
  1. rules
------------------------------------------
        SOME INFORMAL RULES

A. Don't use two reasons in one hint,
   use two steps instead

B. Substituting equals for equals always is okay.

C. Be careful with substitution 
   when you only know an implication
------------------------------------------
  2. strategies
------------------------------------------
        SOME STRATEGIES, HINTS

A. Start from the more complex side.

B. Use lemmas to isolate parts of a proof.

C. Avoid proof by contradiction if possible.

D. Look at the proof afterwards 
   to see if it can be simplified, or clarified
------------------------------------------
 C. practice
---------------------------------------------------------
                PRACTICE

For the following: give a proof or find a counterexample.

      P <==> P <==> P <==> !P

      P <== Q <==> P \/ !Q <==> P

      conjunction distributes over implication:
        P /\ (Q ==> R) <==> P /\ Q ==> P /\ R

      disjunction distributes over discrepancy:
        P \/ (Q ==> R) <==> P \/ Q ==> P \/ R
        
      disjunction distributes over discrepancy:
        P \/ (Q <=!=> R) <==> P \/ Q <=!=> P \/ R

      (P <==> P \/ Q) /\ (P \/ Q <==> P) <==> P <==> Q

       (P ==> Q) \/ (Q ==> P)
---------------------------------------------------------