next up previous contents
Next: Reference Material for Tutorial Up: The Nuprl Proof Development Previous: Walking About a Proof

Running Tactics 3

Execute the D 0 THENW Auto tactic by entering $\langle$C-Z$\rangle$ and move down into the new subgoal. The proof window should look like:

EDIT THM not_over_and
# top 1
1. A: ${\Bbb{P}}${i}
2. B: ${\Bbb{P}}${i}
$\vdash$ $\neg$(A $\wedge$B) $\Longleftrightarrow$ $\neg$A $\vee$$\neg$B
 
BY <refinement rule>
 
 
Now to understand how $\Longleftrightarrow$ decomposes, look at its definition:

\begin{displaymath} P\ \Longleftrightarrow\ Q =_{def} (P \Rightarrow Q) \wedge (P \Leftarrow Q)\end{displaymath}

So, $\Longleftrightarrow$ decomposes the same way that $\wedge$decomposes. Try D 0 on it. (There is no need for THENW Auto since the decomposition rule for $\wedge$ in the conclusion, doesn't generate any well-formedness subgoals. After running D 0, the proof window should look like:

EDIT THM not_over_and
# top 1 1
1. A: ${\Bbb{P}}${i}
2. B: ${\Bbb{P}}${i}
$\vdash$ $\neg$(A $\wedge$B) $\Longleftrightarrow$ $\neg$A $\vee$$\neg$B
 
BY D 0
1# $\vdash$ $\neg$(A $\wedge$B) $\Rightarrow$ $\neg$A $\vee$$\neg$B
 
2# $\vdash$ $\neg$(A $\wedge$B) $\Leftarrow$ $\neg$A $\vee$$\neg$B
 
 
Move down into each of these subgoals in turn, and run D 0 THENW Auto. The two proof nodes should look like

EDIT THM not_over_and
# top 1 1 1
1. A: ${\Bbb{P}}${i}
2. B: ${\Bbb{P}}${i}
$\vdash$ $\neg$(A $\wedge$B) $\Rightarrow$ $\neg$A $\vee$$\neg$B
 
BY D 0 THENW Auto
 
3. $\neg$(A $\wedge$B)
$\vdash$ $\neg$A $\vee$$\neg$B
 
 

and

EDIT THM not_over_and
# top 1 1 2
1. A: ${\Bbb{P}}${i}
2. B: ${\Bbb{P}}${i}
$\vdash$ $\neg$(A $\wedge$B) $\Leftarrow$ $\neg$A $\vee$$\neg$B
 
BY D 0 THENW Auto
 
3. $\neg$A $\vee$$\neg$B
$\vdash$ $\neg$(A $\wedge$B)
 
 
The partial proof you have generated so far is rather gangly and repetitive. All the steps involved running the same tactic (D 0) on the conclusion. Go back to the top of the proof and run instead the tactic GenUnivCD THENW Auto to get:

EDIT THM not_over_and
# top
$\vdash$ $\forall$A:${\Bbb{P}}${i}. $\forall$B:${\Bbb{P}}${i}. $\neg$(A $\wedge$ B) $\Longleftrightarrow$ $\neg$A $\vee$ $\neg$B
BY GenUnivCD THENW Auto
 
1# 1. A: ${\Bbb{P}}${i}
2. B: ${\Bbb{P}}${i}
3. $\neg$(A $\wedge$B)
$\vdash$ $\neg$A $\vee$$\neg$B
 
2# 1. A: ${\Bbb{P}}${i}
2. B: ${\Bbb{P}}${i}
3. $\neg$A $\vee$$\neg$B
$\vdash$ $\neg$(A $\wedge$B)
 
 

Isn't that better! GenUnivCD repeats D 0 on all, implies, is implied by, and iff terms. Sometimes GenUniv does a bit much, in which case UnivCD is the tactic to use. UnivCD is like GenUnivCD but it stops at and and iff terms.

Move down into the first subgoal and open the rule box. At this point in the proof, it is appropriate to do a case split on whether A or $\neg$A is true. That is, you need to invoke the classical rule of the excluded middle. The tactic to use is ClassDecide. It has ML type term -> tactic; It takes as its argument the proposition to do the case split on. Enter:





\begin{parbox} {25em} {\tt ClassDecide\hspace{.2em}\lower.2ex\hbox{ \framebox {\rule[-.2ex]{0em}{1.5ex}\sc space} }\hspace{.2em}}\end{parbox}




Now enter $\langle$C-O$\rangle$. The window should look like

EDIT rule of not_over_and
 
ClassDecide '\framebox {[term]} '
 
 
 
Here we are supplying a term from Nuprl's object language as an argument to an ML function, just as we did in Section 2 Enter A \framebox {\rule[-.2ex]{0em}{1.5ex}\sc return} $\langle$C-Z$\rangle$ and the tactic executes, giving the proof window:

EDIT THM not_over_and
# top 1
1. A: ${\Bbb{P}}${i}
2. B: ${\Bbb{P}}${i}
3. $\neg$(A $\wedge$B)
$\vdash$ $\neg$A $\vee$$\neg$B
 
BY ClassDecide 'A'
 
1# 4. A $\vdash$ $\neg$A $\vee$$\neg$B
 
2# 4. $\neg$A $\vdash$ $\neg$A $\vee$$\neg$B
 
 

The 2nd subgoal is easily proved by applying the tactic Sel 1 (D 0) THENW Auto , and then Hypothesis. Try first by running each of these tactics at seperate proof nodes. Then, use the THENM tactical and run instead (Sel 1 (D 0) THENM Hypothesis) THENW Auto. T1 THENM T2 runs T2 only on the main subgoal(s) produced by T1 . Well-formedness subgoals are not considered to be main subgoals. Infix tacticals in ML all have the same parsing precedence, and associate to the left. So, the parentheses around Sel 1 (D 0) THENM Hypothesis are not strictly necessary. Still, they improve readability.

It is possible to compress the depth of a proof significantly, by use of tacticals such as THENM[*]. Be careful though; once you string together more than a couple of THENM's, it can become very difficult to read a proof. On the other hand, as you become more experienced at using Nuprl, you learn of tactics such as GenUnivCD which can shorten sequences of trivial steps which are fairly uniform in nature.

The 1st subgoal is a bit harder. The main decision to make is whether to do Sel 2 (D 0) first, or D 3 first. It's instructive to each in turn!

You now know enough that you should be able to complete the proof of this theorem, and go onto prove similar theorems from propositional calculus. You almost have enough for proving theorems from predicate calculus. The main new things you need to know are how to express the theorems in Nuprl's logic, and how both quantifiers decompose on either side of the turnstile (the $\ulcorner$$\vdash$$\urcorner$ symbol in sequents which separates the hypotheses on the left from the conclusion on the right).

Note that the theorem we proved is a theorem of classical, not constructive logic. Constructive logic does not permit the unrestricted use of case splits on whether some proposition or its negation is true. (Hence the name of the tactic ClassDecide.)

next up previous contents
Next: Reference Material for Tutorial Up: The Nuprl Proof Development Previous: Walking About a Proof
Dora Abdullah, 12/4/97