finite_bounded_injective_surjective

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. 0001induction n
2. 0002intro b
3. 0003intro c
4. 0004intro hbounded
5. 0005intro hinjective
6. 0006specialize finite_surjective_zero b
7. 0007specialize finite_surjective_zero c
8. 0008specialize finite_surjective_zero 0
9. 0009apply finite_surjective_zero
10. 0010refl
11. 0011intro b
12. 0012intro c
13. 0013intro hbounded
14. 0014intro hinjective
15. 0015have hcontains : (exists fp_i_contains_top. ((exists fp_gap_contains_top_index. fp_gap_contains_top_index + S fp_i_contains_top = n) /\ (((exists ff_h_contains_top_entry. ff_h_contains_top_entry + S (n) = S ((S (fp_i_contains_top)) * c)) /\ exists ff_q_contains_top_entry. b = ff_q_contains_top_entry * S ((S (fp_i_contains_top)) * c) + (n))))) \/ ~(exists fp_i_contains_top. ((exists fp_gap_contains_top_index. fp_gap_contains_top_index + S fp_i_contains_top = n) /\ (((exists ff_h_contains_top_entry. ff_h_contains_top_entry + S (n) = S ((S (fp_i_contains_top)) * c)) /\ exists ff_q_contains_top_entry. b = ff_q_contains_top_entry * S ((S (fp_i_contains_top)) * c) + (n)))))
16. 0016specialize finite_contains_decidable b
17. 0017specialize finite_contains_decidable c
18. 0018specialize finite_contains_decidable n
19. 0019specialize finite_contains_decidable n
20. 0020exact finite_contains_decidable
21. 0021cases hcontains
22. 0022cases hcontains_left
23. 0023cases hcontains_left_witness
24. 0024have hlast : exists y. (((exists h. h + S y = S ((S n) * c)) /\ exists q. b = q * S ((S n) * c) + y) /\ exists h. h + S y = S n)
25. 0025specialize finite_bounded_last_succ b
26. 0026specialize finite_bounded_last_succ c
27. 0027specialize finite_bounded_last_succ n
28. 0028specialize finite_bounded_last_succ (S n)
29. 0029apply finite_bounded_last_succ
30. 0030refl
31. 0031exact hbounded
32. 0032cases hlast
33. 0033cases hlast_witness
34. 0034have hswap : exists z d. ((((exists ff_h_pigeon_swap_new_i. ff_h_pigeon_swap_new_i + S (x1) = S ((S (x)) * d)) /\ exists ff_q_pigeon_swap_new_i. z = ff_q_pigeon_swap_new_i * S ((S (x)) * d) + (x1))) /\ ((((exists ff_h_pigeon_swap_new_n. ff_h_pigeon_swap_new_n + S (n) = S ((S (n)) * d)) /\ exists ff_q_pigeon_swap_new_n. z = ff_q_pigeon_swap_new_n * S ((S (n)) * d) + (n))) /\ forall j a. (exists h. h + S j = S n) -> ~(j = x) -> ~(j = n) -> (((exists ff_h_pigeon_swap_old_other. ff_h_pigeon_swap_old_other + S (a) = S ((S (j)) * c)) /\ exists ff_q_pigeon_swap_old_other. b = ff_q_pigeon_swap_old_other * S ((S (j)) * c) + (a))) -> (((exists ff_h_pigeon_swap_new_other. ff_h_pigeon_swap_new_other + S (a) = S ((S (j)) * d)) /\ exists ff_q_pigeon_swap_new_other. z = ff_q_pigeon_swap_new_other * S ((S (j)) * d) + (a)))))
35. 0035specialize beta_prefix_swap_last_from_entries b
36. 0036specialize beta_prefix_swap_last_from_entries c
37. 0037specialize beta_prefix_swap_last_from_entries n
38. 0038specialize beta_prefix_swap_last_from_entries x
39. 0039specialize beta_prefix_swap_last_from_entries n
40. 0040specialize beta_prefix_swap_last_from_entries x1
41. 0041apply beta_prefix_swap_last_from_entries
42. 0042exact hcontains_left_witness_left
43. 0043exact hcontains_left_witness_right
44. 0044exact hlast_witness_left
45. 0045cases hswap
46. 0046cases hswap_witness
47. 0047cases hswap_witness_witness
48. 0048cases hswap_witness_witness_right
49. 0049have hswap_bounded : forall fp_i_pigeon_swapped_bounded. (exists fp_gap_pigeon_swapped_bounded_index. fp_gap_pigeon_swapped_bounded_index + S fp_i_pigeon_swapped_bounded = S n) -> exists fp_value_pigeon_swapped_bounded. ((((exists ff_h_pigeon_swapped_bounded_entry. ff_h_pigeon_swapped_bounded_entry + S (fp_value_pigeon_swapped_bounded) = S ((S (fp_i_pigeon_swapped_bounded)) * x3)) /\ exists ff_q_pigeon_swapped_bounded_entry. x2 = ff_q_pigeon_swapped_bounded_entry * S ((S (fp_i_pigeon_swapped_bounded)) * x3) + (fp_value_pigeon_swapped_bounded))) /\ (exists fp_gap_pigeon_swapped_bounded_value. fp_gap_pigeon_swapped_bounded_value + S fp_value_pigeon_swapped_bounded = S n))
50. 0050specialize finite_swap_last_bounded b
51. 0051specialize finite_swap_last_bounded c
52. 0052specialize finite_swap_last_bounded x2
53. 0053specialize finite_swap_last_bounded x3
54. 0054specialize finite_swap_last_bounded n
55. 0055specialize finite_swap_last_bounded (S n)
56. 0056specialize finite_swap_last_bounded x
57. 0057specialize finite_swap_last_bounded n
58. 0058specialize finite_swap_last_bounded x1
59. 0059apply finite_swap_last_bounded
60. 0060refl
61. 0061exact hcontains_left_witness_left
62. 0062exact hbounded
63. 0063exact hcontains_left_witness_right
64. 0064exact hlast_witness_left
65. 0065exact hswap_witness_witness_left
66. 0066exact hswap_witness_witness_right_left
67. 0067exact hswap_witness_witness_right_right
68. 0068have hswap_injective : forall fp_i_pigeon_swapped_injective fp_j_pigeon_swapped_injective fp_value_pigeon_swapped_injective. (exists fp_gap_pigeon_swapped_injective_i. fp_gap_pigeon_swapped_injective_i + S fp_i_pigeon_swapped_injective = S n) -> (exists fp_gap_pigeon_swapped_injective_j. fp_gap_pigeon_swapped_injective_j + S fp_j_pigeon_swapped_injective = S n) -> (((exists ff_h_pigeon_swapped_injective_left. ff_h_pigeon_swapped_injective_left + S (fp_value_pigeon_swapped_injective) = S ((S (fp_i_pigeon_swapped_injective)) * x3)) /\ exists ff_q_pigeon_swapped_injective_left. x2 = ff_q_pigeon_swapped_injective_left * S ((S (fp_i_pigeon_swapped_injective)) * x3) + (fp_value_pigeon_swapped_injective))) -> (((exists ff_h_pigeon_swapped_injective_right. ff_h_pigeon_swapped_injective_right + S (fp_value_pigeon_swapped_injective) = S ((S (fp_j_pigeon_swapped_injective)) * x3)) /\ exists ff_q_pigeon_swapped_injective_right. x2 = ff_q_pigeon_swapped_injective_right * S ((S (fp_j_pigeon_swapped_injective)) * x3) + (fp_value_pigeon_swapped_injective))) -> fp_i_pigeon_swapped_injective = fp_j_pigeon_swapped_injective
69. 0069specialize finite_swap_last_injective b
70. 0070specialize finite_swap_last_injective c
71. 0071specialize finite_swap_last_injective x2
72. 0072specialize finite_swap_last_injective x3
73. 0073specialize finite_swap_last_injective n
74. 0074specialize finite_swap_last_injective (S n)
75. 0075specialize finite_swap_last_injective x
76. 0076specialize finite_swap_last_injective n
77. 0077specialize finite_swap_last_injective x1
78. 0078apply finite_swap_last_injective
79. 0079refl
80. 0080exact hcontains_left_witness_left
81. 0081exact hinjective
82. 0082exact hcontains_left_witness_right
83. 0083exact hlast_witness_left
84. 0084exact hswap_witness_witness_left
85. 0085exact hswap_witness_witness_right_left
86. 0086exact hswap_witness_witness_right_right
87. 0087have hnotop : forall j. (exists h. h + S j = n) -> ~(((exists ff_h_pigeon_top_j. ff_h_pigeon_top_j + S (n) = S ((S (j)) * x3)) /\ exists ff_q_pigeon_top_j. x2 = ff_q_pigeon_top_j * S ((S (j)) * x3) + (n)))
88. 0088intro j
89. 0089intro hj
90. 0090intro htop
91. 0091have hjsn : exists h. h + S j = S n
92. 0092specialize le_succ (S j)
93. 0093specialize le_succ n
94. 0094apply le_succ
95. 0095exact hj
96. 0096have hnsn : exists h. h + S n = S n
97. 0097specialize le_refl (S n)
98. 0098exact le_refl
99. 0099have hjneq : j = n
100. 0100specialize hswap_injective j
101. 0101specialize hswap_injective n
102. 0102specialize hswap_injective n
103. 0103apply hswap_injective
104. 0104exact hjsn
105. 0105exact hnsn
106. 0106exact htop
107. 0107exact hswap_witness_witness_right_left
108. 0108specialize lt_irrefl_expanded n
109. 0109apply lt_irrefl_expanded
110. 0110rewrite hjneq at hj
111. 0111exact hj
112. 0112have hprefix_bounded : forall fp_i_pigeon_swapped_prefix_bounded. (exists fp_gap_pigeon_swapped_prefix_bounded_index. fp_gap_pigeon_swapped_prefix_bounded_index + S fp_i_pigeon_swapped_prefix_bounded = n) -> exists fp_value_pigeon_swapped_prefix_bounded. ((((exists ff_h_pigeon_swapped_prefix_bounded_entry. ff_h_pigeon_swapped_prefix_bounded_entry + S (fp_value_pigeon_swapped_prefix_bounded) = S ((S (fp_i_pigeon_swapped_prefix_bounded)) * x3)) /\ exists ff_q_pigeon_swapped_prefix_bounded_entry. x2 = ff_q_pigeon_swapped_prefix_bounded_entry * S ((S (fp_i_pigeon_swapped_prefix_bounded)) * x3) + (fp_value_pigeon_swapped_prefix_bounded))) /\ (exists fp_gap_pigeon_swapped_prefix_bounded_value. fp_gap_pigeon_swapped_prefix_bounded_value + S fp_value_pigeon_swapped_prefix_bounded = n))
113. 0113specialize finite_bounded_prefix_without_top x2
114. 0114specialize finite_bounded_prefix_without_top x3
115. 0115specialize finite_bounded_prefix_without_top n
116. 0116specialize finite_bounded_prefix_without_top (S n)
117. 0117apply finite_bounded_prefix_without_top
118. 0118refl
119. 0119exact hswap_bounded
120. 0120exact hnotop
121. 0121have hprefix_injective : forall fp_i_pigeon_swapped_prefix_injective fp_j_pigeon_swapped_prefix_injective fp_value_pigeon_swapped_prefix_injective. (exists fp_gap_pigeon_swapped_prefix_injective_i. fp_gap_pigeon_swapped_prefix_injective_i + S fp_i_pigeon_swapped_prefix_injective = n) -> (exists fp_gap_pigeon_swapped_prefix_injective_j. fp_gap_pigeon_swapped_prefix_injective_j + S fp_j_pigeon_swapped_prefix_injective = n) -> (((exists ff_h_pigeon_swapped_prefix_injective_left. ff_h_pigeon_swapped_prefix_injective_left + S (fp_value_pigeon_swapped_prefix_injective) = S ((S (fp_i_pigeon_swapped_prefix_injective)) * x3)) /\ exists ff_q_pigeon_swapped_prefix_injective_left. x2 = ff_q_pigeon_swapped_prefix_injective_left * S ((S (fp_i_pigeon_swapped_prefix_injective)) * x3) + (fp_value_pigeon_swapped_prefix_injective))) -> (((exists ff_h_pigeon_swapped_prefix_injective_right. ff_h_pigeon_swapped_prefix_injective_right + S (fp_value_pigeon_swapped_prefix_injective) = S ((S (fp_j_pigeon_swapped_prefix_injective)) * x3)) /\ exists ff_q_pigeon_swapped_prefix_injective_right. x2 = ff_q_pigeon_swapped_prefix_injective_right * S ((S (fp_j_pigeon_swapped_prefix_injective)) * x3) + (fp_value_pigeon_swapped_prefix_injective))) -> fp_i_pigeon_swapped_prefix_injective = fp_j_pigeon_swapped_prefix_injective
122. 0122specialize finite_injective_prefix_succ x2
123. 0123specialize finite_injective_prefix_succ x3
124. 0124specialize finite_injective_prefix_succ n
125. 0125specialize finite_injective_prefix_succ (S n)
126. 0126apply finite_injective_prefix_succ
127. 0127refl
128. 0128exact hswap_injective
129. 0129have hprefix_surjective : forall fp_value_pigeon_swapped_prefix_surjective. (exists fp_gap_pigeon_swapped_prefix_surjective_value. fp_gap_pigeon_swapped_prefix_surjective_value + S fp_value_pigeon_swapped_prefix_surjective = n) -> exists fp_i_pigeon_swapped_prefix_surjective. ((exists fp_gap_pigeon_swapped_prefix_surjective_index. fp_gap_pigeon_swapped_prefix_surjective_index + S fp_i_pigeon_swapped_prefix_surjective = n) /\ (((exists ff_h_pigeon_swapped_prefix_surjective_entry. ff_h_pigeon_swapped_prefix_surjective_entry + S (fp_value_pigeon_swapped_prefix_surjective) = S ((S (fp_i_pigeon_swapped_prefix_surjective)) * x3)) /\ exists ff_q_pigeon_swapped_prefix_surjective_entry. x2 = ff_q_pigeon_swapped_prefix_surjective_entry * S ((S (fp_i_pigeon_swapped_prefix_surjective)) * x3) + (fp_value_pigeon_swapped_prefix_surjective))))
130. 0130specialize IH x2
131. 0131specialize IH x3
132. 0132apply IH
133. 0133exact hprefix_bounded
134. 0134exact hprefix_injective
135. 0135have hswap_surjective : forall fp_value_pigeon_swapped_surjective. (exists fp_gap_pigeon_swapped_surjective_value. fp_gap_pigeon_swapped_surjective_value + S fp_value_pigeon_swapped_surjective = S n) -> exists fp_i_pigeon_swapped_surjective. ((exists fp_gap_pigeon_swapped_surjective_index. fp_gap_pigeon_swapped_surjective_index + S fp_i_pigeon_swapped_surjective = S n) /\ (((exists ff_h_pigeon_swapped_surjective_entry. ff_h_pigeon_swapped_surjective_entry + S (fp_value_pigeon_swapped_surjective) = S ((S (fp_i_pigeon_swapped_surjective)) * x3)) /\ exists ff_q_pigeon_swapped_surjective_entry. x2 = ff_q_pigeon_swapped_surjective_entry * S ((S (fp_i_pigeon_swapped_surjective)) * x3) + (fp_value_pigeon_swapped_surjective))))
136. 0136specialize finite_surjective_succ_from_prefix x2
137. 0137specialize finite_surjective_succ_from_prefix x3
138. 0138specialize finite_surjective_succ_from_prefix n
139. 0139specialize finite_surjective_succ_from_prefix (S n)
140. 0140apply finite_surjective_succ_from_prefix
141. 0141refl
142. 0142exact hswap_bounded
143. 0143exact hswap_injective
144. 0144exact hprefix_surjective
145. 0145specialize finite_swap_last_surjective_back b
146. 0146specialize finite_swap_last_surjective_back c
147. 0147specialize finite_swap_last_surjective_back x2
148. 0148specialize finite_swap_last_surjective_back x3
149. 0149specialize finite_swap_last_surjective_back n
150. 0150specialize finite_swap_last_surjective_back (S n)
151. 0151specialize finite_swap_last_surjective_back x
152. 0152specialize finite_swap_last_surjective_back n
153. 0153specialize finite_swap_last_surjective_back x1
154. 0154apply finite_swap_last_surjective_back
155. 0155refl
156. 0156exact hcontains_left_witness_left
157. 0157exact hcontains_left_witness_right
158. 0158exact hlast_witness_left
159. 0159exact hswap_witness_witness_left
160. 0160exact hswap_witness_witness_right_left
161. 0161exact hswap_witness_witness_right_right
162. 0162exact hswap_surjective
163. 0163specialize finite_no_top_successor_gate b
164. 0164specialize finite_no_top_successor_gate c
165. 0165specialize finite_no_top_successor_gate n
166. 0166specialize finite_no_top_successor_gate (S n)
167. 0167apply finite_no_top_successor_gate
168. 0168refl
169. 0169exact hbounded
170. 0170exact hinjective
171. 0171exact hcontains_right
172. 0172intro hprefix_bounded
173. 0173intro hprefix_injective
174. 0174specialize IH b
175. 0175specialize IH c
176. 0176apply IH
177. 0177exact hprefix_bounded
178. 0178exact hprefix_injective