logo

Proof of proveit.numbers.ordering.min_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, min_def_bin)
In [2]:
%proving min_bin_args_commute
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
min_bin_args_commute:
(see dependencies)
In [3]:
defaults.assumptions = min_bin_args_commute.conditions
defaults.assumptions:
In [4]:
min_def_bin
 ⊢  
In [5]:
min_x_y_def = min_def_bin.instantiate({x: x, y: y})
min_x_y_def: ,  ⊢  
In [6]:
min_y_x_def = min_def_bin.instantiate({x: y, y: x})
min_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]:
min_x_y_def.inner_expr().rhs.simplify(assumptions=case_1_assumptions)
, ,  ⊢  
In [11]:
min_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:

For Case 2, we can quickly get the desired output for Min(y, x):

In [13]:
case_2_non_implication = min_y_x_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()
,  ⊢  

For Min(x, y), Case 2 needs to be broken up into two pieces.

In [15]:
less_eq_def
 ⊢  
In [16]:
y_le_x_as_disjunction = less_eq_def.instantiate({x: y, y: x})
y_le_x_as_disjunction:  ⊢  
In [17]:
y_le_x_as_disjunction.derive_right_via_equality(assumptions=case_2_assumptions)
 ⊢  
In [18]:
case_2_a_assumptions = defaults.assumptions + (y_le_x_as_disjunction.rhs.operands[0],)
case_2_a_assumptions:
In [19]:
min_x_y_def.inner_expr().rhs.simplify(assumptions=case_2_a_assumptions)
, ,  ⊢  
In [20]:
case_2_b_assumptions = defaults.assumptions + (y_le_x_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]:
min_x_y_when_y_eq_x = min_x_y_def.inner_expr().rhs.simplify(assumptions=case_2_b_assumptions)
min_x_y_when_y_eq_x: , ,  ⊢  
In [23]:
case_2_b_non_implication = min_x_y_when_y_eq_x.inner_expr().rhs.substitute(y,
        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]:
y_le_x_as_disjunction
 ⊢  
In [25]:
y_le_x_as_disjunction.rhs.derive_via_singular_dilemma(
        min_bin_args_commute.instance_expr,
        assumptions=defaults.assumptions+(y_le_x_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(
    min_bin_args_commute.instance_expr)
,  ⊢   
min_bin_args_commute may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".
In [27]:
%qed

proveit.numbers.ordering.min_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,  ⊢  
  :
7instantiation54, 10, 44, ,  ⊢  
  : , : , :
8instantiation11, 12, 13, 27, 14, 15, ,  ⊢  
  : , : , :
9instantiation16, 95, 96,  ⊢  
  : , :
10instantiation54, 17, 18, ,  ⊢  
  : , : , :
11theorem  ⊢  
 proveit.logic.booleans.disjunction.singular_constructive_dilemma
12instantiation19, 21  ⊢  
  : , :
13instantiation20, 21  ⊢  
  : , :
14deduction22, ,  ⊢  
15deduction23, ,  ⊢  
16conjecture  ⊢  
 proveit.numbers.ordering.less_or_greater_eq
17instantiation98, 24, ,  ⊢  
  : , :
18instantiation71, 25, 64, ,  ⊢  
  : , : , :
19axiom  ⊢  
 proveit.logic.booleans.disjunction.left_in_bool
20axiom  ⊢  
 proveit.logic.booleans.disjunction.right_in_bool
21instantiation26, 27  ⊢  
  :
22instantiation54, 28, 30, , ,  ⊢  
  : , : , :
23instantiation54, 29, 30, , ,  ⊢  
  : , : , :
24instantiation43, 30, 31, ,  ⊢  
  : , : , :
25instantiation71, 32, 33, ,  ⊢  
  : , : , :
26conjecture  ⊢  
 proveit.logic.booleans.in_bool_if_true
27instantiation34, 91, 35  ⊢  
  : , :
28instantiation54, 36, 47, , ,  ⊢  
  : , : , :
29instantiation54, 37, 44, , ,  ⊢  
  : , : , :
30instantiation51, 96, 95,  ⊢  
  : , :
31instantiation71, 38, 39, ,  ⊢  
  : , : , :
32instantiation83, 40  ⊢  
  : , : , :
33instantiation83, 41, ,  ⊢  
  : , : , :
34theorem  ⊢  
 proveit.logic.equality.rhs_via_equality
35instantiation42  ⊢  
  : , :
36instantiation43, 44, 45, ,  ⊢  
  : , : , :
37instantiation54, 46, 47, , ,  ⊢  
  : , : , :
38instantiation71, 48, 49, ,  ⊢  
  : , : , :
39instantiation74, 76, 75, 77  ⊢  
  : , : , : , : , :
40instantiation88, 60  ⊢  
  : , :
41instantiation89, 50, ,  ⊢  
  : , :
42axiom  ⊢  
 proveit.numbers.ordering.less_eq_def
43theorem  ⊢  
 proveit.logic.equality.sub_right_side_into
44instantiation51, 95, 96,  ⊢  
  : , :
45instantiation71, 52, 53, ,  ⊢  
  : , : , :
46instantiation54, 97, 55, ,  ⊢  
  : , : , :
47instantiation71, 56, 57, ,  ⊢  
  : , : , :
48instantiation83, 58, ,  ⊢  
  : , : , :
49instantiation83, 59  ⊢  
  : , : , :
50instantiation92, 95, 96, 60, ,  ⊢  
  : , :
51axiom  ⊢  
 proveit.numbers.ordering.min_def_bin
52instantiation71, 61, 62, ,  ⊢  
  : , : , :
53instantiation74, 76, 75, 77  ⊢  
  : , : , : , : , :
54theorem  ⊢  
 proveit.logic.equality.sub_left_side_into
55instantiation71, 63, 64, ,  ⊢  
  : , : , :
56instantiation71, 65, 66, ,  ⊢  
  : , : , :
57instantiation74, 75, 76, 77  ⊢  
  : , : , : , : , :
58instantiation89, 67, ,  ⊢  
  : , :
59instantiation88, 80  ⊢  
  : , :
60instantiation68, 80  ⊢  
  : , :
61instantiation83, 69, ,  ⊢  
  : , : , :
62instantiation83, 70  ⊢  
  : , : , :
63instantiation71, 72, 73, ,  ⊢  
  : , : , :
64instantiation74, 75, 76, 77  ⊢  
  : , : , : , : , :
65instantiation83, 78  ⊢  
  : , : , :
66instantiation83, 79, ,  ⊢  
  : , : , :
67instantiation86, 95, 96, 80, ,  ⊢  
  : , :
68conjecture  ⊢  
 proveit.numbers.ordering.relax_less
69instantiation89, 81, ,  ⊢  
  : , :
70instantiation88, 87  ⊢  
  : , :
71axiom  ⊢  
 proveit.logic.equality.equals_transitivity
72instantiation83, 82, ,  ⊢  
  : , : , :
73instantiation83, 84, ,  ⊢  
  : , : , :
74axiom  ⊢  
 proveit.core_expr_types.conditionals.true_case_reduction
75axiom  ⊢  
 proveit.numbers.number_sets.natural_numbers.zero_in_nats
76theorem  ⊢  
 proveit.numbers.numerals.decimals.nat1
77conjecture  ⊢  
 proveit.core_expr_types.tuples.tuple_len_0_typical_eq
78instantiation88, 91  ⊢  
  : , :
79instantiation89, 85, ,  ⊢  
  : , :
80assumption  ⊢  
81instantiation86, 96, 95, 87, ,  ⊢  
  : , :
82instantiation88, 93, ,  ⊢  
  : , :
83axiom  ⊢  
 proveit.logic.equality.substitution
84instantiation89, 90, ,  ⊢  
  : , :
85instantiation92, 96, 95, 91, ,  ⊢  
  : , :
86conjecture  ⊢  
 proveit.numbers.ordering.not_less_eq_from_less
87assumption  ⊢  
88conjecture  ⊢  
 proveit.core_expr_types.conditionals.satisfied_condition_reduction
89conjecture  ⊢  
 proveit.core_expr_types.conditionals.dissatisfied_condition_reduction
90instantiation92, 95, 96, 93, ,  ⊢  
  : , :
91assumption  ⊢  
92conjecture  ⊢  
 proveit.numbers.ordering.not_less_from_less_eq
93instantiation94, 95, 96, 97, ,  ⊢  
  : , :
94conjecture  ⊢  
 proveit.numbers.ordering.relax_equal_to_less_eq
95assumption  ⊢  
96assumption  ⊢  
97instantiation98, 99  ⊢  
  : , :
98theorem  ⊢  
 proveit.logic.equality.equals_reversal
99assumption  ⊢