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