In [1]:
import proveit
from proveit import defaults
from proveit import Judgment
from proveit.logic.sets import EmptySet
from proveit.logic.sets.cardinality import empty_card
from proveit import Operation, IndexedVar
from proveit.logic import Forall, InSet, Or, Boolean, in_bool, And
from proveit import A, B, Q, x, i, l, m, n, P,S
from proveit.core_expr_types import A_1_to_m
from proveit.numbers import num, Exp, Add, one, Natural, Less, zero, greater
from proveit.numbers.number_sets.natural_numbers import fold_forall_natural_pos
#from proveit.numbers.number_sets.integers import empty_nat_def
from proveit.logic.booleans.disjunction import multi_disjunction_def, empty_disjunction
from proveit.logic.booleans.disjunction import binary_closure
theory = proveit.Theory() # the theorem's theory
In [2]:
%proving closure
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
closure:
(see dependencies)
closure:
(see dependencies)
In [3]:
closure.instance_expr
In [4]:
fold_forall_natural_pos
In [5]:
from proveit import Function
from proveit import P, m
induction_inst = \
fold_forall_natural_pos.instantiate({Function(P, m):closure.instance_expr})
induction_inst: ⊢ 
First prove the base case of the induction.¶
In [6]:
induction_base = induction_inst.antecedent.operands[0]
induction_base: 
In [7]:
induction_base.prove()
Now prove the induction step assuming the induction hypothesis¶
In [8]:
induction_step = induction_inst.antecedent.operands[1]
induction_step: 
In [9]:
in_bool_conds = induction_step.instance_expr.conditions[0]
in_bool_conds: 
In [10]:
defaults.assumptions = (induction_step.conditions + [in_bool_conds])
defaults.assumptions: 
In [11]:
induction_hyp = induction_step.conditions[1]
induction_hyp: 
Splitting apart the conjunction of "in Bool" conditions is an important step
In [12]:
in_bool_cond_partition = in_bool_conds.partition(m)
in_bool_cond_partition: 
⊢ 
⊢ 
In [13]:
in_bool_conds_conjunction = And(in_bool_conds).prove()
in_bool_conds_conjunction: ⊢ 
⊢ 
In [14]:
in_bool_conds_conjunction_partition = \
in_bool_cond_partition.sub_right_side_into(in_bool_conds_conjunction)
in_bool_conds_conjunction_partition: , ⊢ 
, ⊢ 
In [15]:
in_bool_conds_conjunction_partition.derive_some(0)
, ⊢ 
Now we can instantiate the induction hypothesis
In [16]:
induction_hyp.instantiate()
, , ⊢ 
And now we will be able to prove the induction step via binary_closure and multi_disjunction_def
In [17]:
last_in_bool_cond = in_bool_conds_conjunction_partition.derive_any(1)
last_in_bool_cond: , ⊢ 
, ⊢ 
In [18]:
A_mp1 = last_in_bool_cond.element
A_mp1: 
In [19]:
binary_closure
In [20]:
binary_conclusion = binary_closure.instantiate({A:Or(A_1_to_m), B:A_mp1})
binary_conclusion: , , ⊢ 
, , ⊢ 
In [21]:
multi_disjunction_eq = multi_disjunction_def.instantiate({B:A_mp1})
multi_disjunction_eq: ⊢ 
⊢ 
In [22]:
pre_merge_conclusion = multi_disjunction_eq.sub_left_side_into(binary_conclusion)
pre_merge_conclusion: , , ⊢ 
, , ⊢ 
In [23]:
pre_merge_conclusion.inner_expr().element.operands.merge()
, , ⊢ 
In [24]:
induction_step
In [25]:
induction_step.prove()
With the base case and the induction step proven, the induction proof is easily finished.¶
In [26]:
induction_inst.derive_consequent()
In [27]:
%qed
Out[27]:
