# Proof of proveit.logic.booleans.disjunction.closure theorem¶

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

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

In [27]:
%qed

proveit.logic.booleans.disjunction.closure has been proven.

Out[27]:
step typerequirementsstatement
0modus ponens1, 2
1instantiation3, 4, 5*
:
2instantiation6, 7, 8
: , :
3conjecture
proveit.numbers.number_sets.natural_numbers.fold_forall_natural_pos
4instantiation9, 10, 11
: , : , :
5instantiation12, 13
:
6theorem
proveit.logic.booleans.conjunction.and_if_both
7generalization13
8generalization14
9axiom
proveit.logic.equality.equals_transitivity
10instantiation15, 56, 18, 71, 57, 16, 20, 21
: , : , : , : , : , :
11instantiation17, 71, 18, 56, 19, 57, 20, 21, 22*
: , : , : , : , : , :
12conjecture
proveit.logic.booleans.disjunction.unary_or_reduction
13assumption
14instantiation60, 66, 23, 24, 25, 26, ,  ⊢
: , : , : , :
15conjecture
16instantiation27
: , :
17conjecture
18conjecture
proveit.numbers.numerals.decimals.nat2
19instantiation27
: , :
20instantiation74, 29, 28
: , : , :
21instantiation74, 29, 30
: , : , :
22conjecture
23instantiation67, 73
: , : , :
24instantiation65, 66
: , :
25instantiation31, 32, 33, ,  ⊢
: , : , :
26instantiation34, 35
: , : , :
27conjecture
proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
28instantiation36, 37, 38
: , : , :
29conjecture
proveit.numbers.number_sets.complex_numbers.real_within_complex
30instantiation74, 39, 40
: , : , :
31conjecture
proveit.logic.equality.sub_left_side_into
32instantiation41, 42, 43, ,  ⊢
: , :
33instantiation44, 73
: , : , :
34conjecture
proveit.core_expr_types.tuples.merge_extension
35instantiation72, 73
: , :
36conjecture
proveit.logic.sets.inclusion.unfold_subset_eq
37instantiation45, 46
: , :
38instantiation47, 48
: , :
39conjecture
proveit.numbers.number_sets.real_numbers.rational_within_real
40instantiation74, 49, 50
: , : , :
41conjecture
proveit.logic.booleans.disjunction.binary_closure
42instantiation51, 52, ,  ⊢
:
43instantiation53, 73, 56, 58, 57, 59,  ⊢
: , : , : , : , :
44axiom
proveit.logic.booleans.disjunction.multi_disjunction_def
45theorem
proveit.logic.sets.inclusion.relax_proper_subset
46conjecture
proveit.numbers.number_sets.real_numbers.nat_pos_within_real
47theorem
proveit.logic.booleans.conjunction.left_from_and
48assumption
49conjecture
proveit.numbers.number_sets.rational_numbers.int_within_rational
50instantiation74, 54, 71
: , : , :
51assumption
52instantiation55, 56, 73, 71, 57, 58, 59,  ⊢
: , : , : , : , : , :
53conjecture
proveit.logic.booleans.conjunction.any_from_and
54conjecture
proveit.numbers.number_sets.integers.nat_within_int
55conjecture
proveit.logic.booleans.conjunction.some_from_and
56axiom
proveit.numbers.number_sets.natural_numbers.zero_in_nats
57conjecture
proveit.core_expr_types.tuples.tuple_len_0_typical_eq
58instantiation65, 73
: , :
59instantiation60, 66, 61, 62, 63, 64,  ⊢
: , : , : , :
60conjecture
proveit.logic.equality.sub_in_right_operands_via_tuple
61instantiation65, 66
: , :
62instantiation67, 73
: , : , :
63assumption
64instantiation68, 69
: , : , :
65conjecture
proveit.core_expr_types.tuples.range_from1_len_typical_eq
66instantiation70, 73, 71
: , :
67conjecture
proveit.core_expr_types.tuples.extended_range_from1_len_typical_eq
68axiom
proveit.core_expr_types.tuples.range_extension_def
69instantiation72, 73
: , :
70conjecture