PA005J

mod_eq_decidable_from_remainders

Stable checked-use theorem · independently closed

Canonical bounded remainders constructively decide congruence.

Exact expanded PA statement

forall p a b qa ra qb rb. a = qa * p + ra -> (exists ha. ha + S ra = p) -> b = qb * p + rb -> (exists hb. hb + S rb = p) -> (exists u v. a + p * u = b + p * v) \/ ~(exists u v. a + p * u = b + p * v)

Structural proof guide

Generated structural guide

Canonical bounded remainders constructively decide congruence.

Use the direct prerequisites eq_decidable, remainder_decomposition_to_mod_eq, mod_eq_symm, mod_eq_trans, mod_eq_bounded_unique as previously established PA formulas.

The proof proceeds by case analysis (1), intermediate claims (8), equality transport (1).

Referenced ingredients

PA004G eq_decidable PA003C remainder_decomposition_to_mod_eq PA003L mod_eq_symm PA0024 mod_eq_trans PA002U mod_eq_bounded_unique

Proof neighborhood

Direct dependencies

PA004G eq_decidable PA003C remainder_decomposition_to_mod_eq PA003L mod_eq_symm PA0024 mod_eq_trans PA002U mod_eq_bounded_unique

Direct dependents

PA005K mod_eq_decidable_nonzero

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. 0001intro p
  2. 0002intro a
  3. 0003intro b
  4. 0004intro qa
  5. 0005intro ra
  6. 0006intro qb
  7. 0007intro rb
  8. 0008intro ha
  9. 0009intro hra
  10. 0010intro hb
  11. 0011intro hrb
  12. 0012specialize eq_decidable ra
  13. 0013specialize eq_decidable rb
  14. 0014cases eq_decidable
  15. 0015left
  16. 0016have har : exists u v. a + p * u = ra + p * v
  17. 0017specialize remainder_decomposition_to_mod_eq p
  18. 0018specialize remainder_decomposition_to_mod_eq a
  19. 0019specialize remainder_decomposition_to_mod_eq qa
  20. 0020specialize remainder_decomposition_to_mod_eq ra
  21. 0021apply remainder_decomposition_to_mod_eq
  22. 0022exact ha
  23. 0023have hbr : exists u v. b + p * u = rb + p * v
  24. 0024specialize remainder_decomposition_to_mod_eq p
  25. 0025specialize remainder_decomposition_to_mod_eq b
  26. 0026specialize remainder_decomposition_to_mod_eq qb
  27. 0027specialize remainder_decomposition_to_mod_eq rb
  28. 0028apply remainder_decomposition_to_mod_eq
  29. 0029exact hb
  30. 0030have hbra : exists u v. b + p * u = ra + p * v
  31. 0031rewrite eq_decidable_left
  32. 0032exact hbr
  33. 0033have hrab : exists u v. ra + p * u = b + p * v
  34. 0034specialize mod_eq_symm p
  35. 0035specialize mod_eq_symm b
  36. 0036specialize mod_eq_symm ra
  37. 0037apply mod_eq_symm
  38. 0038exact hbra
  39. 0039specialize mod_eq_trans p
  40. 0040specialize mod_eq_trans a
  41. 0041specialize mod_eq_trans ra
  42. 0042specialize mod_eq_trans b
  43. 0043apply mod_eq_trans
  44. 0044exact har
  45. 0045exact hrab
  46. 0046right
  47. 0047intro hab
  48. 0048apply eq_decidable_right
  49. 0049specialize mod_eq_bounded_unique p
  50. 0050specialize mod_eq_bounded_unique ra
  51. 0051specialize mod_eq_bounded_unique rb
  52. 0052apply mod_eq_bounded_unique
  53. 0053exact hra
  54. 0054exact hrb
  55. 0055have har : exists u v. a + p * u = ra + p * v
  56. 0056specialize remainder_decomposition_to_mod_eq p
  57. 0057specialize remainder_decomposition_to_mod_eq a
  58. 0058specialize remainder_decomposition_to_mod_eq qa
  59. 0059specialize remainder_decomposition_to_mod_eq ra
  60. 0060apply remainder_decomposition_to_mod_eq
  61. 0061exact ha
  62. 0062have hra_a : exists u v. ra + p * u = a + p * v
  63. 0063specialize mod_eq_symm p
  64. 0064specialize mod_eq_symm a
  65. 0065specialize mod_eq_symm ra
  66. 0066apply mod_eq_symm
  67. 0067exact har
  68. 0068have hra_b : exists u v. ra + p * u = b + p * v
  69. 0069specialize mod_eq_trans p
  70. 0070specialize mod_eq_trans ra
  71. 0071specialize mod_eq_trans a
  72. 0072specialize mod_eq_trans b
  73. 0073apply mod_eq_trans
  74. 0074exact hra_a
  75. 0075exact hab
  76. 0076have hbr : exists u v. b + p * u = rb + p * v
  77. 0077specialize remainder_decomposition_to_mod_eq p
  78. 0078specialize remainder_decomposition_to_mod_eq b
  79. 0079specialize remainder_decomposition_to_mod_eq qb
  80. 0080specialize remainder_decomposition_to_mod_eq rb
  81. 0081apply remainder_decomposition_to_mod_eq
  82. 0082exact hb
  83. 0083specialize mod_eq_trans p
  84. 0084specialize mod_eq_trans ra
  85. 0085specialize mod_eq_trans b
  86. 0086specialize mod_eq_trans rb
  87. 0087apply mod_eq_trans
  88. 0088exact hra_b
  89. 0089exact hbr