Proof of proveit.core_expr_types.tuples.tuple_eq_via_elem_eq theorem¶
In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import defaults
from proveit import a, b, c, d, m
from proveit.core_expr_types.tuples import tuple_eq_def
from proveit.logic import And
from proveit.numbers import Add, zero, one
from proveit.numbers.number_sets.natural_numbers import fold_forall_natural_pos
In [2]:
%proving tuple_eq_via_elem_eq
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
tuple_eq_via_elem_eq:
(see dependencies)
tuple_eq_via_elem_eq:
(see dependencies)
Instantiate the induction theorem for an inductive proof.¶
In [3]:
tuple_eq_via_elem_eq.instance_expr
In [4]:
fold_forall_natural_pos
In [5]:
from proveit import Function
from proveit import P, i
induction_inst = \
fold_forall_natural_pos.instantiate({Function(P, i):tuple_eq_via_elem_eq.instance_expr}) \
.inner_expr().with_wrapping_at(1).inner_expr().antecedent.with_wrapping_at(1) \
.inner_expr().antecedent.operands[1].with_wrapping()
induction_inst: ⊢ 
First prove the base case of the induction.¶
In [6]:
induction_base = induction_inst.antecedent.operands[0]
induction_base: 
In [7]:
a1, b1 = induction_base.instance_params
a1: 
b1: 
In [8]:
tuple_eq_def
In [9]:
tuple_eq_base = tuple_eq_def.instantiate({i:zero})
tuple_eq_base: ⊢ 
In [10]:
tuple_eq_base_inst = tuple_eq_base.instantiate({b:a1, d:b1})
tuple_eq_base_inst: ⊢ 
In [11]:
tuple_eq_base_inst.rhs.prove(assumptions=induction_base.conditions)
In [12]:
tuple_eq_base_inst.derive_left_via_equality(assumptions=induction_base.conditions)
In [13]:
induction_base.prove()
Now prove the induction step assuming the induction hypothesis¶
In [14]:
induction_step = induction_inst.antecedent.operands[1].with_wrapping()
induction_step: 
In [15]:
eq_conds = induction_step.instance_expr.explicit_conditions()[0]
eq_conds: 
In [16]:
defaults.assumptions = (induction_step.conditions + [eq_conds])
defaults.assumptions: 
In [17]:
induction_hyp = induction_step.conditions[1]
induction_hyp: 
Splitting apart the conjunction of equality conditions is an important step
In [18]:
eq_cond_partition = eq_conds.partition(m)
eq_cond_partition: 
⊢ 
⊢ 
In [19]:
eq_conds_conjunction = And(eq_conds).prove()
eq_conds_conjunction: ⊢ 
⊢ 
In [20]:
eq_conds_conjunction_partition = eq_cond_partition.sub_right_side_into(eq_conds_conjunction)
eq_conds_conjunction_partition: , ⊢ 
, ⊢ 
In [21]:
eq_conds_conjunction_partition.derive_some(0)
, ⊢ 
Now we can instantiate the induction hypothesis
In [22]:
induction_hyp.instantiate()
, , ⊢ 
And now we will be able to prove the induction step by invoking the tuple_eq_def axiom
In [23]:
last_eq = eq_conds_conjunction_partition.derive_any(1)
last_eq: , ⊢ 
, ⊢ 
In [24]:
a_mp1, b_mp1 = last_eq.operands
a_mp1: 
b_mp1: 
In [25]:
tuple_eq_def
In [26]:
tuple_eq_def_inst = tuple_eq_def.instantiate({i:m, c:b, b:a_mp1, d:b_mp1})
tuple_eq_def_inst: ⊢ 
⊢ 
In [27]:
tuple_eq_def_inst.rhs.prove()
, , ⊢ 
In [28]:
tuple_eq_split_both = tuple_eq_def_inst.derive_left_via_equality()
tuple_eq_split_both: , , ⊢ 
, , ⊢ 
In [29]:
tuple_eq_split_right = tuple_eq_split_both.inner_expr().lhs.merge()
tuple_eq_split_right: , , ⊢ 
, , ⊢ 
In [30]:
tuple_eq = tuple_eq_split_right.inner_expr().rhs.merge()
tuple_eq: , , ⊢ 
, , ⊢ 
In [31]:
induction_step.prove()
With the base case and the induction step proven, the induction proof is easily finished.¶
In [32]:
induction_inst.derive_consequent()
In [33]:
%qed
Out[33]:
