CIS301 Monday, March 10 NAME___sample solution________
Write a proof of this sequent. Consciously apply (some of) the tactics for ^i, ve, and >i, and you will find the proof easily.
p > r, q > s  (p v q) > (r v s)
Tactic 1: Since > is the main connective in the goal, apply the >i tactic: assume (p v q) in a box and try to prove (r v s):
1. p > r premise
2. q > s premise
+
 3. p v q assumption


 m. r v s
+
m+1. (p v q) > (r v s) >i 3m
Tactic 2: Since v appears in a fact, apply the ve tactic: assume p in one box, q in another box, and try to prove (r v s) in both:
1. p > r premise
2. q > s premise
+
 3. p v q assumption
 +
  4. p assumption
 
  n. r v s
 +
 +
  n+1. q assumption
 
  m1. r v s
 +
 m. r v s ve 3, 4n, n+1m1
+
m+1. (p v q) > (r v s) >i 3m
Now, fill in the details:
1. p > r premise
2. q > s premise
+
 3. p v q assumption
 +
  4. p assumption
  5. r >e 1,4
  6. r v s vi1 5
 +
 +
  7. q assumption
  8. s >e 2,7
  9. r v s vi2 8
 +
 10. r v s ve 3, 46, 79
+
11. (p v q) > (r v s) >i 310
The tactics we used are listed in Chapter 5's Summary Section, 5.10.
The "computer code" in this proof is a function that takes as an argument a "variant value" (tagged pair/struct) and applies an ifcommand to it to compute an answer, which is itself tagged as a variant value. See the Lecture notes, Section 5.9.3.
You should think of programming and proof building as the stepwise application of goaldirected structures to solving a goal. Socalled "structure editors" help you do this. (VS is not much of a structure editor. ):