logo
In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import a, b, e, l, x, y, defaults
from proveit.logic import Iff, InSet, Or, SubsetEq, Union
from proveit.numbers import zero, Add, subtract, greater_eq, Less, Neg, NaturalPos
from proveit.numbers.ordering import less_or_greater_eq
from proveit.physics.quantum.QPE import (
    _full_domain, _modabs_in_full_domain_simp, _neg_domain, _pos_domain)
from proveit.physics.quantum.QPE import (
    _two_pow_t, _two_pow_t__minus_one, _t_in_natural_pos, _two_pow_t_minus_one_is_nat_pos)
In [2]:
%proving _fail_sum_prob_conds_equiv_lemma
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
_fail_sum_prob_conds_equiv_lemma:
(see dependencies)
In [3]:
defaults.assumptions = _fail_sum_prob_conds_equiv_lemma.all_conditions()
defaults.assumptions:

We want to derive the logical equivalence (if and only if) between the following conditions:

In [4]:
lhs_condition = _fail_sum_prob_conds_equiv_lemma.instance_expr.instance_expr.lhs
lhs_condition:
In [5]:
rhs_condition = _fail_sum_prob_conds_equiv_lemma.instance_expr.instance_expr.rhs
rhs_condition:

(1) $\text{lhs} \Rightarrow \text{rhs}$. This direction is straightforward using the fact that $\{-2^{t-1}+1~\ldotp \ldotp~-(e+1)\} \cup \{e + 1~\ldotp \ldotp~2^{t-1}\} \subseteq \{-2^{t-1}+1~\ldotp \ldotp~2^{t-2}\}$.

In [6]:
SubsetEq(Union(_neg_domain, _pos_domain), _full_domain).prove()
In [7]:
rhs_condition.prove(assumptions=defaults.assumptions + (lhs_condition,))

(2) $\text{lhs} \Leftarrow \text{rhs}$.

Going from rhs to lhs requires us to consider the non-negative/negative cases separately.

2(a): $\text{lhs} \Leftarrow \text{rhs}$. The NON-NEGATIVE case.

In [8]:
# update our default assumptions
defaults.assumptions = _fail_sum_prob_conds_equiv_lemma.all_conditions() + [rhs_condition, greater_eq(l, zero)]
defaults.assumptions:
In [9]:
_modabs_in_full_domain_simp
In [10]:
_modabs_in_full_domain_simp.instantiate().sub_right_side_into(rhs_condition.operands[1])
In [11]:
InSet(subtract(l, e), NaturalPos).prove()
, ,  ⊢  
In [12]:
lhs_condition.prove()
, ,  ⊢  

2(b): $\text{lhs} \Leftarrow \text{rhs}$. The NEGATIVE case.

In [13]:
# update our default assumptions
defaults.assumptions = _fail_sum_prob_conds_equiv_lemma.all_conditions() + [rhs_condition, Less(l, zero)]
defaults.assumptions:
In [14]:
_modabs_in_full_domain_simp.instantiate().sub_right_side_into(rhs_condition.operands[1])
In [15]:
InSet(Neg(Add(e, l)), NaturalPos).prove()
, ,  ⊢  
In [16]:
lhs_condition.prove()
, ,  ⊢  

Since either $l \geq 0$ or $l < 0$ but we can derive lhs_condition either way, then lhs_condition must be true (under these assumptions).

In [17]:
# update our default assumptions (removing the specifics about ell being negative or non-negative)
defaults.assumptions = _fail_sum_prob_conds_equiv_lemma.all_conditions() + [rhs_condition]
defaults.assumptions:
In [18]:
less_or_greater_eq
In [19]:
less_or_greater_eq.instantiate({x:l, y:zero})
In [20]:
Or(Less(l, zero), greater_eq(l, zero)).derive_via_dilemma(lhs_condition)
_fail_sum_prob_conds_equiv_lemma may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".
In [21]:
%qed
proveit.physics.quantum.QPE._fail_sum_prob_conds_equiv_lemma has been proven.
Out[21]:
 step typerequirementsstatement
0generalization1  ⊢  
1instantiation2, 3, 4  ⊢  
  : , :
2theorem  ⊢  
 proveit.logic.booleans.implication.iff_intro
3deduction5  ⊢  
4deduction6  ⊢  
5instantiation85, 7, 8,  ⊢  
  : , :
6instantiation9, 10, 11, 26, 12, 13,  ⊢  
  : , : , :
7instantiation365, 14, 15,  ⊢  
  : , : , :
8instantiation283, 24  ⊢  
  : , :
9theorem  ⊢  
 proveit.logic.booleans.disjunction.singular_constructive_dilemma
10instantiation16, 18  ⊢  
  : , :
11instantiation17, 18  ⊢  
  : , :
12deduction19,  ⊢  
13deduction20,  ⊢  
14instantiation21, 394, 35, 22, 23  ⊢  
  : , : , :
15instantiation378, 24  ⊢  
  : , :
16axiom  ⊢  
 proveit.logic.booleans.disjunction.left_in_bool
17axiom  ⊢  
 proveit.logic.booleans.disjunction.right_in_bool
18instantiation25, 26  ⊢  
  :
19instantiation85, 27, 260, ,  ⊢  
  : , :
20instantiation85, 28, 260, ,  ⊢  
  : , :
21conjecture  ⊢  
 proveit.logic.sets.unification.union_inclusion
22instantiation30, 377, 83, 404, 29  ⊢  
  : , : , : , :
23instantiation30, 377, 113, 404, 31  ⊢  
  : , : , : , :
24assumption  ⊢  
25conjecture  ⊢  
 proveit.logic.booleans.in_bool_if_true
26instantiation32, 328, 132  ⊢  
  : , :
27instantiation34, 394, 35, 33, ,  ⊢  
  : , : , :
28instantiation34, 394, 35, 36, ,  ⊢  
  : , : , :
29instantiation40, 319, 37, 38, 52, 39  ⊢  
  : , :
30conjecture  ⊢  
 proveit.numbers.number_sets.integers.interval_subset_eq
31instantiation40, 319, 41, 42, 43, 44  ⊢  
  : , :
32conjecture  ⊢  
 proveit.numbers.ordering.less_or_greater_eq
33instantiation110, 45, 46, ,  ⊢  
  : , :
34conjecture  ⊢  
 proveit.logic.sets.unification.membership_folding
35instantiation323  ⊢  
  : , :
36instantiation114, 47, 48, ,  ⊢  
  : , :
37instantiation335  ⊢  
  : , : , :
38instantiation57, 154, 49  ⊢  
  : , :
39instantiation325, 50  ⊢  
  : , :
40conjecture  ⊢  
 proveit.logic.booleans.conjunction.and_if_all
41instantiation335  ⊢  
  : , : , :
42instantiation51, 52, 53  ⊢  
  : , : , :
43instantiation131, 384, 351, 54, 55, 56*  ⊢  
  : , : , :
44instantiation57, 151, 58  ⊢  
  : , :
45instantiation63, 377, 83, 352, 59, ,  ⊢  
  : , : , :
46instantiation61, 60, ,  ⊢  
  : , :
47instantiation61, 62, ,  ⊢  
  : , :
48instantiation63, 113, 404, 352, 64, ,  ⊢  
  : , : , :
49instantiation303  ⊢  
  :
50instantiation149, 156, 65  ⊢  
  : , : , :
51conjecture  ⊢  
 proveit.numbers.ordering.transitivity_less_eq_less_eq
52instantiation131, 66, 351, 75, 76, 67*, 68*  ⊢  
  : , : , :
53instantiation131, 172, 69, 70, 71, 72*, 73*  ⊢  
  : , : , :
54instantiation327, 75, 384  ⊢  
  : , :
55instantiation74, 351, 75, 384, 76, 77  ⊢  
  : , : , :
56instantiation314, 78, 277, 79  ⊢  
  : , : , : , :
57conjecture  ⊢  
 proveit.numbers.ordering.relax_equal_to_less_eq
58instantiation303  ⊢  
  :
59instantiation85, 155, 80, ,  ⊢  
  : , :
60instantiation82, 113, 404, 352, 81, ,  ⊢  
  : , : , :
61theorem  ⊢  
 proveit.logic.sets.membership.unfold_not_in_set
62instantiation82, 377, 83, 352, 84, ,  ⊢  
  : , : , :
63conjecture  ⊢  
 proveit.numbers.number_sets.integers.in_interval
64instantiation85, 86, 152, ,  ⊢  
  : , :
65instantiation187, 409  ⊢  
  :
66instantiation87, 319, 88, 89, 384, 206  ⊢  
  : , :
67instantiation314, 90, 91, 92  ⊢  
  : , : , : , :
68instantiation331, 93  ⊢  
  : , :
69instantiation229, 397, 132  ⊢  
  : , :
70instantiation327, 207, 397  ⊢  
  : , :
71instantiation94, 95, 96, 411, 97, 98  ⊢  
  : , : , :
72instantiation331, 99  ⊢  
  : , :
73instantiation314, 100, 101, 102  ⊢  
  : , : , : , :
74conjecture  ⊢  
 proveit.numbers.ordering.less_eq_add_right
75instantiation412, 401, 103  ⊢  
  : , : , :
76instantiation188, 400, 399, 391  ⊢  
  : , : , :
77instantiation166, 406  ⊢  
  :
78instantiation272, 104, 105  ⊢  
  : , : , :
79instantiation331, 297  ⊢  
  : , :
80instantiation131, 309, 384, 106, 107, 108*, 109*, ,  ⊢  
  : , : , :
81instantiation110, 111, 112, ,  ⊢  
  : , :
82conjecture  ⊢  
 proveit.numbers.number_sets.integers.int_not_in_interval
83instantiation410, 113  ⊢  
  :
84instantiation114, 115, 116, ,  ⊢  
  : , :
85theorem  ⊢  
 proveit.logic.booleans.conjunction.and_if_both
86instantiation131, 351, 384, 117, 118, 119*, 120*, ,  ⊢  
  : , : , :
87conjecture  ⊢  
 proveit.numbers.addition.add_real_closure
88instantiation335  ⊢  
  : , : , :
89instantiation412, 401, 121  ⊢  
  : , : , :
90instantiation272, 122, 123  ⊢  
  : , : , :
91instantiation303  ⊢  
  :
92instantiation331, 124  ⊢  
  : , :
93instantiation314, 184, 125, 126  ⊢  
  : , : , : , :
94conjecture  ⊢  
 proveit.numbers.ordering.less_add_right_weak_int
95instantiation412, 413, 127  ⊢  
  : , : , :
96instantiation412, 413, 128  ⊢  
  : , : , :
97instantiation129, 397, 132, 351, 294, 130  ⊢  
  : , : , :
98instantiation131, 344, 132, 203, 133, 134*, 135*  ⊢  
  : , : , :
99instantiation314, 184, 185, 136  ⊢  
  : , : , : , :
100instantiation299, 300, 414, 406, 302, 138, 175, 387, 137  ⊢  
  : , : , : , : , : , :
101instantiation299, 414, 300, 138, 254, 302, 175, 387, 322, 342  ⊢  
  : , : , : , : , : , :
102instantiation314, 139, 140, 141  ⊢  
  : , : , : , :
103instantiation412, 407, 399  ⊢  
  : , : , :
104instantiation333, 142  ⊢  
  : , : , :
105instantiation272, 143, 144  ⊢  
  : , : , :
106instantiation365, 366, 145, ,  ⊢  
  : , : , :
107instantiation157, 145, ,  ⊢  
  :
108instantiation272, 146, 147  ⊢  
  : , : , :
109instantiation331, 148,  ⊢  
  : , :
110theorem  ⊢  
 proveit.logic.booleans.disjunction.or_if_only_left
111instantiation149, 326, 150,  ⊢  
  : , : , :
112instantiation153, 328, 151, 152  ⊢  
  : , :
113instantiation403, 376, 400  ⊢  
  : , :
114theorem  ⊢  
 proveit.logic.booleans.disjunction.or_if_only_right
115instantiation153, 154, 328, 155  ⊢  
  : , :
116instantiation311, 156, 296,  ⊢  
  : , : , :
117instantiation327, 328, 206,  ⊢  
  : , :
118instantiation157, 158, ,  ⊢  
  :
119instantiation340, 370, 337  ⊢  
  : , :
120instantiation272, 159, 160,  ⊢  
  : , : , :
121instantiation412, 407, 392  ⊢  
  : , : , :
122instantiation333, 244  ⊢  
  : , : , :
123instantiation272, 161, 162  ⊢  
  : , : , :
124instantiation333, 271  ⊢  
  : , : , :
125instantiation340, 322, 342  ⊢  
  : , :
126instantiation331, 163  ⊢  
  : , :
127instantiation164, 414, 300  ⊢  
  : , :
128instantiation164, 414, 165  ⊢  
  : , :
129conjecture  ⊢  
 proveit.numbers.multiplication.strong_bound_via_right_factor_bound
130instantiation187, 394  ⊢  
  :
131conjecture  ⊢  
 proveit.numbers.addition.weak_bound_via_left_term_bound
132conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.zero_is_real
133instantiation166, 319  ⊢  
  :
134instantiation278, 167, 168  ⊢  
  : , : , :
135instantiation282, 387, 370, 169, 170  ⊢  
  : , : , :
136instantiation331, 171  ⊢  
  : , :
137instantiation412, 396, 172  ⊢  
  : , : , :
138instantiation323  ⊢  
  : , :
139instantiation173, 406, 175, 387, 322, 342  ⊢  
  : , : , : , : , : , : , :
140instantiation247, 300, 414, 302, 174, 257, 175, 322, 387, 342, 176*  ⊢  
  : , : , : , : , : , :
141instantiation247, 406, 414, 300, 257, 302, 337, 387, 342, 258*  ⊢  
  : , : , : , : , : , :
142instantiation272, 177, 178  ⊢  
  : , : , :
143instantiation299, 300, 414, 406, 302, 179, 336, 342, 370  ⊢  
  : , : , : , : , : , :
144instantiation195, 370, 336, 183  ⊢  
  : , : , :
145instantiation180, 181, ,  ⊢  
  :
146instantiation299, 406, 414, 300, 289, 302, 370, 292, 342  ⊢  
  : , : , : , : , : , :
147instantiation182, 370, 292, 183  ⊢  
  : , : , :
148instantiation314, 184, 185, 186,  ⊢  
  : , : , : , :
149axiom  ⊢  
 proveit.numbers.ordering.transitivity_less_less
150instantiation187, 217  ⊢  
  :
151instantiation365, 366, 409  ⊢  
  : , : , :
152instantiation188, 377, 404, 364  ⊢  
  : ,