This exercise explores a different style of automation of the sequent formulation of the same logic used in Exercise 1. This time the automation builds the proof "backwards", starting from the goal.
As you work through this exercise we expect you to learn the following:
This exercise assumes that you have completed Exercise 1. It assumes that you have installed the Haskell platform, edited a Haskell source file, and recorded proofs in the files.
The proofs you will turn in will be mechanically checked proofs. The checking is done by a Haskell program, and in order to check your proofs you will have to:
The primary difference between the natural deducation proofs of Exercise 1 and the sequent form used here is that instead of using proof structure to distinguish between premises, undischarged assumptions, and discharged assumptions, sequent-style proofs keep this information in an explicit data structure called a sequent. In general, a sequent is two lists of formulas. The list on the left is thought of as the hypotheses. The list on the right is the list of consequents. Sometimes the logic will be designed to have exactly one consequent. That is the case of the first logic we study, which follows Huth and Ryan's logic very closely. (This is suggested in Exercises 1.2, problem 6, on page 80 of HR.)
To do example 1.14 in the backward style, begin with the conclusion:
p => (q => r) |- p /\ q => r
This is expressed by the value of type Sequent, which I construct systematically as value goal in Ex2.hs:
module Ex2 where import Prop import Examples import Tactics import HR p = LetterP "p" q = LetterP "q" r = LetterP "r" lhs = ImpliesP p (ImpliesP q r) rhs = ImpliesP (AndP p q) r goal = Sequent [lhs] rhs |
|---|
A proof will be a list of rules applied to a sequent. Each rule will act on a sequent, called the goal, and replace it with a set of sequents, called the subgoals. The prove function will apply the rules to the goals, returning a list of the remaining subgoals. The replay function takes the same arguments, but annimates the intermediate steps by printing the goal being reduced and the subgoals introduced.
Applying proof to the empty list of rules yields:
*Ex2> prove goal [] Remaining Subgoals: p => q => r |- p /\ q => r
Given that the top level connective of the consequent is an implication, it is very natural to begin with implies introduction:
*Ex2> prove goal [impliesI]
Remaining Subgoals:
p /\ q, p => q => r |- r
Note that instead of creating a box, we have added a new proposition to our list of antecedents. Next we use implies elimination to reduce showing r to showing q and q implies r:
*Ex2> prove goal [impliesI, impliesE q]
Remaining Subgoals:
p /\ q, p => q => r |- q => r, p /\ q, p => q => r |- q
Note here that the implies elimination rule required an additional argument to figure out what q was, since that was not determined by pattern matching on the goal.
The proof now has two subgoals. We focus first on the first in the list, which is to show that q implies r. We again use implies elimination, this time introducing p:
*Ex2> prove goal [impliesI, impliesE q, impliesE p]
Remaining Subgoals:
p /\ q, p => q => r |- p => q => r,
p /\ q, p => q => r |- p,
p /\ q, p => q => r |- q
Now we are up to three subgoals. The first subgoal now is trivial. It is exactly an instance of one of our hypotheses. The hypothesis rule will complete this subproof.
*Ex2> prove goal [impliesI, impliesE q, impliesE p, hypothesis]
Remaining Subgoals:
p /\ q, p => q => r |- p, p /\ q, p => q => r |- q
The remaining two subgoals are basic facts about a known conjunction. To get p from p and q we use and elimination 1, supplying term q:
*Ex2> prove goal [impliesI, impliesE q, impliesE p, hypothesis, andE1 q]
Remaining Subgoals:
p /\ q, p => q => r |- p /\ q, p /\ q, p => q => r |- q
This can now be discharaged as a hypothesis:
*Ex2> prove goal [impliesI, impliesE q, impliesE p, hypothesis, andE1 q, hypothesis]
Remaining Subgoals:
p /\ q, p => q => r |- q
We complete the proof with the other and elimination rule and a final application of the hypothesis rule:
*Ex2> prove goal [impliesI, impliesE q, impliesE p, hypothesis, andE1 q, hypothesis, andE2 p, hypothesis]
QED
The entire proof can be animated with the replay command:
*Ex2> replay goal [impliesI, impliesE q, impliesE p, hypothesis, andE1 q, hypothesis, andE2 p, hypothesis]
Focus: p => q => r |- p /\ q => r
p /\ q, p => q => r |- r
Focus: p /\ q, p => q => r |- r
p /\ q, p => q => r |- q => r, p /\ q, p => q => r |- q
Focus: p /\ q, p => q => r |- q => r
p /\ q, p => q => r |- p => q => r, p /\ q, p => q => r |- p
Focus: p /\ q, p => q => r |- p => q => r
Focus: p /\ q, p => q => r |- p
p /\ q, p => q => r |- p /\ q
Focus: p /\ q, p => q => r |- p /\ q
Focus: p /\ q, p => q => r |- q
p /\ q, p => q => r |- p /\ q
Focus: p /\ q, p => q => r |- p /\ q
QED
In this proof I conveniently didn't make any mistakes. What happens when we screw up?
The most direct kind of mistake is to try to apply a rule incorrectly. For example, what if I tried to start with and introduction instead of implies introduction?
*Ex2> prove goal [andI]
Focus: p => q => r |- p /\ q => r Fails
In this case the theorem prover gives us the very informative message "Fails".
Read the source for this prover. Compare the rules in HR.hs to those in Figure 1.2 of Huth and Ryan.
Take a look at Tactics.hs. Explore simple ways to automate this proof.
Consider mechanically translating a proof from the format used in Exercise 1 to this format. There will be some potential duplication of substructure. If you don't like the duplication, see if you can come up with a (sound) rule that allows increased sharing of substructure.
Also look at L.hs and its companion example file GentzenEgs.hs, explore doing some of these proofs in that logic.