BT00SH

division_successor_quotient_by_bit

Alpha body-checked · checked-use disabled

A divisibility bit is exactly the successor quotient increment.

Exact expanded PA statement

forall d n q r z s bit. (((n) = (d) * (q) + (r) /\ exists blsr_lt_gap_quotient_bit_old_bound. blsr_lt_gap_quotient_bit_old_bound + S (r) = (d))) -> (((S n) = (d) * (z) + (s) /\ exists blsr_lt_gap_quotient_bit_new_bound. blsr_lt_gap_quotient_bit_new_bound + S (s) = (d))) -> ((bit = 1 /\ (exists k. S n = d * k)) \/ (bit = 0 /\ ~(exists k. S n = d * k))) -> z = q + bit

Structural proof guide

A divisibility bit is exactly the successor quotient increment.

Direct prerequisites: division_remainder_successor_cases, add_eq_zero_right, succ_ne_zero, multiple_has_zero_remainder, division_remainder_unique, zero_remainder_implies_multiple. The authored body proceeds by case analysis (22), intermediate claims (6), equality transport (9).

Proof neighborhood

Direct dependencies

BT00SG division_remainder_successor_cases BT000L add_eq_zero_right BT000C succ_ne_zero BT001W multiple_has_zero_remainder BT001U division_remainder_unique BT001V zero_remainder_implies_multiple

Direct dependents

BT00SK power_quotient_successor_pointwise_add

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 z
  6. 0006intro s
  7. 0007intro bit
  8. 0008intro hold
  9. 0009intro hnew
  10. 0010intro hbit
  11. 0011have hcases : ((S r = d /\ (z = S q /\ s = 0)) \/ ((exists blsr_lt_gap_quotient_bit_cases_no_carry. blsr_lt_gap_quotient_bit_cases_no_carry + S (S r) = (d)) /\ (z = q /\ s = S r)))
  12. 0012specialize division_remainder_successor_cases d
  13. 0013specialize division_remainder_successor_cases n
  14. 0014specialize division_remainder_successor_cases q
  15. 0015specialize division_remainder_successor_cases r
  16. 0016specialize division_remainder_successor_cases z
  17. 0017specialize division_remainder_successor_cases s
  18. 0018apply division_remainder_successor_cases
  19. 0019exact hold
  20. 0020exact hnew
  21. 0021cases hbit
  22. 0022cases hbit_left
  23. 0023cases hcases
  24. 0024cases hcases_left
  25. 0025cases hcases_left_right
  26. 0026rewrite hbit_left_left
  27. 0027rewrite hcases_left_right_left
  28. 0028rewrite PA4
  29. 0029rewrite PA3
  30. 0030refl
  31. 0031cases hcases_right
  32. 0032cases hcases_right_right
  33. 0033have hd0 : ~(d = 0)
  34. 0034intro hd
  35. 0035cases hold
  36. 0036cases hold_right
  37. 0037rewrite hd at hold_right_witness
  38. 0038have hsr0 : S r = 0
  39. 0039specialize add_eq_zero_right x
  40. 0040specialize add_eq_zero_right (S r)
  41. 0041apply add_eq_zero_right
  42. 0042exact hold_right_witness
  43. 0043specialize succ_ne_zero r
  44. 0044apply succ_ne_zero
  45. 0045exact hsr0
  46. 0046have hzero : exists q0 r0. ((S n = d * q0 + r0 /\ r0 = 0) /\ exists gap. gap + S r0 = d)
  47. 0047specialize multiple_has_zero_remainder d
  48. 0048specialize multiple_has_zero_remainder (S n)
  49. 0049apply multiple_has_zero_remainder
  50. 0050exact hd0
  51. 0051exact hbit_left_right
  52. 0052cases hzero
  53. 0053cases hzero_witness
  54. 0054cases hzero_witness_witness
  55. 0055cases hzero_witness_witness_left
  56. 0056have hunique : z = x /\ s = x1
  57. 0057cases hnew
  58. 0058specialize division_remainder_unique d
  59. 0059specialize division_remainder_unique (S n)
  60. 0060specialize division_remainder_unique z
  61. 0061specialize division_remainder_unique s
  62. 0062specialize division_remainder_unique x
  63. 0063specialize division_remainder_unique x1
  64. 0064apply division_remainder_unique
  65. 0065exact hnew_left
  66. 0066exact hnew_right
  67. 0067exact hzero_witness_witness_left_left
  68. 0068exact hzero_witness_witness_right
  69. 0069cases hunique
  70. 0070have hs0 : s = 0
  71. 0071trans x1
  72. 0072exact hunique_right
  73. 0073exact hzero_witness_witness_left_right
  74. 0074exfalso
  75. 0075specialize succ_ne_zero r
  76. 0076apply succ_ne_zero
  77. 0077trans s
  78. 0078symm
  79. 0079exact hcases_right_right_right
  80. 0080exact hs0
  81. 0081cases hbit_right
  82. 0082cases hcases
  83. 0083cases hcases_left
  84. 0084cases hcases_left_right
  85. 0085exfalso
  86. 0086apply hbit_right_right
  87. 0087cases hnew
  88. 0088rewrite hcases_left_right_right at hnew_left
  89. 0089specialize zero_remainder_implies_multiple d
  90. 0090specialize zero_remainder_implies_multiple (S n)
  91. 0091specialize zero_remainder_implies_multiple z
  92. 0092apply zero_remainder_implies_multiple
  93. 0093exact hnew_left
  94. 0094cases hcases_right
  95. 0095cases hcases_right_right
  96. 0096rewrite hbit_right_left
  97. 0097rewrite hcases_right_right_left
  98. 0098rewrite PA3
  99. 0099refl