BT00XG

division_double_quotient_bit

Alpha body-checked · checked-use disabled

Doubling a dividend changes its quotient by one binary carry.

Exact expanded PA statement

forall d n q r Q R. (((n) = (d) * (q) + (r) /\ (exists bcf_lt_gap_bddqb_source_bound. bcf_lt_gap_bddqb_source_bound + S (r) = d))) -> (((n + n) = (d) * (Q) + (R) /\ (exists bcf_lt_gap_bddqb_double_bound. bcf_lt_gap_bddqb_double_bound + S (R) = d))) -> (Q = q + q \/ Q = S (q + q))

Structural proof guide

Doubling a dividend changes its quotient by one binary carry.

Direct prerequisites: le_or_lt, le_eq_or_lt, lt_not_le, zero_le, one_le_of_ne_zero, add_shuffle_middle, mul_add, add_assoc, add_comm, add_lt_add, add_lt_cancel_left, division_remainder_unique. The authored body proceeds by case analysis (8), intermediate claims (12), equality transport (6).

Proof neighborhood

Direct dependencies

BT001G le_or_lt BT001C le_eq_or_lt BT001I lt_not_le BT000W zero_le BT0010 one_le_of_ne_zero BT00MY add_shuffle_middle BT0007 mul_add BT0003 add_assoc BT0002 add_comm BT00XB add_lt_add BT00XC add_lt_cancel_left BT001U division_remainder_unique

Direct dependents

BT00XV double_quotient_carry_choice

Formal native tactic body

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

  1. 0001intro d
  2. 0002intro n
  3. 0003intro q
  4. 0004intro r
  5. 0005intro Q
  6. 0006intro R
  7. 0007intro hsource
  8. 0008intro hdouble
  9. 0009cases hsource
  10. 0010cases hdouble
  11. 0011have hdouble_eq : n + n = d * (q + q) + (r + r)
  12. 0012rewrite hsource_left
  13. 0013rewrite hsource_left
  14. 0014trans (d * q + d * q) + (r + r)
  15. 0015apply add_shuffle_middle
  16. 0016congr
  17. 0017symm
  18. 0018apply mul_add
  19. 0019refl
  20. 0020specialize le_or_lt (r + r)
  21. 0021specialize le_or_lt d
  22. 0022cases le_or_lt
  23. 0023have hsplit : r + r = d \/ exists k. k + S (r + r) = d
  24. 0024specialize le_eq_or_lt (r + r)
  25. 0025specialize le_eq_or_lt d
  26. 0026apply le_eq_or_lt
  27. 0027exact le_or_lt_left
  28. 0028cases hsplit
  29. 0029have hd0 : ~(d = 0)
  30. 0030intro hd
  31. 0031rewrite hd at hsource_right
  32. 0032specialize lt_not_le r
  33. 0033specialize lt_not_le 0
  34. 0034apply lt_not_le
  35. 0035exact hsource_right
  36. 0036specialize zero_le r
  37. 0037exact zero_le
  38. 0038have hzero_bound : exists k. k + S 0 = d
  39. 0039specialize one_le_of_ne_zero d
  40. 0040apply one_le_of_ne_zero
  41. 0041exact hd0
  42. 0042have hcandidate_eq : n + n = d * S (q + q) + 0
  43. 0043trans d * (q + q) + (r + r)
  44. 0044exact hdouble_eq
  45. 0045rewrite hsplit_left
  46. 0046trans d * S (q + q)
  47. 0047symm
  48. 0048apply PA6
  49. 0049symm
  50. 0050apply PA3
  51. 0051have hunique : Q = S (q + q) /\ R = 0
  52. 0052specialize division_remainder_unique d
  53. 0053specialize division_remainder_unique (n + n)
  54. 0054specialize division_remainder_unique Q
  55. 0055specialize division_remainder_unique R
  56. 0056specialize division_remainder_unique (S (q + q))
  57. 0057specialize division_remainder_unique 0
  58. 0058apply division_remainder_unique
  59. 0059exact hdouble_left
  60. 0060exact hdouble_right
  61. 0061exact hcandidate_eq
  62. 0062exact hzero_bound
  63. 0063cases hunique
  64. 0064right
  65. 0065exact hunique_left
  66. 0066have hunique : Q = q + q /\ R = r + r
  67. 0067specialize division_remainder_unique d
  68. 0068specialize division_remainder_unique (n + n)
  69. 0069specialize division_remainder_unique Q
  70. 0070specialize division_remainder_unique R
  71. 0071specialize division_remainder_unique (q + q)
  72. 0072specialize division_remainder_unique (r + r)
  73. 0073apply division_remainder_unique
  74. 0074exact hdouble_left
  75. 0075exact hdouble_right
  76. 0076exact hdouble_eq
  77. 0077exact hsplit_right
  78. 0078cases hunique
  79. 0079left
  80. 0080exact hunique_left
  81. 0081cases le_or_lt_right
  82. 0082have hrr : r + r = d + S x
  83. 0083trans x + S d
  84. 0084symm
  85. 0085exact le_or_lt_right_witness
  86. 0086trans S (x + d)
  87. 0087apply PA4
  88. 0088trans S (d + x)
  89. 0089congr
  90. 0090apply add_comm
  91. 0091symm
  92. 0092apply PA4
  93. 0093have hsum_lt : exists k. k + S (r + r) = d + d
  94. 0094specialize add_lt_add r
  95. 0095specialize add_lt_add d
  96. 0096specialize add_lt_add r
  97. 0097specialize add_lt_add d
  98. 0098apply add_lt_add
  99. 0099exact hsource_right
  100. 0100exact hsource_right
  101. 0101rewrite hrr at hsum_lt
  102. 0102have hcarry_bound : exists k. k + S (S x) = d
  103. 0103specialize add_lt_cancel_left d
  104. 0104specialize add_lt_cancel_left (S x)
  105. 0105specialize add_lt_cancel_left d
  106. 0106apply add_lt_cancel_left
  107. 0107exact hsum_lt
  108. 0108have hcandidate_eq : n + n = d * S (q + q) + S x
  109. 0109trans d * (q + q) + (r + r)
  110. 0110exact hdouble_eq
  111. 0111rewrite hrr
  112. 0112trans (d * (q + q) + d) + S x
  113. 0113symm
  114. 0114apply add_assoc
  115. 0115congr
  116. 0116symm
  117. 0117apply PA6
  118. 0118refl
  119. 0119have hunique : Q = S (q + q) /\ R = S x
  120. 0120specialize division_remainder_unique d
  121. 0121specialize division_remainder_unique (n + n)
  122. 0122specialize division_remainder_unique Q
  123. 0123specialize division_remainder_unique R
  124. 0124specialize division_remainder_unique (S (q + q))
  125. 0125specialize division_remainder_unique (S x)
  126. 0126apply division_remainder_unique
  127. 0127exact hdouble_left
  128. 0128exact hdouble_right
  129. 0129exact hcandidate_eq
  130. 0130exact hcarry_bound
  131. 0131cases hunique
  132. 0132right
  133. 0133exact hunique_left