PA002G

beta_exclusive_recode_congruence_step

Stable checked-use theorem · independently closed

Add the next source value to a target-base CRT code for an exclusive prefix.

Exact expanded PA statement

forall N c b e k P z. (exists h. h + S k = N) -> ~(P = 0) -> (forall i. (exists h. h + S i = k) -> exists q. P = S ((S i) * c) * q) -> (forall i a. (exists h. h + S i = k) -> ((exists h. h + S a = S ((S i) * e)) /\ exists q. b = q * S ((S i) * e) + a) -> exists u v. z + S ((S i) * c) * u = a + S ((S i) * c) * v) -> (forall j. (exists g. g + k = j) -> (exists h. h + j = N) -> forall d. (exists u. P = d * u) -> (exists v. S ((S j) * c) = d * v) -> d = 1) -> exists z2. forall i a. (exists h. h + S i = S k) -> ((exists h. h + S a = S ((S i) * e)) /\ exists q. b = q * S ((S i) * e) + a) -> exists u v. z2 + S ((S i) * c) * u = a + S ((S i) * c) * v

Structural proof guide

Generated structural guide

Add the next source value to a target-base CRT code for an exclusive prefix.

Use the direct prerequisites beta_modulus_nonzero, le_refl, lt_to_le, binary_crt_fold_step, beta_at_exists, beta_at_unique, le_of_succ_le_succ, le_eq_or_lt as previously established PA formulas.

The proof proceeds by case analysis (4), intermediate claims (11), equality transport (5).

Referenced ingredients

PA000U beta_modulus_nonzero PA001A le_refl PA000X lt_to_le PA0028 binary_crt_fold_step PA0029 beta_at_exists PA002F beta_at_unique PA000V le_of_succ_le_succ PA000W le_eq_or_lt

Proof neighborhood

Direct dependencies

PA000U beta_modulus_nonzero PA001A le_refl PA000X lt_to_le PA0028 binary_crt_fold_step PA0029 beta_at_exists PA002F beta_at_unique PA000V le_of_succ_le_succ PA000W le_eq_or_lt

Direct dependents

PA002H beta_exclusive_recode_invariant_step

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 N
  2. 0002intro c
  3. 0003intro b
  4. 0004intro e
  5. 0005intro k
  6. 0006intro P
  7. 0007intro z
  8. 0008intro hkN
  9. 0009intro hP
  10. 0010intro hdiv
  11. 0011intro hcong
  12. 0012intro hfuture
  13. 0013have hnew : ~(S ((S k) * c) = 0)
  14. 0014specialize beta_modulus_nonzero c
  15. 0015specialize beta_modulus_nonzero k
  16. 0016exact beta_modulus_nonzero
  17. 0017have hkbound : exists h. h + k = N
  18. 0018specialize lt_to_le k
  19. 0019specialize lt_to_le N
  20. 0020apply lt_to_le
  21. 0021exact hkN
  22. 0022have hcop : forall d. (exists u. P = d * u) -> (exists v. S ((S k) * c) = d * v) -> d = 1
  23. 0023specialize hfuture k
  24. 0024apply hfuture
  25. 0025specialize le_refl k
  26. 0026exact le_refl
  27. 0027exact hkbound
  28. 0028have hvalue : exists a. ((exists h. h + S a = S ((S k) * e)) /\ exists q. b = q * S ((S k) * e) + a)
  29. 0029specialize beta_at_exists b
  30. 0030specialize beta_at_exists e
  31. 0031specialize beta_at_exists k
  32. 0032exact beta_at_exists
  33. 0033cases hvalue
  34. 0034have hfold : exists z2. ((forall m a. (exists q. P = m * q) -> (exists u v. z + m * u = a + m * v) -> exists r s. z2 + m * r = a + m * s) /\ exists q r. z2 + S ((S k) * c) * q = x + S ((S k) * c) * r)
  35. 0035specialize binary_crt_fold_step P
  36. 0036specialize binary_crt_fold_step (S ((S k) * c))
  37. 0037specialize binary_crt_fold_step z
  38. 0038specialize binary_crt_fold_step x
  39. 0039apply binary_crt_fold_step
  40. 0040exact hP
  41. 0041exact hnew
  42. 0042exact hcop
  43. 0043cases hfold
  44. 0044cases hfold_witness
  45. 0045exists x1
  46. 0046intro i
  47. 0047intro a
  48. 0048intro hi
  49. 0049intro hati
  50. 0050have hik : exists r. r + i = k
  51. 0051specialize le_of_succ_le_succ i
  52. 0052specialize le_of_succ_le_succ k
  53. 0053apply le_of_succ_le_succ
  54. 0054exact hi
  55. 0055have hsplit : i = k \/ exists r. r + S i = k
  56. 0056specialize le_eq_or_lt i
  57. 0057specialize le_eq_or_lt k
  58. 0058apply le_eq_or_lt
  59. 0059exact hik
  60. 0060cases hsplit
  61. 0061have hati_new : ((exists h. h + S a = S ((S k) * e)) /\ exists q. b = q * S ((S k) * e) + a)
  62. 0062rewrite <- hsplit_left
  63. 0063rewrite <- hsplit_left
  64. 0064exact hati
  65. 0065have haeq : a = x
  66. 0066specialize beta_at_unique b
  67. 0067specialize beta_at_unique e
  68. 0068specialize beta_at_unique k
  69. 0069specialize beta_at_unique a
  70. 0070specialize beta_at_unique x
  71. 0071apply beta_at_unique
  72. 0072exact hati_new
  73. 0073exact hvalue_witness
  74. 0074rewrite hsplit_left
  75. 0075rewrite hsplit_left
  76. 0076rewrite haeq
  77. 0077exact hfold_witness_right
  78. 0078have hmiP : exists q. P = S ((S i) * c) * q
  79. 0079specialize hdiv i
  80. 0080apply hdiv
  81. 0081exact hsplit_right
  82. 0082have hzold : exists u v. z + S ((S i) * c) * u = a + S ((S i) * c) * v
  83. 0083specialize hcong i
  84. 0084specialize hcong a
  85. 0085apply hcong
  86. 0086exact hsplit_right
  87. 0087exact hati
  88. 0088specialize hfold_witness_left (S ((S i) * c))
  89. 0089specialize hfold_witness_left a
  90. 0090apply hfold_witness_left
  91. 0091exact hmiP
  92. 0092exact hzold