beta_prefix_sum_trace_exists

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 Stable checked-use theorem is independently kernel-checked when replayed.

1. 0001intro b
2. 0002intro c
3. 0003induction l
4. 0004exists 0
5. 0005exists 1
6. 0006split
7. 0007specialize beta_at_self_of_bound 1
8. 0008specialize beta_at_self_of_bound 0
9. 0009specialize beta_at_self_of_bound 0
10. 0010apply beta_at_self_of_bound
11. 0011specialize one_mul 1
12. 0012rewrite one_mul
13. 0013specialize succ_le_succ 0
14. 0014specialize succ_le_succ (S 0)
15. 0015apply succ_le_succ
16. 0016specialize zero_le (S 0)
17. 0017exact zero_le
18. 0018intro i
19. 0019intro hi
20. 0020exfalso
21. 0021cases hi
22. 0022have hsi0 : S i = 0
23. 0023specialize add_eq_zero_right x
24. 0024specialize add_eq_zero_right (S i)
25. 0025apply add_eq_zero_right
26. 0026exact hi_witness
27. 0027specialize succ_ne_zero i
28. 0028apply succ_ne_zero
29. 0029exact hsi0
30. 0030have htrace : exists fs_u_induction fs_v_induction. ((((exists fs_h_induction_start. fs_h_induction_start + S (0) = S ((S (0)) * fs_v_induction)) /\ exists fs_q_induction_start. fs_u_induction = fs_q_induction_start * S ((S (0)) * fs_v_induction) + (0))) /\ forall fs_i_induction_steps. (exists fs_lt_induction_steps_bound. fs_lt_induction_steps_bound + S fs_i_induction_steps = l) -> exists fs_a_induction_steps fs_r_induction_steps fs_s_induction_steps. ((((exists fs_h_induction_steps_summand. fs_h_induction_steps_summand + S (fs_a_induction_steps) = S ((S (fs_i_induction_steps)) * c)) /\ exists fs_q_induction_steps_summand. b = fs_q_induction_steps_summand * S ((S (fs_i_induction_steps)) * c) + (fs_a_induction_steps))) /\ ((((exists fs_h_induction_steps_partial. fs_h_induction_steps_partial + S (fs_r_induction_steps) = S ((S (fs_i_induction_steps)) * fs_v_induction)) /\ exists fs_q_induction_steps_partial. fs_u_induction = fs_q_induction_steps_partial * S ((S (fs_i_induction_steps)) * fs_v_induction) + (fs_r_induction_steps))) /\ ((((exists fs_h_induction_steps_successor. fs_h_induction_steps_successor + S (fs_s_induction_steps) = S ((S (S fs_i_induction_steps)) * fs_v_induction)) /\ exists fs_q_induction_steps_successor. fs_u_induction = fs_q_induction_steps_successor * S ((S (S fs_i_induction_steps)) * fs_v_induction) + (fs_s_induction_steps))) /\ fs_s_induction_steps = fs_r_induction_steps + fs_a_induction_steps))))
31. 0031apply IH
32. 0032cases htrace
33. 0033cases htrace_witness
34. 0034cases htrace_witness_witness
35. 0035have hfactor : exists p. ((exists fs_h_trace_factor. fs_h_trace_factor + S (p) = S ((S (l)) * c)) /\ exists fs_q_trace_factor. b = fs_q_trace_factor * S ((S (l)) * c) + (p))
36. 0036specialize beta_at_exists b
37. 0037specialize beta_at_exists c
38. 0038specialize beta_at_exists l
39. 0039exact beta_at_exists
40. 0040cases hfactor
41. 0041have hlast : exists r. ((exists fs_h_trace_last. fs_h_trace_last + S (r) = S ((S (l)) * x1)) /\ exists fs_q_trace_last. x = fs_q_trace_last * S ((S (l)) * x1) + (r))
42. 0042specialize beta_at_exists x
43. 0043specialize beta_at_exists x1
44. 0044specialize beta_at_exists l
45. 0045exact beta_at_exists
46. 0046cases hlast
47. 0047have hext : exists z v. ((((exists fs_h_trace_extension. fs_h_trace_extension + S (x3 + x2) = S ((S (S l)) * v)) /\ exists fs_q_trace_extension. z = fs_q_trace_extension * S ((S (S l)) * v) + (x3 + x2))) /\ forall i a. (exists h. h + S i = S l) -> (((exists fs_h_trace_old. fs_h_trace_old + S (a) = S ((S (i)) * x1)) /\ exists fs_q_trace_old. x = fs_q_trace_old * S ((S (i)) * x1) + (a))) -> (((exists fs_h_trace_new. fs_h_trace_new + S (a) = S ((S (i)) * v)) /\ exists fs_q_trace_new. z = fs_q_trace_new * S ((S (i)) * v) + (a))))
48. 0048specialize beta_prefix_extend (S l)
49. 0049specialize beta_prefix_extend x
50. 0050specialize beta_prefix_extend x1
51. 0051specialize beta_prefix_extend (x3 + x2)
52. 0052exact beta_prefix_extend
53. 0053cases hext
54. 0054cases hext_witness
55. 0055cases hext_witness_witness
56. 0056exists x4
57. 0057exists x5
58. 0058split
59. 0059specialize hext_witness_witness_right 0
60. 0060specialize hext_witness_witness_right 0
61. 0061apply hext_witness_witness_right
62. 0062have h0 : exists h. h + S 0 = S l
63. 0063have hzero : exists h. h + 0 = l
64. 0064specialize zero_le l
65. 0065exact zero_le
66. 0066specialize succ_le_succ 0
67. 0067specialize succ_le_succ l
68. 0068apply succ_le_succ
69. 0069exact hzero
70. 0070exact h0
71. 0071exact htrace_witness_witness_left
72. 0072intro i
73. 0073intro hi
74. 0074have hil : exists h. h + i = l
75. 0075specialize le_of_succ_le_succ i
76. 0076specialize le_of_succ_le_succ l
77. 0077apply le_of_succ_le_succ
78. 0078exact hi
79. 0079have hsplit : i = l \/ exists h. h + S i = l
80. 0080specialize le_eq_or_lt i
81. 0081specialize le_eq_or_lt l
82. 0082apply le_eq_or_lt
83. 0083exact hil
84. 0084cases hsplit
85. 0085exists x2
86. 0086exists x3
87. 0087exists x3 + x2
88. 0088split
89. 0089rewrite hsplit_left
90. 0090rewrite hsplit_left
91. 0091exact hfactor_witness
92. 0092split
93. 0093rewrite hsplit_left
94. 0094rewrite hsplit_left
95. 0095specialize hext_witness_witness_right l
96. 0096specialize hext_witness_witness_right x3
97. 0097apply hext_witness_witness_right
98. 0098specialize le_refl (S l)
99. 0099exact le_refl
100. 0100exact hlast_witness
101. 0101split
102. 0102rewrite hsplit_left
103. 0103rewrite hsplit_left
104. 0104exact hext_witness_witness_left
105. 0105refl
106. 0106have hold : exists p r s. ((((exists fs_h_trace_hold_factor. fs_h_trace_hold_factor + S (p) = S ((S (i)) * c)) /\ exists fs_q_trace_hold_factor. b = fs_q_trace_hold_factor * S ((S (i)) * c) + (p))) /\ ((((exists fs_h_trace_hold_partial. fs_h_trace_hold_partial + S (r) = S ((S (i)) * x1)) /\ exists fs_q_trace_hold_partial. x = fs_q_trace_hold_partial * S ((S (i)) * x1) + (r))) /\ ((((exists fs_h_trace_hold_successor. fs_h_trace_hold_successor + S (s) = S ((S (S i)) * x1)) /\ exists fs_q_trace_hold_successor. x = fs_q_trace_hold_successor * S ((S (S i)) * x1) + (s))) /\ s = r + p)))
107. 0107specialize htrace_witness_witness_right i
108. 0108apply htrace_witness_witness_right
109. 0109exact hsplit_right
110. 0110cases hold
111. 0111cases hold_witness
112. 0112cases hold_witness_witness
113. 0113cases hold_witness_witness_witness
114. 0114cases hold_witness_witness_witness_right
115. 0115cases hold_witness_witness_witness_right_right
116. 0116exists x6
117. 0117exists x7
118. 0118exists x8
119. 0119split
120. 0120exact hold_witness_witness_witness_left
121. 0121split
122. 0122specialize hext_witness_witness_right i
123. 0123specialize hext_witness_witness_right x7
124. 0124apply hext_witness_witness_right
125. 0125exact hi
126. 0126exact hold_witness_witness_witness_right_left
127. 0127split
128. 0128specialize hext_witness_witness_right (S i)
129. 0129specialize hext_witness_witness_right x8
130. 0130apply hext_witness_witness_right
131. 0131specialize succ_le_succ (S i)
132. 0132specialize succ_le_succ l
133. 0133apply succ_le_succ
134. 0134exact hsplit_right
135. 0135exact hold_witness_witness_witness_right_right_left
136. 0136exact hold_witness_witness_witness_right_right_right