BT004F

binary_crt

Stable · empty-context checked

Constructive binary CRT for positive coprime natural moduli using balanced congruence.

Exact expanded PA statement

forall m n a b. ~(m = 0) -> ~(n = 0) -> (forall d. (exists u. m = d * u) -> (exists v. n = d * v) -> d = 1) -> exists x. (exists u v. x + m * u = a + m * v) /\ (exists r s. x + n * r = b + n * s)

Structural proof guide

Constructive binary CRT for positive coprime natural moduli using balanced congruence.

Direct prerequisites: nonzero_is_succ, coprime_balanced_bezout, bezout_mod_left, bezout_mod_right, mod_eq_mul_left, mul_add, mul_one, dvd_to_mod_zero, mul_assoc, mul_comm, mod_eq_add, mod_eq_refl, mod_eq_trans, mod_eq_predecessor_cancel, zero_add. The authored body proceeds by case analysis (6), intermediate claims (35), equality transport (11).

Proof neighborhood

Direct dependencies

BT000R nonzero_is_succ BT0038 coprime_balanced_bezout BT004C bezout_mod_left BT004D bezout_mod_right BT003T mod_eq_mul_left BT0007 mul_add BT000A mul_one BT0046 dvd_to_mod_zero BT0008 mul_assoc BT0006 mul_comm BT003R mod_eq_add BT003O mod_eq_refl BT003Q mod_eq_trans BT004E mod_eq_predecessor_cancel BT0000 zero_add

Direct dependents

BT004U binary_crt_fold_step

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  1. 0001intro m
  2. 0002intro n
  3. 0003intro a
  4. 0004intro b
  5. 0005intro hm
  6. 0006intro hn
  7. 0007intro hcop
  8. 0008have hms : exists k. m = S k
  9. 0009specialize nonzero_is_succ m
  10. 0010apply nonzero_is_succ
  11. 0011exact hm
  12. 0012have hns : exists k. n = S k
  13. 0013specialize nonzero_is_succ n
  14. 0014apply nonzero_is_succ
  15. 0015exact hn
  16. 0016have hbez : exists xp yp xn yn. m * xp + n * yp = 1 + (m * xn + n * yn)
  17. 0017specialize coprime_balanced_bezout m
  18. 0018specialize coprime_balanced_bezout n
  19. 0019apply coprime_balanced_bezout
  20. 0020exact hcop
  21. 0021cases hms
  22. 0022cases hns
  23. 0023cases hbez
  24. 0024cases hbez_witness
  25. 0025cases hbez_witness_witness
  26. 0026cases hbez_witness_witness_witness
  27. 0027have hbl : exists u v. n * x3 + m * u = (1 + n * x5) + m * v
  28. 0028specialize bezout_mod_left m
  29. 0029specialize bezout_mod_left n
  30. 0030specialize bezout_mod_left x2
  31. 0031specialize bezout_mod_left x3
  32. 0032specialize bezout_mod_left x4
  33. 0033specialize bezout_mod_left x5
  34. 0034apply bezout_mod_left
  35. 0035exact hbez_witness_witness_witness_witness
  36. 0036have hbr : exists u v. m * x2 + n * u = (1 + m * x4) + n * v
  37. 0037specialize bezout_mod_right m
  38. 0038specialize bezout_mod_right n
  39. 0039specialize bezout_mod_right x2
  40. 0040specialize bezout_mod_right x3
  41. 0041specialize bezout_mod_right x4
  42. 0042specialize bezout_mod_right x5
  43. 0043apply bezout_mod_right
  44. 0044exact hbez_witness_witness_witness_witness
  45. 0045have hal0 : exists u v. (a * (n * x3)) + m * u = (a * (1 + n * x5)) + m * v
  46. 0046specialize mod_eq_mul_left m
  47. 0047specialize mod_eq_mul_left (n * x3)
  48. 0048specialize mod_eq_mul_left (1 + n * x5)
  49. 0049specialize mod_eq_mul_left a
  50. 0050apply mod_eq_mul_left
  51. 0051exact hbl
  52. 0052have hal : exists u v. (a * (n * x3)) + m * u = (a + a * (n * x5)) + m * v
  53. 0053have haexpand : a * (1 + n * x5) = a + a * (n * x5)
  54. 0054trans a * 1 + a * (n * x5)
  55. 0055apply mul_add
  56. 0056congr
  57. 0057apply mul_one
  58. 0058refl
  59. 0059rewrite <- haexpand
  60. 0060exact hal0
  61. 0061have hbm : exists u v. (b * (m * x2)) + m * u = 0 + m * v
  62. 0062apply dvd_to_mod_zero
  63. 0063exists b * x2
  64. 0064trans (b * m) * x2
  65. 0065symm
  66. 0066apply mul_assoc
  67. 0067trans (m * b) * x2
  68. 0068congr
  69. 0069apply mul_comm
  70. 0070refl
  71. 0071apply mul_assoc
  72. 0072have hym : exists u v. ((a * (n * x3)) + (b * (m * x2))) + m * u = ((a + a * (n * x5)) + 0) + m * v
  73. 0073specialize mod_eq_add m
  74. 0074specialize mod_eq_add (a * (n * x3))
  75. 0075specialize mod_eq_add (a + a * (n * x5))
  76. 0076specialize mod_eq_add (b * (m * x2))
  77. 0077specialize mod_eq_add 0
  78. 0078apply mod_eq_add
  79. 0079exact hal
  80. 0080exact hbm
  81. 0081have hym_norm : exists u v. ((a * (n * x3)) + (b * (m * x2))) + m * u = (a + a * (n * x5)) + m * v
  82. 0082have hym_zero : (a + a * (n * x5)) + 0 = a + a * (n * x5)
  83. 0083rewrite PA3
  84. 0084refl
  85. 0085rewrite <- hym_zero
  86. 0086exact hym
  87. 0087have hkm : exists u v. (x * (a * (n * x5))) + m * u = (x * (a * (n * x5))) + m * v
  88. 0088specialize mod_eq_refl m
  89. 0089specialize mod_eq_refl (x * (a * (n * x5)))
  90. 0090apply mod_eq_refl
  91. 0091have hymk : exists u v. (((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5)))) + m * u = ((a + a * (n * x5)) + (x * (a * (n * x5)))) + m * v
  92. 0092specialize mod_eq_add m
  93. 0093specialize mod_eq_add ((a * (n * x3)) + (b * (m * x2)))
  94. 0094specialize mod_eq_add (a + a * (n * x5))
  95. 0095specialize mod_eq_add (x * (a * (n * x5)))
  96. 0096specialize mod_eq_add (x * (a * (n * x5)))
  97. 0097apply mod_eq_add
  98. 0098exact hym_norm
  99. 0099exact hkm
  100. 0100have hcancelm : exists u v. ((a + a * (n * x5)) + x * (a * (n * x5))) + S x * u = a + S x * v
  101. 0101specialize mod_eq_predecessor_cancel x
  102. 0102specialize mod_eq_predecessor_cancel a
  103. 0103specialize mod_eq_predecessor_cancel (a * (n * x5))
  104. 0104apply mod_eq_predecessor_cancel
  105. 0105rewrite <- hms_witness at hcancelm
  106. 0106rewrite <- hms_witness at hcancelm
  107. 0107have hbasem : exists u v. (((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5)))) + m * u = a + m * v
  108. 0108specialize mod_eq_trans m
  109. 0109specialize mod_eq_trans (((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5))))
  110. 0110specialize mod_eq_trans ((a + a * (n * x5)) + (x * (a * (n * x5))))
  111. 0111specialize mod_eq_trans a
  112. 0112apply mod_eq_trans
  113. 0113exact hymk
  114. 0114exact hcancelm
  115. 0115have hknznm : exists u v. (x1 * (b * (m * x4))) + m * u = 0 + m * v
  116. 0116apply dvd_to_mod_zero
  117. 0117exists x1 * (b * x4)
  118. 0118trans x1 * ((b * m) * x4)
  119. 0119congr
  120. 0120refl
  121. 0121symm
  122. 0122apply mul_assoc
  123. 0123trans x1 * ((m * b) * x4)
  124. 0124congr
  125. 0125refl
  126. 0126congr
  127. 0127apply mul_comm
  128. 0128refl
  129. 0129trans x1 * (m * (b * x4))
  130. 0130congr
  131. 0131refl
  132. 0132apply mul_assoc
  133. 0133trans (x1 * m) * (b * x4)
  134. 0134symm
  135. 0135apply mul_assoc
  136. 0136trans (m * x1) * (b * x4)
  137. 0137congr
  138. 0138apply mul_comm
  139. 0139refl
  140. 0140apply mul_assoc
  141. 0141have hfinalm0 : exists u v. ((((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5)))) + (x1 * (b * (m * x4)))) + m * u = (a + 0) + m * v
  142. 0142specialize mod_eq_add m
  143. 0143specialize mod_eq_add (((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5))))
  144. 0144specialize mod_eq_add a
  145. 0145specialize mod_eq_add (x1 * (b * (m * x4)))
  146. 0146specialize mod_eq_add 0
  147. 0147apply mod_eq_add
  148. 0148exact hbasem
  149. 0149exact hknznm
  150. 0150have hazerom : exists u v. (a + 0) + m * u = a + m * v
  151. 0151exists 0
  152. 0152exists 0
  153. 0153simp
  154. 0154have hfinalm : exists u v. ((((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5)))) + (x1 * (b * (m * x4)))) + m * u = a + m * v
  155. 0155specialize mod_eq_trans m
  156. 0156specialize mod_eq_trans ((((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5)))) + (x1 * (b * (m * x4))))
  157. 0157specialize mod_eq_trans (a + 0)
  158. 0158specialize mod_eq_trans a
  159. 0159apply mod_eq_trans
  160. 0160exact hfinalm0
  161. 0161exact hazerom
  162. 0162have hbn0 : exists u v. (b * (m * x2)) + n * u = (b * (1 + m * x4)) + n * v
  163. 0163specialize mod_eq_mul_left n
  164. 0164specialize mod_eq_mul_left (m * x2)
  165. 0165specialize mod_eq_mul_left (1 + m * x4)
  166. 0166specialize mod_eq_mul_left b
  167. 0167apply mod_eq_mul_left
  168. 0168exact hbr
  169. 0169have hbn : exists u v. (b * (m * x2)) + n * u = (b + b * (m * x4)) + n * v
  170. 0170have hbexpand : b * (1 + m * x4) = b + b * (m * x4)
  171. 0171trans b * 1 + b * (m * x4)
  172. 0172apply mul_add
  173. 0173congr
  174. 0174apply mul_one
  175. 0175refl
  176. 0176rewrite <- hbexpand
  177. 0177exact hbn0
  178. 0178have han : exists u v. (a * (n * x3)) + n * u = 0 + n * v
  179. 0179apply dvd_to_mod_zero
  180. 0180exists a * x3
  181. 0181trans (a * n) * x3
  182. 0182symm
  183. 0183apply mul_assoc
  184. 0184trans (n * a) * x3
  185. 0185congr
  186. 0186apply mul_comm
  187. 0187refl
  188. 0188apply mul_assoc
  189. 0189have hyn0 : exists u v. ((a * (n * x3)) + (b * (m * x2))) + n * u = (0 + (b + b * (m * x4))) + n * v
  190. 0190specialize mod_eq_add n
  191. 0191specialize mod_eq_add (a * (n * x3))
  192. 0192specialize mod_eq_add 0
  193. 0193specialize mod_eq_add (b * (m * x2))
  194. 0194specialize mod_eq_add (b + b * (m * x4))
  195. 0195apply mod_eq_add
  196. 0196exact han
  197. 0197exact hbn
  198. 0198have hyn_norm : exists u v. ((a * (n * x3)) + (b * (m * x2))) + n * u = (b + b * (m * x4)) + n * v
  199. 0199have hyn_zero : 0 + (b + b * (m * x4)) = b + b * (m * x4)
  200. 0200specialize zero_add (b + b * (m * x4))
  201. 0201exact zero_add
  202. 0202rewrite <- hyn_zero
  203. 0203exact hyn0
  204. 0204have hkmz : exists u v. (x * (a * (n * x5))) + n * u = 0 + n * v
  205. 0205apply dvd_to_mod_zero
  206. 0206exists x * (a * x5)
  207. 0207trans x * ((a * n) * x5)
  208. 0208congr
  209. 0209refl
  210. 0210symm
  211. 0211apply mul_assoc
  212. 0212trans x * ((n * a) * x5)
  213. 0213congr
  214. 0214refl
  215. 0215congr
  216. 0216apply mul_comm
  217. 0217refl
  218. 0218trans x * (n * (a * x5))
  219. 0219congr
  220. 0220refl
  221. 0221apply mul_assoc
  222. 0222trans (x * n) * (a * x5)
  223. 0223symm
  224. 0224apply mul_assoc
  225. 0225trans (n * x) * (a * x5)
  226. 0226congr
  227. 0227apply mul_comm
  228. 0228refl
  229. 0229apply mul_assoc
  230. 0230have hyn1 : exists u v. (((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5)))) + n * u = ((b + b * (m * x4)) + 0) + n * v
  231. 0231specialize mod_eq_add n
  232. 0232specialize mod_eq_add ((a * (n * x3)) + (b * (m * x2)))
  233. 0233specialize mod_eq_add (b + b * (m * x4))
  234. 0234specialize mod_eq_add (x * (a * (n * x5)))
  235. 0235specialize mod_eq_add 0
  236. 0236apply mod_eq_add
  237. 0237exact hyn_norm
  238. 0238exact hkmz
  239. 0239have hyn1_norm : exists u v. (((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5)))) + n * u = (b + b * (m * x4)) + n * v
  240. 0240have hyn1_zero : (b + b * (m * x4)) + 0 = b + b * (m * x4)
  241. 0241rewrite PA3
  242. 0242refl
  243. 0243rewrite <- hyn1_zero
  244. 0244exact hyn1
  245. 0245have hkn : exists u v. (x1 * (b * (m * x4))) + n * u = (x1 * (b * (m * x4))) + n * v
  246. 0246specialize mod_eq_refl n
  247. 0247specialize mod_eq_refl (x1 * (b * (m * x4)))
  248. 0248apply mod_eq_refl
  249. 0249have hynk : exists u v. ((((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5)))) + (x1 * (b * (m * x4)))) + n * u = ((b + b * (m * x4)) + (x1 * (b * (m * x4)))) + n * v
  250. 0250specialize mod_eq_add n
  251. 0251specialize mod_eq_add (((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5))))
  252. 0252specialize mod_eq_add (b + b * (m * x4))
  253. 0253specialize mod_eq_add (x1 * (b * (m * x4)))
  254. 0254specialize mod_eq_add (x1 * (b * (m * x4)))
  255. 0255apply mod_eq_add
  256. 0256exact hyn1_norm
  257. 0257exact hkn
  258. 0258have hcanceln : exists u v. ((b + b * (m * x4)) + x1 * (b * (m * x4))) + S x1 * u = b + S x1 * v
  259. 0259specialize mod_eq_predecessor_cancel x1
  260. 0260specialize mod_eq_predecessor_cancel b
  261. 0261specialize mod_eq_predecessor_cancel (b * (m * x4))
  262. 0262apply mod_eq_predecessor_cancel
  263. 0263rewrite <- hns_witness at hcanceln
  264. 0264rewrite <- hns_witness at hcanceln
  265. 0265have hfinaln : exists u v. ((((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5)))) + (x1 * (b * (m * x4)))) + n * u = b + n * v
  266. 0266specialize mod_eq_trans n
  267. 0267specialize mod_eq_trans ((((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5)))) + (x1 * (b * (m * x4))))
  268. 0268specialize mod_eq_trans ((b + b * (m * x4)) + (x1 * (b * (m * x4))))
  269. 0269specialize mod_eq_trans b
  270. 0270apply mod_eq_trans
  271. 0271exact hynk
  272. 0272exact hcanceln
  273. 0273exists (((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5)))) + (x1 * (b * (m * x4)))
  274. 0274split
  275. 0275exact hfinalm
  276. 0276exact hfinaln