BT00TA

beta_pascal_row_step_pointwise_functional

Alpha body-checked · checked-use disabled

Pascal successor rows preserve pointwise agreement across encodings.

Exact expanded PA statement

forall pb pc qb qc b c d e w v. (forall bcf_index_bpspf_left. (exists bcf_lt_gap_bpspf_left_bound. bcf_lt_gap_bpspf_left_bound + S (bcf_index_bpspf_left) = w) -> exists bcf_value_bpspf_left. ((((exists bcf_height_bpspf_left_entry. bcf_height_bpspf_left_entry + S (bcf_value_bpspf_left) = S ((S (bcf_index_bpspf_left)) * c)) /\ exists bcf_quotient_bpspf_left_entry. b = bcf_quotient_bpspf_left_entry * S ((S (bcf_index_bpspf_left)) * c) + (bcf_value_bpspf_left))) /\ ((bcf_index_bpspf_left = 0 /\ bcf_value_bpspf_left = 1) \/ exists bcf_predecessor_bpspf_left bcf_left_bpspf_left bcf_right_bpspf_left. bcf_index_bpspf_left = S bcf_predecessor_bpspf_left /\ ((((exists bcf_height_bpspf_left_previous_left. bcf_height_bpspf_left_previous_left + S (bcf_left_bpspf_left) = S ((S (bcf_predecessor_bpspf_left)) * pc)) /\ exists bcf_quotient_bpspf_left_previous_left. pb = bcf_quotient_bpspf_left_previous_left * S ((S (bcf_predecessor_bpspf_left)) * pc) + (bcf_left_bpspf_left))) /\ ((((exists bcf_height_bpspf_left_previous_right. bcf_height_bpspf_left_previous_right + S (bcf_right_bpspf_left) = S ((S (S (bcf_predecessor_bpspf_left))) * pc)) /\ exists bcf_quotient_bpspf_left_previous_right. pb = bcf_quotient_bpspf_left_previous_right * S ((S (S (bcf_predecessor_bpspf_left))) * pc) + (bcf_right_bpspf_left))) /\ bcf_value_bpspf_left = bcf_left_bpspf_left + bcf_right_bpspf_left))))) -> (forall bcf_index_bpspf_right. (exists bcf_lt_gap_bpspf_right_bound. bcf_lt_gap_bpspf_right_bound + S (bcf_index_bpspf_right) = v) -> exists bcf_value_bpspf_right. ((((exists bcf_height_bpspf_right_entry. bcf_height_bpspf_right_entry + S (bcf_value_bpspf_right) = S ((S (bcf_index_bpspf_right)) * e)) /\ exists bcf_quotient_bpspf_right_entry. d = bcf_quotient_bpspf_right_entry * S ((S (bcf_index_bpspf_right)) * e) + (bcf_value_bpspf_right))) /\ ((bcf_index_bpspf_right = 0 /\ bcf_value_bpspf_right = 1) \/ exists bcf_predecessor_bpspf_right bcf_left_bpspf_right bcf_right_bpspf_right. bcf_index_bpspf_right = S bcf_predecessor_bpspf_right /\ ((((exists bcf_height_bpspf_right_previous_left. bcf_height_bpspf_right_previous_left + S (bcf_left_bpspf_right) = S ((S (bcf_predecessor_bpspf_right)) * qc)) /\ exists bcf_quotient_bpspf_right_previous_left. qb = bcf_quotient_bpspf_right_previous_left * S ((S (bcf_predecessor_bpspf_right)) * qc) + (bcf_left_bpspf_right))) /\ ((((exists bcf_height_bpspf_right_previous_right. bcf_height_bpspf_right_previous_right + S (bcf_right_bpspf_right) = S ((S (S (bcf_predecessor_bpspf_right))) * qc)) /\ exists bcf_quotient_bpspf_right_previous_right. qb = bcf_quotient_bpspf_right_previous_right * S ((S (S (bcf_predecessor_bpspf_right))) * qc) + (bcf_right_bpspf_right))) /\ bcf_value_bpspf_right = bcf_left_bpspf_right + bcf_right_bpspf_right))))) -> (forall i x y. (exists bcf_lt_gap_bpspf_previous_left_bound. bcf_lt_gap_bpspf_previous_left_bound + S (i) = w) -> (exists bcf_lt_gap_bpspf_previous_right_bound. bcf_lt_gap_bpspf_previous_right_bound + S (i) = v) -> (((exists bcf_height_bpspf_previous_left_at. bcf_height_bpspf_previous_left_at + S (x) = S ((S (i)) * pc)) /\ exists bcf_quotient_bpspf_previous_left_at. pb = bcf_quotient_bpspf_previous_left_at * S ((S (i)) * pc) + (x))) -> (((exists bcf_height_bpspf_previous_right_at. bcf_height_bpspf_previous_right_at + S (y) = S ((S (i)) * qc)) /\ exists bcf_quotient_bpspf_previous_right_at. qb = bcf_quotient_bpspf_previous_right_at * S ((S (i)) * qc) + (y))) -> x = y) -> (forall i x y. (exists bcf_lt_gap_bpspf_current_left_bound. bcf_lt_gap_bpspf_current_left_bound + S (i) = w) -> (exists bcf_lt_gap_bpspf_current_right_bound. bcf_lt_gap_bpspf_current_right_bound + S (i) = v) -> (((exists bcf_height_bpspf_current_left_at. bcf_height_bpspf_current_left_at + S (x) = S ((S (i)) * c)) /\ exists bcf_quotient_bpspf_current_left_at. b = bcf_quotient_bpspf_current_left_at * S ((S (i)) * c) + (x))) -> (((exists bcf_height_bpspf_current_right_at. bcf_height_bpspf_current_right_at + S (y) = S ((S (i)) * e)) /\ exists bcf_quotient_bpspf_current_right_at. d = bcf_quotient_bpspf_current_right_at * S ((S (i)) * e) + (y))) -> x = y)

Structural proof guide

Pascal successor rows preserve pointwise agreement across encodings.

Direct prerequisites: beta_at_unique, succ_ne_zero, succ_injective, lt_to_le. The authored body proceeds by case analysis (26), intermediate claims (16), equality transport (6).

Proof neighborhood

Direct dependencies

BT0042 beta_at_unique BT000C succ_ne_zero BT000D succ_injective BT0019 lt_to_le

Direct dependents

BT00TB beta_pascal_table_row_pointwise_functional

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  1. 0001intro pb
  2. 0002intro pc
  3. 0003intro qb
  4. 0004intro qc
  5. 0005intro b
  6. 0006intro c
  7. 0007intro d
  8. 0008intro e
  9. 0009intro w
  10. 0010intro v
  11. 0011intro hleft
  12. 0012intro hright
  13. 0013intro hagree
  14. 0014intro i
  15. 0015intro x
  16. 0016intro y
  17. 0017intro hiw
  18. 0018intro hiv
  19. 0019intro hxi
  20. 0020intro hyi
  21. 0021have hleft_value : exists bcf_cell_value_bpspf_left_cell. ((((exists bcf_height_bpspf_left_cell_entry. bcf_height_bpspf_left_cell_entry + S (bcf_cell_value_bpspf_left_cell) = S ((S (i)) * c)) /\ exists bcf_quotient_bpspf_left_cell_entry. b = bcf_quotient_bpspf_left_cell_entry * S ((S (i)) * c) + (bcf_cell_value_bpspf_left_cell))) /\ ((i = 0 /\ bcf_cell_value_bpspf_left_cell = 1) \/ exists bcf_cell_predecessor_bpspf_left_cell bcf_cell_left_bpspf_left_cell bcf_cell_right_bpspf_left_cell. i = S bcf_cell_predecessor_bpspf_left_cell /\ ((((exists bcf_height_bpspf_left_cell_previous_left. bcf_height_bpspf_left_cell_previous_left + S (bcf_cell_left_bpspf_left_cell) = S ((S (bcf_cell_predecessor_bpspf_left_cell)) * pc)) /\ exists bcf_quotient_bpspf_left_cell_previous_left. pb = bcf_quotient_bpspf_left_cell_previous_left * S ((S (bcf_cell_predecessor_bpspf_left_cell)) * pc) + (bcf_cell_left_bpspf_left_cell))) /\ ((((exists bcf_height_bpspf_left_cell_previous_right. bcf_height_bpspf_left_cell_previous_right + S (bcf_cell_right_bpspf_left_cell) = S ((S (S (bcf_cell_predecessor_bpspf_left_cell))) * pc)) /\ exists bcf_quotient_bpspf_left_cell_previous_right. pb = bcf_quotient_bpspf_left_cell_previous_right * S ((S (S (bcf_cell_predecessor_bpspf_left_cell))) * pc) + (bcf_cell_right_bpspf_left_cell))) /\ bcf_cell_value_bpspf_left_cell = bcf_cell_left_bpspf_left_cell + bcf_cell_right_bpspf_left_cell))))
  22. 0022specialize hleft i
  23. 0023apply hleft
  24. 0024exact hiw
  25. 0025cases hleft_value
  26. 0026cases hleft_value_witness
  27. 0027have hright_value : exists bcf_cell_value_bpspf_right_cell. ((((exists bcf_height_bpspf_right_cell_entry. bcf_height_bpspf_right_cell_entry + S (bcf_cell_value_bpspf_right_cell) = S ((S (i)) * e)) /\ exists bcf_quotient_bpspf_right_cell_entry. d = bcf_quotient_bpspf_right_cell_entry * S ((S (i)) * e) + (bcf_cell_value_bpspf_right_cell))) /\ ((i = 0 /\ bcf_cell_value_bpspf_right_cell = 1) \/ exists bcf_cell_predecessor_bpspf_right_cell bcf_cell_left_bpspf_right_cell bcf_cell_right_bpspf_right_cell. i = S bcf_cell_predecessor_bpspf_right_cell /\ ((((exists bcf_height_bpspf_right_cell_previous_left. bcf_height_bpspf_right_cell_previous_left + S (bcf_cell_left_bpspf_right_cell) = S ((S (bcf_cell_predecessor_bpspf_right_cell)) * qc)) /\ exists bcf_quotient_bpspf_right_cell_previous_left. qb = bcf_quotient_bpspf_right_cell_previous_left * S ((S (bcf_cell_predecessor_bpspf_right_cell)) * qc) + (bcf_cell_left_bpspf_right_cell))) /\ ((((exists bcf_height_bpspf_right_cell_previous_right. bcf_height_bpspf_right_cell_previous_right + S (bcf_cell_right_bpspf_right_cell) = S ((S (S (bcf_cell_predecessor_bpspf_right_cell))) * qc)) /\ exists bcf_quotient_bpspf_right_cell_previous_right. qb = bcf_quotient_bpspf_right_cell_previous_right * S ((S (S (bcf_cell_predecessor_bpspf_right_cell))) * qc) + (bcf_cell_right_bpspf_right_cell))) /\ bcf_cell_value_bpspf_right_cell = bcf_cell_left_bpspf_right_cell + bcf_cell_right_bpspf_right_cell))))
  28. 0028specialize hright i
  29. 0029apply hright
  30. 0030exact hiv
  31. 0031cases hright_value
  32. 0032cases hright_value_witness
  33. 0033have hx_value : x = x1
  34. 0034specialize beta_at_unique b
  35. 0035specialize beta_at_unique c
  36. 0036specialize beta_at_unique i
  37. 0037specialize beta_at_unique x
  38. 0038specialize beta_at_unique x1
  39. 0039apply beta_at_unique
  40. 0040exact hxi
  41. 0041exact hleft_value_witness_left
  42. 0042have hy_value : y = x2
  43. 0043specialize beta_at_unique d
  44. 0044specialize beta_at_unique e
  45. 0045specialize beta_at_unique i
  46. 0046specialize beta_at_unique y
  47. 0047specialize beta_at_unique x2
  48. 0048apply beta_at_unique
  49. 0049exact hyi
  50. 0050exact hright_value_witness_left
  51. 0051cases hleft_value_witness_right
  52. 0052cases hleft_value_witness_right_left
  53. 0053cases hright_value_witness_right
  54. 0054cases hright_value_witness_right_left
  55. 0055trans x1
  56. 0056exact hx_value
  57. 0057trans 1
  58. 0058exact hleft_value_witness_right_left_right
  59. 0059trans x2
  60. 0060symm
  61. 0061exact hright_value_witness_right_left_right
  62. 0062symm
  63. 0063exact hy_value
  64. 0064cases hright_value_witness_right_right
  65. 0065cases hright_value_witness_right_right_witness
  66. 0066cases hright_value_witness_right_right_witness_witness
  67. 0067cases hright_value_witness_right_right_witness_witness_witness
  68. 0068exfalso
  69. 0069have hbad : S x3 = 0
  70. 0070trans i
  71. 0071symm
  72. 0072exact hright_value_witness_right_right_witness_witness_witness_left
  73. 0073exact hleft_value_witness_right_left_left
  74. 0074specialize succ_ne_zero x3
  75. 0075apply succ_ne_zero
  76. 0076exact hbad
  77. 0077cases hleft_value_witness_right_right
  78. 0078cases hleft_value_witness_right_right_witness
  79. 0079cases hleft_value_witness_right_right_witness_witness
  80. 0080cases hleft_value_witness_right_right_witness_witness_witness
  81. 0081cases hleft_value_witness_right_right_witness_witness_witness_right
  82. 0082cases hleft_value_witness_right_right_witness_witness_witness_right_right
  83. 0083cases hright_value_witness_right
  84. 0084cases hright_value_witness_right_left
  85. 0085exfalso
  86. 0086have hbad : S x3 = 0
  87. 0087trans i
  88. 0088symm
  89. 0089exact hleft_value_witness_right_right_witness_witness_witness_left
  90. 0090exact hright_value_witness_right_left_left
  91. 0091specialize succ_ne_zero x3
  92. 0092apply succ_ne_zero
  93. 0093exact hbad
  94. 0094cases hright_value_witness_right_right
  95. 0095cases hright_value_witness_right_right_witness
  96. 0096cases hright_value_witness_right_right_witness_witness
  97. 0097cases hright_value_witness_right_right_witness_witness_witness
  98. 0098cases hright_value_witness_right_right_witness_witness_witness_right
  99. 0099cases hright_value_witness_right_right_witness_witness_witness_right_right
  100. 0100have hsucc : S x3 = S x6
  101. 0101trans i
  102. 0102symm
  103. 0103exact hleft_value_witness_right_right_witness_witness_witness_left
  104. 0104exact hright_value_witness_right_right_witness_witness_witness_left
  105. 0105have hpred : x3 = x6
  106. 0106specialize succ_injective x3
  107. 0107specialize succ_injective x6
  108. 0108apply succ_injective
  109. 0109exact hsucc
  110. 0110have hcurrent_w : exists bcf_lt_gap_bpspf_current_w. bcf_lt_gap_bpspf_current_w + S (S x3) = w
  111. 0111rewrite <- hleft_value_witness_right_right_witness_witness_witness_left
  112. 0112exact hiw
  113. 0113have hcurrent_v : exists bcf_lt_gap_bpspf_current_v. bcf_lt_gap_bpspf_current_v + S (S x3) = v
  114. 0114rewrite <- hleft_value_witness_right_right_witness_witness_witness_left
  115. 0115exact hiv
  116. 0116have hprevious_w : exists bcf_lt_gap_bpspf_previous_w. bcf_lt_gap_bpspf_previous_w + S (x3) = w
  117. 0117specialize lt_to_le (S x3)
  118. 0118specialize lt_to_le w
  119. 0119apply lt_to_le
  120. 0120exact hcurrent_w
  121. 0121have hprevious_v : exists bcf_lt_gap_bpspf_previous_v. bcf_lt_gap_bpspf_previous_v + S (x3) = v
  122. 0122specialize lt_to_le (S x3)
  123. 0123specialize lt_to_le v
  124. 0124apply lt_to_le
  125. 0125exact hcurrent_v
  126. 0126have hright_previous : ((exists bcf_height_bpspf_aligned_previous. bcf_height_bpspf_aligned_previous + S (x7) = S ((S (x3)) * qc)) /\ exists bcf_quotient_bpspf_aligned_previous. qb = bcf_quotient_bpspf_aligned_previous * S ((S (x3)) * qc) + (x7))
  127. 0127rewrite hpred
  128. 0128rewrite hpred
  129. 0129exact hright_value_witness_right_right_witness_witness_witness_right_left
  130. 0130have hright_current : ((exists bcf_height_bpspf_aligned_current. bcf_height_bpspf_aligned_current + S (x8) = S ((S (S x3)) * qc)) /\ exists bcf_quotient_bpspf_aligned_current. qb = bcf_quotient_bpspf_aligned_current * S ((S (S x3)) * qc) + (x8))
  131. 0131rewrite hpred
  132. 0132rewrite hpred
  133. 0133exact hright_value_witness_right_right_witness_witness_witness_right_right_left
  134. 0134have hu : x4 = x7
  135. 0135specialize hagree x3
  136. 0136specialize hagree x4
  137. 0137specialize hagree x7
  138. 0138apply hagree
  139. 0139exact hprevious_w
  140. 0140exact hprevious_v
  141. 0141exact hleft_value_witness_right_right_witness_witness_witness_right_left
  142. 0142exact hright_previous
  143. 0143have hv : x5 = x8
  144. 0144specialize hagree (S x3)
  145. 0145specialize hagree x5
  146. 0146specialize hagree x8
  147. 0147apply hagree
  148. 0148exact hcurrent_w
  149. 0149exact hcurrent_v
  150. 0150exact hleft_value_witness_right_right_witness_witness_witness_right_right_left
  151. 0151exact hright_current
  152. 0152trans x1
  153. 0153exact hx_value
  154. 0154trans x4 + x5
  155. 0155exact hleft_value_witness_right_right_witness_witness_witness_right_right_right
  156. 0156trans x7 + x8
  157. 0157congr
  158. 0158exact hu
  159. 0159exact hv
  160. 0160trans x2
  161. 0161symm
  162. 0162exact hright_value_witness_right_right_witness_witness_witness_right_right_right
  163. 0163symm
  164. 0164exact hy_value