Proof of proveit.numbers.summation.finite_geom_sum theorem¶
In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import a, defaults, Function, m, n, P, x
from proveit.logic import Equals, InSet, Not, NotEquals
from proveit.numbers import zero, one, Add, Div, frac, Less, LessEq, Mult, Neg, subtract
from proveit.numbers import Complex, Natural
from proveit.numbers.negation import neg_not_eq_zero
from proveit.numbers.number_sets.natural_numbers import fold_forall_natural
In [2]:
%proving finite_geom_sum
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
finite_geom_sum:
(see dependencies)
finite_geom_sum:
(see dependencies)
In [3]:
defaults.assumptions = finite_geom_sum.all_conditions()
defaults.assumptions: 
In [4]:
Mult.change_simplification_directives(combine_all_exponents=True)
Instantiate the Induction Theorem for an induction proof¶
In [5]:
finite_geom_sum.instance_expr
In [6]:
fold_forall_natural
In [7]:
induction_inst = fold_forall_natural.instantiate({Function(P,n):finite_geom_sum.instance_expr})
induction_inst: 
, 
⊢ 
, 
⊢ 
Note that the base case was proven automatically via auto-simplification.
Inductive Step¶
In [8]:
inductive_step = induction_inst.antecedent.operands[1]
inductive_step: 
In [9]:
inductive_step.conditions.entries
In [10]:
defaults.assumptions = defaults.assumptions + inductive_step.conditions.entries
defaults.assumptions: 
In [11]:
sum_zero_to_m_plus_one = induction_inst.antecedent.operands[1].instance_expr.lhs
sum_zero_to_m_plus_one: 
In [12]:
zero_less_eq_m = LessEq(zero, m).prove()
zero_less_eq_m: 
⊢ 
⊢ 
In [13]:
zero_less_eq_m.right_add_both_sides(one)
In [14]:
zero_less_than_m_plus_1 = Less(zero, Add(m, one)).prove()
zero_less_than_m_plus_1: ⊢ 
⊢ 
In [15]:
# also need to have m+1 != -1 for later inductive step(s)
neg_one_less_than_m_plus_1 = zero_less_than_m_plus_1.add_left(Neg(one))
neg_one_less_than_m_plus_1: ⊢ 
⊢ 
In [16]:
NotEquals(Neg(one), Add(m, one)).prove()
In [17]:
sum_zero_to_m_plus_one_split = sum_zero_to_m_plus_one.partition_last()
sum_zero_to_m_plus_one_split: ⊢ 
⊢ 
In [18]:
for the_assumption in defaults.assumptions:
if isinstance(the_assumption, Equals):
print("{}".format(the_assumption))
inductive_hypothesis = the_assumption
inductive_hypothesis
In [19]:
inductive_hypothesis_judgment = inductive_hypothesis.prove()
inductive_hypothesis_judgment: 
⊢
⊢ In [20]:
sum_zero_to_m_plus_one_simplified_01 = inductive_hypothesis_judgment.sub_right_side_into(sum_zero_to_m_plus_one_split)
sum_zero_to_m_plus_one_simplified_01: , ⊢ 
, ⊢ 
In [21]:
alg_expr_01 = sum_zero_to_m_plus_one_simplified_01.rhs.operands[1]
alg_expr_01: 
In [22]:
alg_expr_02 = frac(Mult(subtract(one, x), alg_expr_01), subtract(one, x))
alg_expr_02: 
In [23]:
alg_manip_01 = alg_expr_02.cancelation(subtract(one, x))
alg_manip_01: , , ⊢ 
, , ⊢ 
In [24]:
sum_zero_to_m_plus_one_simplified_02 = (
alg_manip_01.sub_left_side_into(sum_zero_to_m_plus_one_simplified_01.
inner_expr().rhs.operands[1]))
sum_zero_to_m_plus_one_simplified_02: , , , ⊢ 
, , , ⊢ 
In [25]:
sum_zero_to_m_plus_one_simplified_03 = sum_zero_to_m_plus_one_simplified_02.inner_expr().rhs.operands[1].numerator.distribute(0)
sum_zero_to_m_plus_one_simplified_03: , , , ⊢ 
, , , ⊢ 
In [26]:
sum_zero_to_m_plus_one_simplified_04 = sum_zero_to_m_plus_one_simplified_03.inner_expr().rhs.factor(frac(one, subtract(one, x)))
sum_zero_to_m_plus_one_simplified_04: , , , ⊢ 
, , , ⊢ 
In [27]:
Less(Neg(one), Add(m, one)).prove()
In [28]:
sum_zero_to_m_plus_one_formula = inductive_step.instance_expr.rhs.factorization(frac(one, subtract(one, x)))
sum_zero_to_m_plus_one_formula: , , ⊢ 
, , ⊢ 
In [29]:
sum_zero_to_m_plus_one_formula.inner_expr().rhs.operands[1].operands[1].operand.exponent.commute()
, , ⊢ 
In [30]:
inductive_step.instance_expr.conclude_via_transitivity()
, , , ⊢ 
In [31]:
inductive_step.prove()
, ⊢
Finishing Up¶
The final steps are a little complicated because of the extra constraints in the theorem imposed on $x$ (i.e. $x \in \mathbb{C}, x \ne 1$), so we derive the consequent but then instantiate to get domains and conditions as assumptions, and then generalize over the $x$ and $n$ simultaneously.
In [32]:
induction_inst_consequent_intermediate = induction_inst.derive_consequent()
induction_inst_consequent_intermediate: , ⊢ 
, ⊢ 
In [33]:
induction_inst_consequent_intermediate_inst = induction_inst_consequent_intermediate.instantiate({n:n})
induction_inst_consequent_intermediate_inst: , , 
⊢ 
, , 
⊢ In [34]:
induction_inst_consequent_intermediate_inst.generalize([x,n], domain_lists=[[Complex, Natural]], conditions=[NotEquals(x, one)])
In [35]:
%qed
Out[35]:
