PA005J · theorem

mod_eq_decidable_from_remainders

Stable checked-use theorem · independently closed

Canonical bounded remainders constructively decide congruence.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Statement with defined notation

∀ p. ∀ a. ∀ b. ∀ qa. ∀ ra. ∀ qb. ∀ rb. a = qa · p + ra → Lt(ra,p) → b = qb · p + rb → Lt(rb,p) → ModEq(p,a,b) ∨ ¬ModEq(p,a,b)

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0002 Lt PD0008 ModEq

4 occurrences

In local proof propositions

PD0008 ModEq

8 occurrences

Exact expanded native-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)

Proof neighborhood

Direct theorem prerequisites

PA004G eq_decidable PA003C remainder_decomposition_to_mod_eq PA003L mod_eq_symm PA0024 mod_eq_trans PA002U mod_eq_bounded_unique

Direct theorem dependents

PA005K mod_eq_decidable_nonzero

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

Read the argument

Proof checkpoints

89 script commands · 17 reading checkpoints · 8 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (5)
eq decidableremainder decomposition to mod eqmod eq symmmod eq transmod eq bounded unique
01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro p
  2. L2
    intro a
  3. L3
    intro b
  4. L4
    intro qa
  5. L5
    intro ra
  6. L6
    intro qb
  7. L7
    intro rb
  8. L8
    intro ha
  9. L9
    intro hra
  10. L10
    intro hb
02Fix variables and assumptionsL11–11

Work with arbitrary variables or the premises of the current implication.

  1. L11
    intro hrb
03Use earlier factsL12–13

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L12
    specialize eq_decidable ra
  2. L13
    specialize eq_decidable rb
04Separate the logical casesL14–15

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L14
    cases eq_decidable
  2. L15
    left
05Establish harL16–22

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply remainder decomposition to mod eq.

  1. L16
  2. L17
    specialize remainder_decomposition_to_mod_eq p
  3. L18
    specialize remainder_decomposition_to_mod_eq a
  4. L19
    specialize remainder_decomposition_to_mod_eq qa
  5. L20
    specialize remainder_decomposition_to_mod_eq ra
  6. L21
    apply remainder_decomposition_to_mod_eq
  7. L22
    exact ha
06Establish hbrL23–29

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply remainder decomposition to mod eq.

  1. L23
  2. L24
    specialize remainder_decomposition_to_mod_eq p
  3. L25
    specialize remainder_decomposition_to_mod_eq b
  4. L26
    specialize remainder_decomposition_to_mod_eq qb
  5. L27
    specialize remainder_decomposition_to_mod_eq rb
  6. L28
    apply remainder_decomposition_to_mod_eq
  7. L29
    exact hb
07Establish hbraL30–32

Establish this local claim before using it. It is not an additional assumption.

  1. L30
    have hbra : ModEq(p,b,ra)Definitions: ModEq(p,b,ra)Original native command in the exact edition
  2. L31
    rewrite eq_decidable_left
  3. L32
    exact hbr
08Establish hrabL33–42

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq symm.

  1. L33
    have hrab : ModEq(p,ra,b)Definitions: ModEq(p,ra,b)Original native command in the exact edition
  2. L34
    specialize mod_eq_symm p
  3. L35
    specialize mod_eq_symm b
  4. L36
    specialize mod_eq_symm ra
  5. L37
    apply mod_eq_symm
  6. L38
    exact hbra
  7. L39
    specialize mod_eq_trans p
  8. L40
    specialize mod_eq_trans a
  9. L41
    specialize mod_eq_trans ra
  10. L42
    specialize mod_eq_trans b
09Use earlier factsL43–45

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L43
    apply mod_eq_trans
  2. L44
    exact har
  3. L45
    exact hrab
10Separate the logical casesL46–46

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L46
    right
11Fix variables and assumptionsL47–47

Work with arbitrary variables or the premises of the current implication.

  1. L47
    intro hab
12Use earlier factsL48–54

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L48
    apply eq_decidable_right
  2. L49
    specialize mod_eq_bounded_unique p
  3. L50
    specialize mod_eq_bounded_unique ra
  4. L51
    specialize mod_eq_bounded_unique rb
  5. L52
    apply mod_eq_bounded_unique
  6. L53
    exact hra
  7. L54
    exact hrb
13Establish harL55–61

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply remainder decomposition to mod eq.

  1. L55
  2. L56
    specialize remainder_decomposition_to_mod_eq p
  3. L57
    specialize remainder_decomposition_to_mod_eq a
  4. L58
    specialize remainder_decomposition_to_mod_eq qa
  5. L59
    specialize remainder_decomposition_to_mod_eq ra
  6. L60
    apply remainder_decomposition_to_mod_eq
  7. L61
    exact ha
14Establish hra_aL62–67

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq symm.

  1. L62
    have hra_a : ModEq(p,ra,a)Definitions: ModEq(p,ra,a)Original native command in the exact edition
  2. L63
    specialize mod_eq_symm p
  3. L64
    specialize mod_eq_symm a
  4. L65
    specialize mod_eq_symm ra
  5. L66
    apply mod_eq_symm
  6. L67
    exact har
15Establish hra_bL68–75

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq trans.

  1. L68
    have hra_b : ModEq(p,ra,b)Definitions: ModEq(p,ra,b)Original native command in the exact edition
  2. L69
    specialize mod_eq_trans p
  3. L70
    specialize mod_eq_trans ra
  4. L71
    specialize mod_eq_trans a
  5. L72
    specialize mod_eq_trans b
  6. L73
    apply mod_eq_trans
  7. L74
    exact hra_a
  8. L75
    exact hab
16Establish hbrL76–85

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply remainder decomposition to mod eq.

  1. L76
  2. L77
    specialize remainder_decomposition_to_mod_eq p
  3. L78
    specialize remainder_decomposition_to_mod_eq b
  4. L79
    specialize remainder_decomposition_to_mod_eq qb
  5. L80
    specialize remainder_decomposition_to_mod_eq rb
  6. L81
    apply remainder_decomposition_to_mod_eq
  7. L82
    exact hb
  8. L83
    specialize mod_eq_trans p
  9. L84
    specialize mod_eq_trans ra
  10. L85
    specialize mod_eq_trans b
17Use earlier factsL86–89

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L86
    specialize mod_eq_trans rb
  2. L87
    apply mod_eq_trans
  3. L88
    exact hra_b
  4. L89
    exact hbr

Library-wide reading audit

Original defined command ledger · 89 lines
  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 : ModEq(p,a,ra)
    Exact native replay linehave 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 : ModEq(p,b,rb)
    Exact native replay linehave 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 : ModEq(p,b,ra)
    Exact native replay linehave hbra : exists u v. b + p * u = ra + p * v
  31. 0031rewrite eq_decidable_left
  32. 0032exact hbr
  33. 0033have hrab : ModEq(p,ra,b)
    Exact native replay linehave 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 : ModEq(p,a,ra)
    Exact native replay linehave 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 : ModEq(p,ra,a)
    Exact native replay linehave 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 : ModEq(p,ra,b)
    Exact native replay linehave 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 : ModEq(p,b,rb)
    Exact native replay linehave 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