To illustrate other possibilities for the courseware beyond its role as reference material, we present a sample exercise adapted from [52]. It would be used shortly after mathematical induction was introduced to the students, and after they have had some experience with the system. The exercise is to produce a simple proof by induction. The student begins by opening a window on the following informal document:
The statement of the first exercise contains three hypertext links. The first points to the proof they are asked to complete, the second points to a short menu of inference tactics adequate for this problem, and the third points to a document containing introductory notes on induction which should support the in class discussion. When the student clicks on the theorem, a window is opened on the proof, which looks like this:
It consists only of the goal to be proved. In some other exercises, the proof supplied to the student will be partially proved; subgoals that are either to difficult or would distract from the point of the exercise would already be proved. This proof is pretty simple though.
Next, the student would probably open the menu of inference forms
to be used with this problem by clicking on
VIEW stamps_proof_menu.
This would open a window that looks like this:
Each line of this menu consists of an ``insert button'' that causes the tactic clicked on to be inserted into the proof. At this stage, the student would already be familiar with using all the tactics listed in the menu except the one for induction. We have narrowed the solution space for this exercise so that the student will not get stuck, and so that the expected kind of proof will be produced.
The first step is to apply induction. If the student clicks on the menu entry
Induction, the tactic will be inserted into the proof, and
when the student hits return, the result will be:
The result is two subgoals: the base case, and the induction case. Notice that the induction hypothesis is so-labeled.
The student may then click on either subgoal to descend into the proof. Let's say the base case is selected; this is what you'd see:
The student should recognize that he or she can now specify witness
for the conclusion. Going back to the tactic menu and clicking on
Witness <term> will simply insert Witness
<term> into the proof, whereupon the student enters the expression
for a witness into the slot marked <term>, say 3. Although it
not necessary, the student could specify witness for both existential
variables at once by chaining two Witness tactics with the THEN tactic from the menu. The result would be:
There are no more subgoals since the system recognizes the truth of the equation given these witnesses.
Clicking on the goal will take us back to the next inference step above, which now looks like
The * indicates that that subproof is finished, leaving us to prove the other subgoal. Clicking on it will cause us to descend into that incomplete subproof and the only obviously (to the student) applicable tactic from the menu is to analyze the existential assumption of the inductive hypotheses.
Then down into the new subgoal and analyze assumption 4 in the same way:
In order to build witnesses for the conclusion from the variables of the hypotheses, we must know which way to do the stamp replacements suggested in the problem. Perhaps the student considers the replacing 3 2-cent stamps; then we need to know there are at least 3 of them to replace. The case splitting tactic from the menu is handy for this decision:
These two subgoals are easy to finish off:
and
The proof is then complete, as could be observed by going to the top of the proof and finding it marked with a *.