CIS301 Friday, March 7      Write a proof of this sequent:

(p ^ q) -> r,  q  |-   p -> r

1. (p ^ q) -> r          premise
2.  q                    premise
+---------------------------------
|  3.  p        assumption
|  4.  p ^ q    ^i 3,2
|  5.  r        ->e 1,4
+--------------------------------
6.  p -> r               ->i 3-5

Tactic:  Goal was  p -> r ,  so we need a box with assumption  p
         and we try to prove  r  at the end of the box.
         Finish with  ->i  on the last line.
  
  
The above proof is a program!  To see why, let:
    p  ==  int
    q  ==  string
    r  ==  bool
     
Then, from the library components (global vars), 
    public bool doStuff(int x, string y)  // (int ^ string) -> bool,
and
    string data                           //  string
                                          //  |-
we built this program:  
    public bool myProc(int z)             //  int -> bool

The code/proof:
                                           // 1. presume  doStuff  is a global var
                                           // 2. presume  data  is a global var
    public bool myProc(int z) {            //    3. assume you have an int param,  z
        Tuple<int,string> args = (z, data) //    4. introduce a pair/tuple (^i)
        bool ans = doStuff(args)           //    5. call doStuff with the pair (->e)
        return ans                         //       and get the bool,  ans
    }                                      // 6. end function def (->i)
    
    
THE C# TYPE CHECKER IS A PROOF CHECKER FOR PROPOSITIONAL LOGIC.