beta_sum_replace_balance

Proof neighborhood

Direct dependencies

Direct dependents

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v16 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

1. 0001induction k
2. 0002intro b
3. 0003intro c
4. 0004intro z
5. 0005intro d
6. 0006intro i
7. 0007intro x
8. 0008intro y
9. 0009intro p
10. 0010intro q
11. 0011intro hi
12. 0012exfalso
13. 0013cases hi
14. 0014have hsi : S i = 0
15. 0015specialize add_eq_zero_right x1
16. 0016specialize add_eq_zero_right (S i)
17. 0017apply add_eq_zero_right
18. 0018exact hi_witness
19. 0019specialize succ_ne_zero i
20. 0020apply succ_ne_zero
21. 0021exact hsi
22. 0022intro b
23. 0023intro c
24. 0024intro z
25. 0025intro d
26. 0026intro i
27. 0027intro x
28. 0028intro y
29. 0029intro p
30. 0030intro q
31. 0031intro hi
32. 0032intro hold_i
33. 0033intro hnew_i
34. 0034intro hpreserve
35. 0035intro hproduct_old
36. 0036intro hproduct_new
37. 0037have hisplit : i = k \/ exists h. h + S i = k
38. 0038specialize finite_lt_succ_eq_or_lt k
39. 0039specialize finite_lt_succ_eq_or_lt i
40. 0040apply finite_lt_succ_eq_or_lt
41. 0041exact hi
42. 0042have hold_decomp : exists a r. (((exists ff_h_balance_old_last. ff_h_balance_old_last + S (a) = S ((S (k)) * c)) /\ exists ff_q_balance_old_last. b = ff_q_balance_old_last * S ((S (k)) * c) + (a))) /\ ((exists ff_u_balance_old_prefix ff_v_balance_old_prefix. ((((exists ff_h_balance_old_prefix_start. ff_h_balance_old_prefix_start + S (0) = S ((S (0)) * ff_v_balance_old_prefix)) /\ exists ff_q_balance_old_prefix_start. ff_u_balance_old_prefix = ff_q_balance_old_prefix_start * S ((S (0)) * ff_v_balance_old_prefix) + (0))) /\ ((((exists ff_h_balance_old_prefix_terminal. ff_h_balance_old_prefix_terminal + S (r) = S ((S (k)) * ff_v_balance_old_prefix)) /\ exists ff_q_balance_old_prefix_terminal. ff_u_balance_old_prefix = ff_q_balance_old_prefix_terminal * S ((S (k)) * ff_v_balance_old_prefix) + (r))) /\ forall ff_i_balance_old_prefix. (exists ff_lt_balance_old_prefix_bound. ff_lt_balance_old_prefix_bound + S ff_i_balance_old_prefix = k) -> exists ff_a_balance_old_prefix ff_r_balance_old_prefix ff_s_balance_old_prefix. ((((exists ff_h_balance_old_prefix_summand. ff_h_balance_old_prefix_summand + S (ff_a_balance_old_prefix) = S ((S (ff_i_balance_old_prefix)) * c)) /\ exists ff_q_balance_old_prefix_summand. b = ff_q_balance_old_prefix_summand * S ((S (ff_i_balance_old_prefix)) * c) + (ff_a_balance_old_prefix))) /\ ((((exists ff_h_balance_old_prefix_partial. ff_h_balance_old_prefix_partial + S (ff_r_balance_old_prefix) = S ((S (ff_i_balance_old_prefix)) * ff_v_balance_old_prefix)) /\ exists ff_q_balance_old_prefix_partial. ff_u_balance_old_prefix = ff_q_balance_old_prefix_partial * S ((S (ff_i_balance_old_prefix)) * ff_v_balance_old_prefix) + (ff_r_balance_old_prefix))) /\ ((((exists ff_h_balance_old_prefix_successor. ff_h_balance_old_prefix_successor + S (ff_s_balance_old_prefix) = S ((S (S ff_i_balance_old_prefix)) * ff_v_balance_old_prefix)) /\ exists ff_q_balance_old_prefix_successor. ff_u_balance_old_prefix = ff_q_balance_old_prefix_successor * S ((S (S ff_i_balance_old_prefix)) * ff_v_balance_old_prefix) + (ff_s_balance_old_prefix))) /\ ff_s_balance_old_prefix = ff_r_balance_old_prefix + ff_a_balance_old_prefix)))))) /\ p = r + a)
43. 0043specialize beta_sum_succ_decompose b
44. 0044specialize beta_sum_succ_decompose c
45. 0045specialize beta_sum_succ_decompose k
46. 0046specialize beta_sum_succ_decompose p
47. 0047apply beta_sum_succ_decompose
48. 0048exact hproduct_old
49. 0049have hnew_decomp : exists a r. (((exists ff_h_balance_new_last. ff_h_balance_new_last + S (a) = S ((S (k)) * d)) /\ exists ff_q_balance_new_last. z = ff_q_balance_new_last * S ((S (k)) * d) + (a))) /\ ((exists ff_u_balance_new_prefix ff_v_balance_new_prefix. ((((exists ff_h_balance_new_prefix_start. ff_h_balance_new_prefix_start + S (0) = S ((S (0)) * ff_v_balance_new_prefix)) /\ exists ff_q_balance_new_prefix_start. ff_u_balance_new_prefix = ff_q_balance_new_prefix_start * S ((S (0)) * ff_v_balance_new_prefix) + (0))) /\ ((((exists ff_h_balance_new_prefix_terminal. ff_h_balance_new_prefix_terminal + S (r) = S ((S (k)) * ff_v_balance_new_prefix)) /\ exists ff_q_balance_new_prefix_terminal. ff_u_balance_new_prefix = ff_q_balance_new_prefix_terminal * S ((S (k)) * ff_v_balance_new_prefix) + (r))) /\ forall ff_i_balance_new_prefix. (exists ff_lt_balance_new_prefix_bound. ff_lt_balance_new_prefix_bound + S ff_i_balance_new_prefix = k) -> exists ff_a_balance_new_prefix ff_r_balance_new_prefix ff_s_balance_new_prefix. ((((exists ff_h_balance_new_prefix_summand. ff_h_balance_new_prefix_summand + S (ff_a_balance_new_prefix) = S ((S (ff_i_balance_new_prefix)) * d)) /\ exists ff_q_balance_new_prefix_summand. z = ff_q_balance_new_prefix_summand * S ((S (ff_i_balance_new_prefix)) * d) + (ff_a_balance_new_prefix))) /\ ((((exists ff_h_balance_new_prefix_partial. ff_h_balance_new_prefix_partial + S (ff_r_balance_new_prefix) = S ((S (ff_i_balance_new_prefix)) * ff_v_balance_new_prefix)) /\ exists ff_q_balance_new_prefix_partial. ff_u_balance_new_prefix = ff_q_balance_new_prefix_partial * S ((S (ff_i_balance_new_prefix)) * ff_v_balance_new_prefix) + (ff_r_balance_new_prefix))) /\ ((((exists ff_h_balance_new_prefix_successor. ff_h_balance_new_prefix_successor + S (ff_s_balance_new_prefix) = S ((S (S ff_i_balance_new_prefix)) * ff_v_balance_new_prefix)) /\ exists ff_q_balance_new_prefix_successor. ff_u_balance_new_prefix = ff_q_balance_new_prefix_successor * S ((S (S ff_i_balance_new_prefix)) * ff_v_balance_new_prefix) + (ff_s_balance_new_prefix))) /\ ff_s_balance_new_prefix = ff_r_balance_new_prefix + ff_a_balance_new_prefix)))))) /\ q = r + a)
50. 0050specialize beta_sum_succ_decompose z
51. 0051specialize beta_sum_succ_decompose d
52. 0052specialize beta_sum_succ_decompose k
53. 0053specialize beta_sum_succ_decompose q
54. 0054apply beta_sum_succ_decompose
55. 0055exact hproduct_new
56. 0056cases hold_decomp
57. 0057cases hold_decomp_witness
58. 0058cases hold_decomp_witness_witness
59. 0059cases hold_decomp_witness_witness_right
60. 0060cases hnew_decomp
61. 0061cases hnew_decomp_witness
62. 0062cases hnew_decomp_witness_witness
63. 0063cases hnew_decomp_witness_witness_right
64. 0064cases hisplit
65. 0065have hax : x1 = x
66. 0066specialize beta_at_unique b
67. 0067specialize beta_at_unique c
68. 0068specialize beta_at_unique k
69. 0069specialize beta_at_unique x1
70. 0070specialize beta_at_unique x
71. 0071apply beta_at_unique
72. 0072exact hold_decomp_witness_witness_left
73. 0073rewrite hisplit_left at hold_i
74. 0074rewrite hisplit_left at hold_i
75. 0075exact hold_i
76. 0076have hby : x3 = y
77. 0077specialize beta_at_unique z
78. 0078specialize beta_at_unique d
79. 0079specialize beta_at_unique k
80. 0080specialize beta_at_unique x3
81. 0081specialize beta_at_unique y
82. 0082apply beta_at_unique
83. 0083exact hnew_decomp_witness_witness_left
84. 0084rewrite hisplit_left at hnew_i
85. 0085rewrite hisplit_left at hnew_i
86. 0086exact hnew_i
87. 0087have hprefix_transport : exists ff_u_balance_transported_prefix ff_v_balance_transported_prefix. ((((exists ff_h_balance_transported_prefix_start. ff_h_balance_transported_prefix_start + S (0) = S ((S (0)) * ff_v_balance_transported_prefix)) /\ exists ff_q_balance_transported_prefix_start. ff_u_balance_transported_prefix = ff_q_balance_transported_prefix_start * S ((S (0)) * ff_v_balance_transported_prefix) + (0))) /\ ((((exists ff_h_balance_transported_prefix_terminal. ff_h_balance_transported_prefix_terminal + S (x2) = S ((S (k)) * ff_v_balance_transported_prefix)) /\ exists ff_q_balance_transported_prefix_terminal. ff_u_balance_transported_prefix = ff_q_balance_transported_prefix_terminal * S ((S (k)) * ff_v_balance_transported_prefix) + (x2))) /\ forall ff_i_balance_transported_prefix. (exists ff_lt_balance_transported_prefix_bound. ff_lt_balance_transported_prefix_bound + S ff_i_balance_transported_prefix = k) -> exists ff_a_balance_transported_prefix ff_r_balance_transported_prefix ff_s_balance_transported_prefix. ((((exists ff_h_balance_transported_prefix_summand. ff_h_balance_transported_prefix_summand + S (ff_a_balance_transported_prefix) = S ((S (ff_i_balance_transported_prefix)) * d)) /\ exists ff_q_balance_transported_prefix_summand. z = ff_q_balance_transported_prefix_summand * S ((S (ff_i_balance_transported_prefix)) * d) + (ff_a_balance_transported_prefix))) /\ ((((exists ff_h_balance_transported_prefix_partial. ff_h_balance_transported_prefix_partial + S (ff_r_balance_transported_prefix) = S ((S (ff_i_balance_transported_prefix)) * ff_v_balance_transported_prefix)) /\ exists ff_q_balance_transported_prefix_partial. ff_u_balance_transported_prefix = ff_q_balance_transported_prefix_partial * S ((S (ff_i_balance_transported_prefix)) * ff_v_balance_transported_prefix) + (ff_r_balance_transported_prefix))) /\ ((((exists ff_h_balance_transported_prefix_successor. ff_h_balance_transported_prefix_successor + S (ff_s_balance_transported_prefix) = S ((S (S ff_i_balance_transported_prefix)) * ff_v_balance_transported_prefix)) /\ exists ff_q_balance_transported_prefix_successor. ff_u_balance_transported_prefix = ff_q_balance_transported_prefix_successor * S ((S (S ff_i_balance_transported_prefix)) * ff_v_balance_transported_prefix) + (ff_s_balance_transported_prefix))) /\ ff_s_balance_transported_prefix = ff_r_balance_transported_prefix + ff_a_balance_transported_prefix)))))
88. 0088specialize beta_sum_transport_prefix b
89. 0089specialize beta_sum_transport_prefix c
90. 0090specialize beta_sum_transport_prefix z
91. 0091specialize beta_sum_transport_prefix d
92. 0092specialize beta_sum_transport_prefix k
93. 0093specialize beta_sum_transport_prefix x2
94. 0094apply beta_sum_transport_prefix
95. 0095exact hold_decomp_witness_witness_right_left
96. 0096intro j
97. 0097intro a
98. 0098intro hj
99. 0099intro hold
100. 0100specialize hpreserve j
101. 0101specialize hpreserve a
102. 0102apply hpreserve
103. 0103specialize le_succ (S j)
104. 0104specialize le_succ k
105. 0105apply le_succ
106. 0106exact hj
107. 0107intro hjk
108. 0108specialize lt_irrefl_expanded k
109. 0109apply lt_irrefl_expanded
110. 0110rewrite hjk at hj
111. 0111rewrite hisplit_left at hj
112. 0112exact hj
113. 0113exact hold
114. 0114cases hprefix_transport
115. 0115cases hprefix_transport_witness
116. 0116cases hnew_decomp_witness_witness_right_left
117. 0117cases hnew_decomp_witness_witness_right_left_witness
118. 0118rewrite hold_decomp_witness_witness_right_right
119. 0119rewrite hnew_decomp_witness_witness_right_right
120. 0120rewrite hax
121. 0121rewrite hby
122. 0122trans (x4 + x) + y
123. 0123simp [add_assoc, add_comm]
124. 0124congr
125. 0125congr
126. 0126symm
127. 0127specialize beta_sum_trace_functional z
128. 0128specialize beta_sum_trace_functional d
129. 0129specialize beta_sum_trace_functional k
130. 0130specialize beta_sum_trace_functional x2
131. 0131specialize beta_sum_trace_functional x5
132. 0132specialize beta_sum_trace_functional x6
133. 0133specialize beta_sum_trace_functional x4
134. 0134specialize beta_sum_trace_functional x7
135. 0135specialize beta_sum_trace_functional x8
136. 0136apply beta_sum_trace_functional
137. 0137exact hprefix_transport_witness_witness
138. 0138exact hnew_decomp_witness_witness_right_left_witness_witness
139. 0139refl
140. 0140refl
141. 0141have hki : ~(k = i)
142. 0142intro hki_eq
143. 0143specialize lt_irrefl_expanded k
144. 0144apply lt_irrefl_expanded
145. 0145rewrite <- hki_eq at hisplit_right
146. 0146exact hisplit_right
147. 0147have hlast_new : ((exists h. h + S x1 = S ((S k) * d)) /\ exists w. z = w * S ((S k) * d) + x1)
148. 0148specialize hpreserve k
149. 0149specialize hpreserve x1
150. 0150apply hpreserve
151. 0151specialize le_refl (S k)
152. 0152exact le_refl
153. 0153exact hki
154. 0154exact hold_decomp_witness_witness_left
155. 0155have hlast_eq : x3 = x1
156. 0156specialize beta_at_unique z
157. 0157specialize beta_at_unique d
158. 0158specialize beta_at_unique k
159. 0159specialize beta_at_unique x3
160. 0160specialize beta_at_unique x1
161. 0161apply beta_at_unique
162. 0162exact hnew_decomp_witness_witness_left
163. 0163exact hlast_new
164. 0164have hprefix_preserve : forall j a. (exists h. h + S j = k) -> ~(j = i) -> ((exists h. h + S a = S ((S j) * c)) /\ exists w. b = w * S ((S j) * c) + a) -> ((exists h. h + S a = S ((S j) * d)) /\ exists w. z = w * S ((S j) * d) + a)
165. 0165intro j
166. 0166intro a
167. 0167intro hj
168. 0168intro hji
169. 0169intro hold
170. 0170specialize hpreserve j
171. 0171specialize hpreserve a
172. 0172apply hpreserve
173. 0173specialize le_succ (S j)
174. 0174specialize le_succ k
175. 0175apply le_succ
176. 0176exact hj
177. 0177exact hji
178. 0178exact hold
179. 0179have hbalance : x4 + x = x2 + y
180. 0180specialize IH b
181. 0181specialize IH c
182. 0182specialize IH z
183. 0183specialize IH d
184. 0184specialize IH i
185. 0185specialize IH x
186. 0186specialize IH y
187. 0187specialize IH x2
188. 0188specialize IH x4
189. 0189apply IH
190. 0190exact hisplit_right
191. 0191exact hold_i
192. 0192exact hnew_i
193. 0193exact hprefix_preserve
194. 0194exact hold_decomp_witness_witness_right_left
195. 0195exact hnew_decomp_witness_witness_right_left
196. 0196rewrite hold_decomp_witness_witness_right_right
197. 0197rewrite hnew_decomp_witness_witness_right_right
198. 0198rewrite hlast_eq
199. 0199trans (x4 + x) + x1
200. 0200simp [add_assoc, add_comm]
201. 0201rewrite hbalance
202. 0202simp [add_assoc, add_comm]