BT00SG

division_remainder_successor_cases

Alpha body-checked · checked-use disabled

Successor division has exactly the carry and no-carry quotient cases.

Exact expanded PA statement

forall d n q r z s. (((n) = (d) * (q) + (r) /\ exists blsr_lt_gap_successor_cases_old_bound. blsr_lt_gap_successor_cases_old_bound + S (r) = (d))) -> (((S n) = (d) * (z) + (s) /\ exists blsr_lt_gap_successor_cases_new_bound. blsr_lt_gap_successor_cases_new_bound + S (s) = (d))) -> ((S r = d /\ (z = S q /\ s = 0)) \/ ((exists blsr_lt_gap_successor_cases_no_carry. blsr_lt_gap_successor_cases_no_carry + S (S r) = (d)) /\ (z = q /\ s = S r)))

Structural proof guide

Successor division has exactly the carry and no-carry quotient cases.

Direct prerequisites: le_eq_or_lt, division_remainder_unique. The authored body proceeds by case analysis (3), intermediate claims (6), equality transport (4).

Proof neighborhood

Direct dependencies

BT001C le_eq_or_lt BT001U division_remainder_unique

Direct dependents

BT00SH division_successor_quotient_by_bit

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 hold
  8. 0008intro hnew
  9. 0009cases hold
  10. 0010cases hnew
  11. 0011have hsplit : S r = d \/ exists blsr_lt_gap_successor_cases_no_carry. blsr_lt_gap_successor_cases_no_carry + S (S r) = (d)
  12. 0012specialize le_eq_or_lt (S r)
  13. 0013specialize le_eq_or_lt d
  14. 0014apply le_eq_or_lt
  15. 0015exact hold_right
  16. 0016cases hsplit
  17. 0017left
  18. 0018split
  19. 0019exact hsplit_left
  20. 0020have hequation : S n = d * S q + 0
  21. 0021trans S (d * q + r)
  22. 0022congr
  23. 0023exact hold_left
  24. 0024trans d * q + S r
  25. 0025symm
  26. 0026apply PA4
  27. 0027rewrite hsplit_left
  28. 0028rewrite PA3
  29. 0029symm
  30. 0030apply PA6
  31. 0031have hbound : exists blsr_lt_gap_successor_cases_carry_zero. blsr_lt_gap_successor_cases_carry_zero + S (0) = (d)
  32. 0032exists r
  33. 0033rewrite PA4
  34. 0034rewrite PA3
  35. 0035exact hsplit_left
  36. 0036have hunique : z = S q /\ s = 0
  37. 0037specialize division_remainder_unique d
  38. 0038specialize division_remainder_unique (S n)
  39. 0039specialize division_remainder_unique z
  40. 0040specialize division_remainder_unique s
  41. 0041specialize division_remainder_unique (S q)
  42. 0042specialize division_remainder_unique 0
  43. 0043apply division_remainder_unique
  44. 0044exact hnew_left
  45. 0045exact hnew_right
  46. 0046exact hequation
  47. 0047exact hbound
  48. 0048exact hunique
  49. 0049right
  50. 0050split
  51. 0051exact hsplit_right
  52. 0052have hequation : S n = d * q + S r
  53. 0053trans S (d * q + r)
  54. 0054congr
  55. 0055exact hold_left
  56. 0056symm
  57. 0057apply PA4
  58. 0058have hunique : z = q /\ s = S r
  59. 0059specialize division_remainder_unique d
  60. 0060specialize division_remainder_unique (S n)
  61. 0061specialize division_remainder_unique z
  62. 0062specialize division_remainder_unique s
  63. 0063specialize division_remainder_unique q
  64. 0064specialize division_remainder_unique (S r)
  65. 0065apply division_remainder_unique
  66. 0066exact hnew_left
  67. 0067exact hnew_right
  68. 0068exact hequation
  69. 0069exact hsplit_right
  70. 0070exact hunique