prime_mul_index_map_exists_up_to

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 l
2. 0002intro n
3. 0003intro p
4. 0004intro a
5. 0005intro hln
6. 0006intro hpn
7. 0007intro hp
8. 0008intro hnotdiv
9. 0009exists 0
10. 0010exists 0
11. 0011intro i
12. 0012intro hi
13. 0013exfalso
14. 0014cases hi
15. 0015have hsi : S i = 0
16. 0016specialize add_eq_zero_right x
17. 0017specialize add_eq_zero_right (S i)
18. 0018apply add_eq_zero_right
19. 0019exact hi_witness
20. 0020specialize succ_ne_zero i
21. 0021apply succ_ne_zero
22. 0022exact hsi
23. 0023intro n
24. 0024intro p
25. 0025intro a
26. 0026intro hln
27. 0027intro hpn
28. 0028intro hp
29. 0029intro hnotdiv
30. 0030have hln_prev : exists h. h + l = n
31. 0031specialize lt_to_le l
32. 0032specialize lt_to_le n
33. 0033apply lt_to_le
34. 0034exact hln
35. 0035have hprev : exists r s. (forall frm_index_previous. (exists frm_gap_previous_index_bound. frm_gap_previous_index_bound + S frm_index_previous = l) -> (exists frm_residue_previous_result. (exists frm_gap_previous_result_residue_bound. frm_gap_previous_result_residue_bound + S frm_residue_previous_result = n) /\ ((((exists ff_h_frm_previous_result_decoded. ff_h_frm_previous_result_decoded + S (frm_residue_previous_result) = S ((S (frm_index_previous)) * s)) /\ exists ff_q_frm_previous_result_decoded. r = ff_q_frm_previous_result_decoded * S ((S (frm_index_previous)) * s) + (frm_residue_previous_result))) /\ (exists frm_mod_left_previous_result_congruence frm_mod_right_previous_result_congruence. a * S frm_index_previous + p * frm_mod_left_previous_result_congruence = S frm_residue_previous_result + p * frm_mod_right_previous_result_congruence))))
36. 0036specialize IH n
37. 0037specialize IH p
38. 0038specialize IH a
39. 0039apply IH
40. 0040exact hln_prev
41. 0041exact hpn
42. 0042exact hp
43. 0043exact hnotdiv
44. 0044cases hprev
45. 0045cases hprev_witness
46. 0046have hslp : exists h. h + S (S l) = p
47. 0047rewrite hpn
48. 0048specialize succ_le_succ (S l)
49. 0049specialize succ_le_succ n
50. 0050apply succ_le_succ
51. 0051exact hln
52. 0052have hp0 : ~(p = 0)
53. 0053intro hpzero
54. 0054specialize prime_nonzero p
55. 0055apply prime_nonzero
56. 0056exact hp
57. 0057exact hpzero
58. 0058have hdiv : exists q rem. a * S l = p * q + rem /\ exists h. h + S rem = p
59. 0059specialize division_remainder_exists p
60. 0060specialize division_remainder_exists (a * S l)
61. 0061apply division_remainder_exists
62. 0062exact hp0
63. 0063cases hdiv
64. 0064cases hdiv_witness
65. 0065cases hdiv_witness_witness
66. 0066have hrem0 : ~(x3 = 0)
67. 0067intro hremzero
68. 0068have hmultiple : exists k. a * S l = p * k
69. 0069exists x2
70. 0070trans p * x2 + x3
71. 0071exact hdiv_witness_witness_left
72. 0072rewrite hremzero
73. 0073apply PA3
74. 0074have hfactor : (exists u. a = p * u) \/ exists v. S l = p * v
75. 0075specialize euclid_prime_dvd_product p
76. 0076specialize euclid_prime_dvd_product a
77. 0077specialize euclid_prime_dvd_product (S l)
78. 0078apply euclid_prime_dvd_product
79. 0079exact hp
80. 0080exact hmultiple
81. 0081cases hfactor
82. 0082apply hnotdiv
83. 0083exact hfactor_left
84. 0084have hsl0 : ~(S l = 0)
85. 0085specialize succ_ne_zero l
86. 0086exact succ_ne_zero
87. 0087have hple : exists k. k + p = S l
88. 0088specialize divisor_le_nonzero p
89. 0089specialize divisor_le_nonzero (S l)
90. 0090apply divisor_le_nonzero
91. 0091exact hsl0
92. 0092exact hfactor_right
93. 0093specialize lt_not_le (S l)
94. 0094specialize lt_not_le p
95. 0095apply lt_not_le
96. 0096exact hslp
97. 0097exact hple
98. 0098have hrem_succ : exists j. x3 = S j
99. 0099specialize nonzero_is_succ x3
100. 0100apply nonzero_is_succ
101. 0101exact hrem0
102. 0102cases hrem_succ
103. 0103have hjn : exists h. h + S x4 = n
104. 0104specialize le_of_succ_le_succ (S x4)
105. 0105specialize le_of_succ_le_succ n
106. 0106apply le_of_succ_le_succ
107. 0107rewrite <- hrem_succ_witness
108. 0108rewrite <- hpn
109. 0109exact hdiv_witness_witness_right
110. 0110have hdecomp : a * S l = x2 * p + x3
111. 0111trans p * x2 + x3
112. 0112exact hdiv_witness_witness_left
113. 0113congr
114. 0114apply mul_comm
115. 0115refl
116. 0116have hmodrem : exists u v. a * S l + p * u = x3 + p * v
117. 0117specialize remainder_decomposition_to_mod_eq p
118. 0118specialize remainder_decomposition_to_mod_eq (a * S l)
119. 0119specialize remainder_decomposition_to_mod_eq x2
120. 0120specialize remainder_decomposition_to_mod_eq x3
121. 0121apply remainder_decomposition_to_mod_eq
122. 0122exact hdecomp
123. 0123have hmod : exists u v. a * S l + p * u = S x4 + p * v
124. 0124rewrite <- hrem_succ_witness
125. 0125exact hmodrem
126. 0126specialize beta_prefix_extend l
127. 0127specialize beta_prefix_extend x
128. 0128specialize beta_prefix_extend x1
129. 0129specialize beta_prefix_extend x4
130. 0130cases beta_prefix_extend
131. 0131cases beta_prefix_extend_witness
132. 0132cases beta_prefix_extend_witness_witness
133. 0133exists x5
134. 0134exists x6
135. 0135intro i
136. 0136intro hi
137. 0137have hsplit : i = l \/ exists h. h + S i = l
138. 0138specialize finite_lt_succ_eq_or_lt l
139. 0139specialize finite_lt_succ_eq_or_lt i
140. 0140apply finite_lt_succ_eq_or_lt
141. 0141exact hi
142. 0142cases hsplit
143. 0143exists x4
144. 0144split
145. 0145exact hjn
146. 0146split
147. 0147rewrite hsplit_left
148. 0148rewrite hsplit_left
149. 0149exact beta_prefix_extend_witness_witness_left
150. 0150rewrite hsplit_left
151. 0151exact hmod
152. 0152have hold : (exists frm_residue_previous_at_i. (exists frm_gap_previous_at_i_residue_bound. frm_gap_previous_at_i_residue_bound + S frm_residue_previous_at_i = n) /\ ((((exists ff_h_frm_previous_at_i_decoded. ff_h_frm_previous_at_i_decoded + S (frm_residue_previous_at_i) = S ((S (i)) * x1)) /\ exists ff_q_frm_previous_at_i_decoded. x = ff_q_frm_previous_at_i_decoded * S ((S (i)) * x1) + (frm_residue_previous_at_i))) /\ (exists frm_mod_left_previous_at_i_congruence frm_mod_right_previous_at_i_congruence. a * S i + p * frm_mod_left_previous_at_i_congruence = S frm_residue_previous_at_i + p * frm_mod_right_previous_at_i_congruence)))
153. 0153specialize hprev_witness_witness i
154. 0154apply hprev_witness_witness
155. 0155exact hsplit_right
156. 0156cases hold
157. 0157cases hold_witness
158. 0158cases hold_witness_right
159. 0159exists x7
160. 0160split
161. 0161exact hold_witness_left
162. 0162split
163. 0163specialize beta_prefix_extend_witness_witness_right i
164. 0164specialize beta_prefix_extend_witness_witness_right x7
165. 0165apply beta_prefix_extend_witness_witness_right
166. 0166exact hsplit_right
167. 0167exact hold_witness_right_left
168. 0168exact hold_witness_right_right