public class ProofByInduction
1: import java.util.Scanner;
3: /**
4: * A program to print out the skeleton of a proof-by-induction.
5: *
6: * @author Mark Young (A00000000)
7: */
8: public class ProofByInduction {
10: public static final Scanner KBD = new Scanner(System.in);
11:
12: /**
13: * @param args the command line arguments
14: */
15: public static void main(String[] args) {
16: printIntroduction();
17:
18: // choose kind of induction (linear/binary)
19: System.out.print("Does your recurrence relation use subtraction "
20: + "or division? ");
21: String choice = KBD.nextLine().toLowerCase();
22: if ("subtraction".startsWith(choice)) {
23: doLinear();
24: } else if ("division".startsWith(choice)) {
25: doBinary();
26: } else {
27: System.out.println("Sorry, I didn't understand that!");
28: }
29: }
30:
31: /**
32: * Get recurrence and formula, and show skeleton of proof of W(N) in terms
33: * of N - 1.
34: */
35: private static void doLinear() {
36: System.out.print("What is your recurrence relation: W(N) = ");
37: String recurrence = KBD.nextLine().replaceAll("N-1", "N - 1");
38: System.out.print("What is your formula for work? W(N) = ");
39: String formula = KBD.nextLine();
40: doInduction("N - 1", recurrence, formula);
41: }
42:
43: /**
44: * Get recurrence and formula, and show skeleton of proof of W(N) in terms
45: * of N/2.
46: */
47: private static void doBinary() {
48: System.out.print("What is your recurrence relation: W(N) = ");
49: String recurrence = KBD.nextLine().replaceAll("N / 2", "N/2");
50: System.out.print("What is your formula for work? W(N) = ");
51: String formula = KBD.nextLine();
52: doInduction("N/2", recurrence, formula);
53: }
54:
55: /**
56: * Print the skeleton of a proof by induction.
57: *
58: * @param smaller the value less than N that we're working in terms of
59: * @param recurrence the rhs of the recurrence relation
60: * @param formula the rhs of the formula for work
61: */
62: private static void doInduction(String smaller,
63: String recurrence, String formula) {
64: // create versions with W(N) = at start
65: String recurrenceEquation = "W(N) = " + recurrence;
66: String formulaEquation = "W(N) = " + formula;
67:
68: // separate from input
69: System.out.println("\n\n\n----------------------------------------\n");
70:
71: // print what's to be proved
72: System.out.println("Proof by Induction");
73: System.out.println("Given that " + recurrenceEquation + ",");
74: System.out.println("prove that " + formulaEquation + ".");
75: System.out.println();
76:
77: // make inductive assumption
78: System.out.println("Let's assume that "
79: + formulaEquation.replace("N", "n")
80: + " is true for all n < N.");
81:
82: // note that smaller is smaller
83: System.out.println("Well, " + smaller + " < N,");
84: String formulaNMinus1 = formula.replace("N", "(" + smaller + ")");
85: System.out.println("so W(" + smaller + ") = "
86: + formulaNMinus1 + ".");
87:
88: // substitute into recurrence equation
89: System.out.println("But " + recurrenceEquation + ",");
90: String expanded = recurrence.replace("W(" + smaller + ")",
91: "(" + formulaNMinus1 + ")");
92: System.out.println("so W(N) = " + expanded + ".");
93:
94: // do some math (need human input here)
95: System.out.println("... (expand and simplify) ...");
96: System.out.println("... (may take multiple lines) ...");
97:
98: // state conclusion
99: System.out.println("and thus " + formulaEquation + " for all N.");
100: System.out.println("Q.E.D.");
101: }
103: /**
104: * Print a description and instructions for this program.
105: */
106: private static void printIntroduction() {
107: System.out.println("This program will print out the shell of a proof "
108: + "by induction.\n\n"
109: + "You need to provide the recurrence relation "
110: + "and the supposed equation of work.\n\n"
111: + "The recurrence relation needs to use subtraction "
112: + "(W(N) = ... W(N - 1) ...)\n"
113: + "or division (W(N) = ... W(N/2) ...).\n\n"
114: + "This is a very simple program, so it can't handle anything "
115: + "more complicated than that!\n\n");
116: }
118: }