logo

Proof of proveit.numbers.ordering.max_bin_args_commute theorem

In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import x, y, defaults
from proveit.logic import Not
from proveit.numbers import greater_eq
from proveit.numbers.ordering import (
        less_eq_def, less_or_greater_eq, max_def_bin)
In [2]:
%proving max_bin_args_commute
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
max_bin_args_commute:
(see dependencies)
In [3]:
defaults.assumptions = max_bin_args_commute.conditions
defaults.assumptions:
In [4]:
max_def_bin
 ⊢  
In [5]:
max_x_y_def = max_def_bin.instantiate({x: x, y: y})
max_x_y_def: ,  ⊢  
In [6]:
max_y_x_def = max_def_bin.instantiate({x: y, y: x})
max_y_x_def: ,  ⊢  
In [7]:
less_or_greater_eq
 ⊢  
In [8]:
relation_choices = less_or_greater_eq.instantiate({x: x, y: y})
relation_choices: ,  ⊢  

Case 1: $x < y$

In [9]:
case_1_assumptions = defaults.assumptions+(relation_choices.operands[0],)
case_1_assumptions:
In [10]:
max_x_y_def.inner_expr().rhs.simplify(assumptions=case_1_assumptions)
, ,  ⊢  
In [11]:
max_y_x_def.inner_expr().rhs.simplify(assumptions=case_1_assumptions)
, ,  ⊢  

Case 2: $x \ge y$

In [12]:
case_2_assumptions = defaults.assumptions+(relation_choices.operands[1],)
case_2_assumptions:
In [13]:
case_2_non_implication = max_x_y_def.inner_expr().rhs.simplify(assumptions=case_2_assumptions)
case_2_non_implication: , ,  ⊢  

Then for later we seem to need this in implication form:

In [14]:
from proveit.logic import Implies
Implies(greater_eq(x, y), case_2_non_implication).prove()
,  ⊢  

The second part of Case 2 needs to be broken up into two pieces.

In [15]:
less_eq_def
 ⊢  
In [16]:
x_ge_y_as_disjunction = less_eq_def.instantiate({x: y, y: x})
x_ge_y_as_disjunction:  ⊢  
In [17]:
x_ge_y_as_disjunction.derive_right_via_equality(assumptions=case_2_assumptions)
 ⊢  
In [18]:
case_2_a_assumptions = defaults.assumptions + (x_ge_y_as_disjunction.rhs.operands[0],)
case_2_a_assumptions:
In [19]:
max_y_x_def.inner_expr().rhs.simplify(assumptions=case_2_a_assumptions)
, ,  ⊢  
In [20]:
case_2_b_assumptions = defaults.assumptions + (x_ge_y_as_disjunction.rhs.operands[1],)
case_2_b_assumptions:
In [21]:
# Need this piece explicitly ---
# y >= x is not derived as an automatic side-effect from y = x
greater_eq(y, x).prove(assumptions=case_2_b_assumptions)
, ,  ⊢  
In [22]:
max_y_x_when_y_eq_x = max_y_x_def.inner_expr().rhs.simplify(assumptions=case_2_b_assumptions)
max_y_x_when_y_eq_x: , ,  ⊢  
In [23]:
case_2_b_non_implication = max_y_x_when_y_eq_x.inner_expr().rhs.substitute(x,
        assumptions=case_2_b_assumptions, auto_simplify=False)
case_2_b_non_implication: , ,  ⊢  

Recall the full Case (2) conditions, and combine the two sub-cases of Case (2) into a single conclusion:

In [24]:
x_ge_y_as_disjunction
 ⊢  
In [25]:
x_ge_y_as_disjunction.rhs.derive_via_singular_dilemma(
        max_bin_args_commute.instance_expr,
        assumptions=defaults.assumptions+(x_ge_y_as_disjunction.lhs,))
, ,  ⊢  

Now we're ready for combining Cases (1) and (2) using derive_via_singular_dilemma() and the default assumptions:

In [26]:
relation_choices.expr.derive_via_singular_dilemma(
    max_bin_args_commute.instance_expr)
,  ⊢   
max_bin_args_commute may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".
In [27]:
%qed

proveit.numbers.ordering.max_bin_args_commute has been proven.
Out[27]:
 step typerequirementsstatement
0generalization1  ⊢  
1instantiation11, 2, 3, 9, 4, 5,  ⊢  
  : , : , :
2instantiation19, 6,  ⊢  
  : , :
3instantiation20, 6,  ⊢  
  : , :
4deduction7,  ⊢  
5deduction8,  ⊢  
6instantiation26, 9,  ⊢  
  :
7instantiation53, 10, 51, ,  ⊢  
  : , : , :
8instantiation11, 12, 13, 27, 14, 15, ,  ⊢  
  : , : , :
9instantiation16, 95, 96,  ⊢  
  : , :
10instantiation53, 17, 18, ,  ⊢  
  : , : , :
11theorem  ⊢  
 proveit.logic.booleans.disjunction.singular_constructive_dilemma
12instantiation19, 21  ⊢  
  : , :
13instantiation20, 21  ⊢  
  : , :
14deduction22, ,  ⊢  
15deduction23, ,  ⊢  
16conjecture  ⊢  
 proveit.numbers.ordering.less_or_greater_eq
17instantiation50, 38, 24, ,  ⊢  
  : , : , :
18instantiation70, 25, 56, ,  ⊢  
  : , : , :
19axiom  ⊢  
 proveit.logic.booleans.disjunction.left_in_bool
20axiom  ⊢  
 proveit.logic.booleans.disjunction.right_in_bool
21instantiation26, 27  ⊢  
  :
22instantiation53, 28, 38, , ,  ⊢  
  : , : , :
23instantiation53, 29, 51, , ,  ⊢  
  : , : , :
24instantiation70, 30, 31, ,  ⊢  
  : , : , :
25instantiation70, 32, 33, ,  ⊢  
  : , : , :
26conjecture  ⊢  
 proveit.logic.booleans.in_bool_if_true
27instantiation34, 93, 35  ⊢  
  : , :
28instantiation53, 36, 54, , ,  ⊢  
  : , : , :
29instantiation53, 37, 38, , ,  ⊢  
  : , : , :
30instantiation70, 39, 40, ,  ⊢  
  : , : , :
31instantiation73, 75, 74, 76  ⊢  
  : , : , : , : , :
32instantiation82, 41  ⊢  
  : , : , :
33instantiation82, 42, ,  ⊢  
  : , : , :
34theorem  ⊢  
 proveit.logic.equality.rhs_via_equality
35instantiation43  ⊢  
  : , :
36instantiation98, 44, ,  ⊢  
  : , :
37instantiation53, 45, 46, , ,  ⊢  
  : , : , :
38instantiation59, 95, 96,  ⊢  
  : , :
39instantiation82, 47, ,  ⊢  
  : , : , :
40instantiation82, 48  ⊢  
  : , : , :
41instantiation86, 58  ⊢  
  : , :
42instantiation87, 49, ,  ⊢  
  : , :
43axiom  ⊢  
 proveit.numbers.ordering.less_eq_def
44instantiation50, 51, 52, ,  ⊢  
  : , : , :
45instantiation53, 97, 54, , ,  ⊢  
  : , : , :
46instantiation70, 55, 56, ,  ⊢  
  : , : , :
47instantiation87, 57, ,  ⊢  
  : , :
48instantiation86, 67  ⊢  
  : , :
49instantiation92, 95, 96, 58, ,  ⊢  
  : , :
50theorem  ⊢  
 proveit.logic.equality.sub_right_side_into
51instantiation59, 96, 95,  ⊢  
  : , :
52instantiation70, 60, 61, ,  ⊢  
  : , : , :
53theorem  ⊢  
 proveit.logic.equality.sub_left_side_into
54instantiation70, 62, 63, ,  ⊢  
  : , : , :
55instantiation70, 64, 65, ,  ⊢  
  : , : , :
56instantiation73, 74, 75, 76  ⊢  
  : , : , : , : , :
57instantiation90, 95, 96, 67, ,  ⊢  
  : , :
58instantiation66, 67  ⊢  
  : , :
59axiom  ⊢  
 proveit.numbers.ordering.max_def_bin
60instantiation70, 68, 69, ,  ⊢  
  : , : , :
61instantiation73, 75, 74, 76  ⊢  
  : , : , : , : , :
62instantiation70, 71, 72, ,  ⊢  
  : , : , :
63instantiation73, 74, 75, 76  ⊢  
  : , : , : , : , :
64instantiation82, 77, ,  ⊢  
  : , : , :
65instantiation82, 78, ,  ⊢  
  : , : , :
66conjecture  ⊢  
 proveit.numbers.ordering.relax_less
67assumption  ⊢  
68instantiation82, 79, ,  ⊢  
  : , : , :
69instantiation82, 80  ⊢  
  : , : , :
70axiom  ⊢  
 proveit.logic.equality.equals_transitivity
71instantiation82, 81  ⊢  
  : , : , :
72instantiation82, 83, ,  ⊢  
  : , : , :
73axiom  ⊢  
 proveit.core_expr_types.conditionals.true_case_reduction
74axiom  ⊢  
 proveit.numbers.number_sets.natural_numbers.zero_in_nats
75theorem  ⊢  
 proveit.numbers.numerals.decimals.nat1
76conjecture  ⊢  
 proveit.core_expr_types.tuples.tuple_len_0_typical_eq
77instantiation86, 89, ,  ⊢  
  : , :
78instantiation87, 84, ,  ⊢  
  : , :
79instantiation87, 85, ,  ⊢  
  : , :
80instantiation86, 91  ⊢  
  : , :
81instantiation86, 93  ⊢  
  : , :
82axiom  ⊢  
 proveit.logic.equality.substitution
83instantiation87, 88, ,  ⊢  
  : , :
84instantiation92, 95, 96, 89, ,  ⊢  
  : , :
85instantiation90, 96, 95, 91, ,  ⊢  
  : , :
86conjecture  ⊢  
 proveit.core_expr_types.conditionals.satisfied_condition_reduction
87conjecture  ⊢  
 proveit.core_expr_types.conditionals.dissatisfied_condition_reduction
88instantiation92, 96, 95, 93, ,  ⊢  
  : , :
89instantiation94, 95, 96, 97, ,  ⊢  
  : , :
90conjecture  ⊢  
 proveit.numbers.ordering.not_less_eq_from_less
91assumption  ⊢  
92conjecture  ⊢  
 proveit.numbers.ordering.not_less_from_less_eq
93assumption  ⊢  
94conjecture  ⊢  
 proveit.numbers.ordering.relax_equal_to_less_eq
95assumption  ⊢  
96assumption  ⊢  
97instantiation98, 99  ⊢  
  : , :
98theorem  ⊢  
 proveit.logic.equality.equals_reversal
99assumption  ⊢