generator_for_weak_nat_induction.py

#!/usr/bin/env python3

# 歸納法樣板
class InductionProof:
  def induction(self, tabs, n):
    if n == 1:
      return tabs + self.base_case.replace("n", str(n))
    else:
      m = n-1
      inductive_hypothesis = "\n".join(tabs + s for s in self.induction(tabs, m).split("\n"))
      proof = self.inductive_case.replace("n", str(n)).replace("m", str(m))
      proof = proof.replace("由歸納假設", inductive_hypothesis)
      proof_lines = proof.split("\n")
      proof_lines = \
        ["/ " + proof_lines[0]] + \
        ["| " + s for s in proof_lines[1:-1]] + \
        ["\\ " + proof_lines[-1]]
      return "\n".join(proof_lines)

  def __init__(self, base_case, inductive_case):
    self.base_case = base_case
    self.inductive_case = inductive_case
  def __call__(self, n):
    return self.induction("      ", n) + "\n"

# 證明 1+2+...+n = n(n+1)/2
sum_k = InductionProof( \
  # 當 n = 1
  base_case = "n = n*(n+1)/2, 式子成立", \
  # 當 n = m+1
  inductive_case = """
1+...+n
= 1+...+m+(m+1)
= (1+...+m)+(m+1)
由歸納假設
= m(m+1)/2 + (m+1)
= (m+1)(m/2 + 1)
= (m+1)(m+2)/2
= (m+1)((m+1)+1)/2
= n(n+1)/2
""")

print(sum_k(7))


"""
$ python3 generator_for_weak_nat_induction.py
/
| 1+...+7
| = 1+...+6+(6+1)
| = (1+...+6)+(6+1)
|       /
|       | 1+...+6
|       | = 1+...+5+(5+1)
|       | = (1+...+5)+(5+1)
|       |       /
|       |       | 1+...+5
|       |       | = 1+...+4+(4+1)
|       |       | = (1+...+4)+(4+1)
|       |       |       /
|       |       |       | 1+...+4
|       |       |       | = 1+...+3+(3+1)
|       |       |       | = (1+...+3)+(3+1)
|       |       |       |       /
|       |       |       |       | 1+...+3
|       |       |       |       | = 1+...+2+(2+1)
|       |       |       |       | = (1+...+2)+(2+1)
|       |       |       |       |       /
|       |       |       |       |       | 1+...+2
|       |       |       |       |       | = 1+...+1+(1+1)
|       |       |       |       |       | = (1+...+1)+(1+1)
|       |       |       |       |       |             1 = 1*(1+1)/2, 式子成立
|       |       |       |       |       | = 1(1+1)/2 + (1+1)
|       |       |       |       |       | = (1+1)(1/2 + 1)
|       |       |       |       |       | = (1+1)(1+2)/2
|       |       |       |       |       | = (1+1)((1+1)+1)/2
|       |       |       |       |       | = 2(2+1)/2
|       |       |       |       |       \
|       |       |       |       | = 2(2+1)/2 + (2+1)
|       |       |       |       | = (2+1)(2/2 + 1)
|       |       |       |       | = (2+1)(2+2)/2
|       |       |       |       | = (2+1)((2+1)+1)/2
|       |       |       |       | = 3(3+1)/2
|       |       |       |       \
|       |       |       | = 3(3+1)/2 + (3+1)
|       |       |       | = (3+1)(3/2 + 1)
|       |       |       | = (3+1)(3+2)/2
|       |       |       | = (3+1)((3+1)+1)/2
|       |       |       | = 4(4+1)/2
|       |       |       \
|       |       | = 4(4+1)/2 + (4+1)
|       |       | = (4+1)(4/2 + 1)
|       |       | = (4+1)(4+2)/2
|       |       | = (4+1)((4+1)+1)/2
|       |       | = 5(5+1)/2
|       |       \
|       | = 5(5+1)/2 + (5+1)
|       | = (5+1)(5/2 + 1)
|       | = (5+1)(5+2)/2
|       | = (5+1)((5+1)+1)/2
|       | = 6(6+1)/2
|       \
| = 6(6+1)/2 + (6+1)
| = (6+1)(6/2 + 1)
| = (6+1)(6+2)/2
| = (6+1)((6+1)+1)/2
| = 7(7+1)/2
\ 
"""

induction.py

#!/usr/bin/env python3

# 證明 1+2+...+n = n(n+1)/2
def induction(tabs,n):
  if n == 1:                                       # Base case: 當 n = 1
    print("%s%d*(%d+1)/2 = %d, 成立."                 #     1*(1+1)/2 = 1, 式子成立
         % (tabs,n,n,n))
  else:
    m = n-1                                        # Inductive case: 當 n = m+1
    print("%s/ 1+2+...+%d+(%d+1)"%(tabs,m,m))        # / 1+2+...+m+(m+1)
    print("%s| = (1+2+...+%d)+(%d+1)"%(tabs,m,m))    # | = (1+2+...+m)+(m+1)
    induction(tabs+"|       ",m)                     # | 由歸納假設, (1+2+...+m)=m(m+1)/2
    print("%s| = %d*(%d+1)/2 +(%d+1)"%(tabs,m,m,m))  # | = m*(m+1)/2 + (m+1)
    print("%s| = (%d/2 + 1)(%d+1)"%(tabs,m,m))       # | = (m/2 + 1)(m+1)
    print("%s| = (%d+2)(%d+1)/2"%(tabs,m,m))         # | = (m+2)(m+1)/2
    print("%s\\ = (%d+1)((%d+1)+1)/2"%(tabs,m,m))    # \ = (m+1)((m+1)+1)/2 也成立

induction("",7)

"""
$ python3 induction.py
/ 1+2+...+6+(6+1)
| = (1+2+...+6)+(6+1)
|       / 1+2+...+5+(5+1)
|       | = (1+2+...+5)+(5+1)
|       |       / 1+2+...+4+(4+1)
|       |       | = (1+2+...+4)+(4+1)
|       |       |       / 1+2+...+3+(3+1)
|       |       |       | = (1+2+...+3)+(3+1)
|       |       |       |       / 1+2+...+2+(2+1)
|       |       |       |       | = (1+2+...+2)+(2+1)
|       |       |       |       |       / 1+2+...+1+(1+1)
|       |       |       |       |       | = (1+2+...+1)+(1+1)
|       |       |       |       |       |       1*(1+1)/2 = 1, 成立.
|       |       |       |       |       | = 1*(1+1)/2 +(1+1)
|       |       |       |       |       | = (1/2 + 1)(1+1)
|       |       |       |       |       | = (1+2)(1+1)/2
|       |       |       |       |       \ = (1+1)((1+1)+1)/2
|       |       |       |       | = 2*(2+1)/2 +(2+1)
|       |       |       |       | = (2/2 + 1)(2+1)
|       |       |       |       | = (2+2)(2+1)/2
|       |       |       |       \ = (2+1)((2+1)+1)/2
|       |       |       | = 3*(3+1)/2 +(3+1)
|       |       |       | = (3/2 + 1)(3+1)
|       |       |       | = (3+2)(3+1)/2
|       |       |       \ = (3+1)((3+1)+1)/2
|       |       | = 4*(4+1)/2 +(4+1)
|       |       | = (4/2 + 1)(4+1)
|       |       | = (4+2)(4+1)/2
|       |       \ = (4+1)((4+1)+1)/2
|       | = 5*(5+1)/2 +(5+1)
|       | = (5/2 + 1)(5+1)
|       | = (5+2)(5+1)/2
|       \ = (5+1)((5+1)+1)/2
| = 6*(6+1)/2 +(6+1)
| = (6/2 + 1)(6+1)
| = (6+2)(6+1)/2
\ = (6+1)((6+1)+1)/2
"""