# 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)

### 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()

tuple_eq_via_elem_eq has been proven.  Now simply execute "%qed".

In [33]:
%qed

proveit.core_expr_types.tuples.tuple_eq_via_elem_eq has been proven.

Out[33]:
step typerequirementsstatement
0modus ponens1, 2
1instantiation3
:
2instantiation33, 4, 5
: , :
3conjecture
proveit.numbers.number_sets.natural_numbers.fold_forall_natural_pos
4generalization6
5generalization7
6instantiation22, 8, 9
: , :
7instantiation15, 10, 11, ,  ⊢
: , : , :
8instantiation33, 12, 13
: , :
9instantiation14
: , : , : , :
10instantiation15, 16, 17, ,  ⊢
: , : , :
11instantiation25, 18
: , : , :
12axiom
proveit.logic.booleans.true_axiom
13assumption
14instantiation36, 53, 19*, 20*, 21*
:
15theorem
proveit.logic.equality.sub_right_side_into
16instantiation22, 23, 24, ,  ⊢
: , :
17instantiation25, 26
: , : , :
18instantiation74, 75
: , :
19instantiation28, 53, 82, 54, 27, 41
: , : , : , : , : , : , :
20instantiation28, 53, 82, 54, 29, 42
: , : , : , : , : , : , :
21instantiation30, 31, 32
: , : , :
22theorem
proveit.logic.equality.lhs_via_equality
23instantiation33, 34, 35, ,  ⊢
: , :
24instantiation36, 75
: , : , : , : , :
25conjecture
proveit.core_expr_types.tuples.merge_extension
26instantiation74, 75
: , :
27instantiation66, 53
: , :
28conjecture
proveit.core_expr_types.tuples.tuple_portion_substitution
29instantiation66, 53
: , :
30axiom
proveit.logic.equality.equals_transitivity
31instantiation37, 38, 39, 40, 41, 42
: , : , : , :
32instantiation43, 44
:
33theorem
proveit.logic.booleans.conjunction.and_if_both
34instantiation45, 46, ,  ⊢
: , :
35instantiation47, 75, 53, 55, 54, 56,  ⊢
: , : , : , : , :
36axiom
proveit.core_expr_types.tuples.tuple_eq_def
37axiom
proveit.core_expr_types.operations.operands_substitution
38conjecture
proveit.numbers.numerals.decimals.nat2
39instantiation48
: , :
40instantiation48
: , :
41instantiation49, 50
: , : , :
42instantiation49, 50
: , : , :
43axiom
proveit.logic.booleans.eq_true_intro
44instantiation51
:
45assumption
46instantiation52, 53, 75, 82, 54, 55, 56,  ⊢
: , : , : , : , : , :
47conjecture
proveit.logic.booleans.conjunction.any_from_and
48conjecture
proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
49axiom
proveit.core_expr_types.tuples.empty_range_def
50instantiation57, 58
:
51axiom
proveit.logic.equality.equals_reflexivity
52conjecture
proveit.logic.booleans.conjunction.some_from_and
53axiom
proveit.numbers.number_sets.natural_numbers.zero_in_nats
54conjecture
proveit.core_expr_types.tuples.tuple_len_0_typical_eq
55instantiation66, 75
: , :
56instantiation59, 67, 60, 61, 62, 63,  ⊢
: , : , : , :
57conjecture
58instantiation80, 64, 65
: , : , :
59conjecture
proveit.logic.equality.sub_in_right_operands_via_tuple
60instantiation66, 67
: , :
61instantiation68, 75
: , : , :
62assumption
63instantiation69, 70
: , : , :
64conjecture
proveit.numbers.number_sets.complex_numbers.real_within_complex
65instantiation80, 71, 72
: , : , :
66conjecture
proveit.core_expr_types.tuples.range_from1_len_typical_eq
67instantiation73, 75, 82
: , :
68conjecture
proveit.core_expr_types.tuples.extended_range_from1_len_typical_eq
69axiom
proveit.core_expr_types.tuples.range_extension_def
70instantiation74, 75
: , :
71conjecture
proveit.numbers.number_sets.real_numbers.rational_within_real
72instantiation80, 76, 77
: , : , :
73conjecture
74conjecture
proveit.core_expr_types.tuples.range_from1_len_is_nat
75instantiation80, 78, 79
: , : , :
76conjecture
proveit.numbers.number_sets.rational_numbers.int_within_rational
77instantiation80, 81, 82
: , : , :
78conjecture
proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
79assumption
80theorem
proveit.logic.sets.inclusion.superset_membership_from_proper_subset
81conjecture
proveit.numbers.number_sets.integers.nat_within_int
82theorem
proveit.numbers.numerals.decimals.nat1
*equality replacement requirements