BT00Y1

bit_count_positive_last_one

Alpha body-checked · checked-use disabled

A positive bit count has a one at an index at least its count.

Exact expanded PA statement

forall b c l e. (((exists ff_u_b5ccbclo_count_sum ff_v_b5ccbclo_count_sum. ((((exists ff_h_b5ccbclo_count_sum_start. ff_h_b5ccbclo_count_sum_start + S (0) = S ((S (0)) * ff_v_b5ccbclo_count_sum)) /\ exists ff_q_b5ccbclo_count_sum_start. ff_u_b5ccbclo_count_sum = ff_q_b5ccbclo_count_sum_start * S ((S (0)) * ff_v_b5ccbclo_count_sum) + (0))) /\ ((((exists ff_h_b5ccbclo_count_sum_terminal. ff_h_b5ccbclo_count_sum_terminal + S ((S e)) = S ((S ((l))) * ff_v_b5ccbclo_count_sum)) /\ exists ff_q_b5ccbclo_count_sum_terminal. ff_u_b5ccbclo_count_sum = ff_q_b5ccbclo_count_sum_terminal * S ((S ((l))) * ff_v_b5ccbclo_count_sum) + ((S e)))) /\ forall ff_i_b5ccbclo_count_sum. (exists ff_lt_b5ccbclo_count_sum_bound. ff_lt_b5ccbclo_count_sum_bound + S ff_i_b5ccbclo_count_sum = (l)) -> exists ff_a_b5ccbclo_count_sum ff_r_b5ccbclo_count_sum ff_s_b5ccbclo_count_sum. ((((exists ff_h_b5ccbclo_count_sum_summand. ff_h_b5ccbclo_count_sum_summand + S (ff_a_b5ccbclo_count_sum) = S ((S (ff_i_b5ccbclo_count_sum)) * c)) /\ exists ff_q_b5ccbclo_count_sum_summand. b = ff_q_b5ccbclo_count_sum_summand * S ((S (ff_i_b5ccbclo_count_sum)) * c) + (ff_a_b5ccbclo_count_sum))) /\ ((((exists ff_h_b5ccbclo_count_sum_partial. ff_h_b5ccbclo_count_sum_partial + S (ff_r_b5ccbclo_count_sum) = S ((S (ff_i_b5ccbclo_count_sum)) * ff_v_b5ccbclo_count_sum)) /\ exists ff_q_b5ccbclo_count_sum_partial. ff_u_b5ccbclo_count_sum = ff_q_b5ccbclo_count_sum_partial * S ((S (ff_i_b5ccbclo_count_sum)) * ff_v_b5ccbclo_count_sum) + (ff_r_b5ccbclo_count_sum))) /\ ((((exists ff_h_b5ccbclo_count_sum_successor. ff_h_b5ccbclo_count_sum_successor + S (ff_s_b5ccbclo_count_sum) = S ((S (S ff_i_b5ccbclo_count_sum)) * ff_v_b5ccbclo_count_sum)) /\ exists ff_q_b5ccbclo_count_sum_successor. ff_u_b5ccbclo_count_sum = ff_q_b5ccbclo_count_sum_successor * S ((S (S ff_i_b5ccbclo_count_sum)) * ff_v_b5ccbclo_count_sum) + (ff_s_b5ccbclo_count_sum))) /\ ff_s_b5ccbclo_count_sum = ff_r_b5ccbclo_count_sum + ff_a_b5ccbclo_count_sum)))))) /\ (forall ff_i_b5ccbclo_count_bits. (exists ff_lt_b5ccbclo_count_bits_bound. ff_lt_b5ccbclo_count_bits_bound + S ff_i_b5ccbclo_count_bits = (l)) -> exists ff_bit_b5ccbclo_count_bits. ((((exists ff_h_b5ccbclo_count_bits_decoded. ff_h_b5ccbclo_count_bits_decoded + S (ff_bit_b5ccbclo_count_bits) = S ((S (ff_i_b5ccbclo_count_bits)) * c)) /\ exists ff_q_b5ccbclo_count_bits_decoded. b = ff_q_b5ccbclo_count_bits_decoded * S ((S (ff_i_b5ccbclo_count_bits)) * c) + (ff_bit_b5ccbclo_count_bits))) /\ (ff_bit_b5ccbclo_count_bits = 0 \/ ff_bit_b5ccbclo_count_bits = 1))))) -> exists i. (exists bcf_lt_gap_b5ccbclo_bound. bcf_lt_gap_b5ccbclo_bound + S (i) = l) /\ ((((exists fs_h_b5ccbclo_entry. fs_h_b5ccbclo_entry + S (1) = S ((S (i)) * c)) /\ exists fs_q_b5ccbclo_entry. b = fs_q_b5ccbclo_entry * S ((S (i)) * c) + (1))) /\ (exists bcf_le_gap_b5ccbclo_result. bcf_le_gap_b5ccbclo_result + (S e) = S i))

Structural proof guide

A positive bit count has a one at an index at least its count.

Direct prerequisites: bit_count_zero, bit_count_succ_decompose, bit_count_bounded, le_succ, le_refl. The authored body proceeds by structural induction (1), case analysis (9), intermediate claims (4), equality transport (6).

Proof neighborhood

Direct dependencies

BT008N bit_count_zero BT008O bit_count_succ_decompose BT008P bit_count_bounded BT0018 le_succ BT000E le_refl

Direct dependents

BT00Y5 central_binom_prime_power_contribution_le_double BT00YD central_binom_prime_valuation_zero_of_exact_double_quotients

Formal native tactic body

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

  1. 0001intro b
  2. 0002intro c
  3. 0003induction l
  4. 0004intro e
  5. 0005intro hcount
  6. 0006have himpossible : S e = 0
  7. 0007specialize bit_count_zero b
  8. 0008specialize bit_count_zero c
  9. 0009specialize bit_count_zero 0
  10. 0010specialize bit_count_zero (S e)
  11. 0011apply bit_count_zero
  12. 0012refl
  13. 0013exact hcount
  14. 0014exfalso
  15. 0015apply PA1
  16. 0016exact himpossible
  17. 0017intro e
  18. 0018intro hcount
  19. 0019have hdecomp : exists a r. (((exists fs_h_b5ccbclo_last. fs_h_b5ccbclo_last + S (a) = S ((S (l)) * c)) /\ exists fs_q_b5ccbclo_last. b = fs_q_b5ccbclo_last * S ((S (l)) * c) + (a))) /\ ((((exists ff_u_b5ccbclo_prefix_sum ff_v_b5ccbclo_prefix_sum. ((((exists ff_h_b5ccbclo_prefix_sum_start. ff_h_b5ccbclo_prefix_sum_start + S (0) = S ((S (0)) * ff_v_b5ccbclo_prefix_sum)) /\ exists ff_q_b5ccbclo_prefix_sum_start. ff_u_b5ccbclo_prefix_sum = ff_q_b5ccbclo_prefix_sum_start * S ((S (0)) * ff_v_b5ccbclo_prefix_sum) + (0))) /\ ((((exists ff_h_b5ccbclo_prefix_sum_terminal. ff_h_b5ccbclo_prefix_sum_terminal + S (r) = S ((S (l)) * ff_v_b5ccbclo_prefix_sum)) /\ exists ff_q_b5ccbclo_prefix_sum_terminal. ff_u_b5ccbclo_prefix_sum = ff_q_b5ccbclo_prefix_sum_terminal * S ((S (l)) * ff_v_b5ccbclo_prefix_sum) + (r))) /\ forall ff_i_b5ccbclo_prefix_sum. (exists ff_lt_b5ccbclo_prefix_sum_bound. ff_lt_b5ccbclo_prefix_sum_bound + S ff_i_b5ccbclo_prefix_sum = l) -> exists ff_a_b5ccbclo_prefix_sum ff_r_b5ccbclo_prefix_sum ff_s_b5ccbclo_prefix_sum. ((((exists ff_h_b5ccbclo_prefix_sum_summand. ff_h_b5ccbclo_prefix_sum_summand + S (ff_a_b5ccbclo_prefix_sum) = S ((S (ff_i_b5ccbclo_prefix_sum)) * c)) /\ exists ff_q_b5ccbclo_prefix_sum_summand. b = ff_q_b5ccbclo_prefix_sum_summand * S ((S (ff_i_b5ccbclo_prefix_sum)) * c) + (ff_a_b5ccbclo_prefix_sum))) /\ ((((exists ff_h_b5ccbclo_prefix_sum_partial. ff_h_b5ccbclo_prefix_sum_partial + S (ff_r_b5ccbclo_prefix_sum) = S ((S (ff_i_b5ccbclo_prefix_sum)) * ff_v_b5ccbclo_prefix_sum)) /\ exists ff_q_b5ccbclo_prefix_sum_partial. ff_u_b5ccbclo_prefix_sum = ff_q_b5ccbclo_prefix_sum_partial * S ((S (ff_i_b5ccbclo_prefix_sum)) * ff_v_b5ccbclo_prefix_sum) + (ff_r_b5ccbclo_prefix_sum))) /\ ((((exists ff_h_b5ccbclo_prefix_sum_successor. ff_h_b5ccbclo_prefix_sum_successor + S (ff_s_b5ccbclo_prefix_sum) = S ((S (S ff_i_b5ccbclo_prefix_sum)) * ff_v_b5ccbclo_prefix_sum)) /\ exists ff_q_b5ccbclo_prefix_sum_successor. ff_u_b5ccbclo_prefix_sum = ff_q_b5ccbclo_prefix_sum_successor * S ((S (S ff_i_b5ccbclo_prefix_sum)) * ff_v_b5ccbclo_prefix_sum) + (ff_s_b5ccbclo_prefix_sum))) /\ ff_s_b5ccbclo_prefix_sum = ff_r_b5ccbclo_prefix_sum + ff_a_b5ccbclo_prefix_sum)))))) /\ (forall ff_i_b5ccbclo_prefix_bits. (exists ff_lt_b5ccbclo_prefix_bits_bound. ff_lt_b5ccbclo_prefix_bits_bound + S ff_i_b5ccbclo_prefix_bits = l) -> exists ff_bit_b5ccbclo_prefix_bits. ((((exists ff_h_b5ccbclo_prefix_bits_decoded. ff_h_b5ccbclo_prefix_bits_decoded + S (ff_bit_b5ccbclo_prefix_bits) = S ((S (ff_i_b5ccbclo_prefix_bits)) * c)) /\ exists ff_q_b5ccbclo_prefix_bits_decoded. b = ff_q_b5ccbclo_prefix_bits_decoded * S ((S (ff_i_b5ccbclo_prefix_bits)) * c) + (ff_bit_b5ccbclo_prefix_bits))) /\ (ff_bit_b5ccbclo_prefix_bits = 0 \/ ff_bit_b5ccbclo_prefix_bits = 1))))) /\ ((a = 0 \/ a = 1) /\ S e = r + a))
  20. 0020specialize bit_count_succ_decompose b
  21. 0021specialize bit_count_succ_decompose c
  22. 0022specialize bit_count_succ_decompose l
  23. 0023specialize bit_count_succ_decompose (S l)
  24. 0024specialize bit_count_succ_decompose (S e)
  25. 0025apply bit_count_succ_decompose
  26. 0026refl
  27. 0027exact hcount
  28. 0028cases hdecomp
  29. 0029cases hdecomp_witness
  30. 0030cases hdecomp_witness_witness
  31. 0031cases hdecomp_witness_witness_right
  32. 0032cases hdecomp_witness_witness_right_right
  33. 0033cases hdecomp_witness_witness_right_right_left
  34. 0034have hprefix_value : S e = x1
  35. 0035rewrite hdecomp_witness_witness_right_right_left_left at hdecomp_witness_witness_right_right_right
  36. 0036rewrite PA3 at hdecomp_witness_witness_right_right_right
  37. 0037exact hdecomp_witness_witness_right_right_right
  38. 0038rewrite <- hprefix_value at hdecomp_witness_witness_right_left
  39. 0039rewrite <- hprefix_value at hdecomp_witness_witness_right_left
  40. 0040have hprevious : exists i. (exists bcf_lt_gap_b5ccbclo_previous_bound. bcf_lt_gap_b5ccbclo_previous_bound + S (i) = l) /\ ((((exists fs_h_b5ccbclo_previous_entry. fs_h_b5ccbclo_previous_entry + S (1) = S ((S (i)) * c)) /\ exists fs_q_b5ccbclo_previous_entry. b = fs_q_b5ccbclo_previous_entry * S ((S (i)) * c) + (1))) /\ (exists bcf_le_gap_b5ccbclo_previous_result. bcf_le_gap_b5ccbclo_previous_result + (S e) = S i))
  41. 0041specialize IH e
  42. 0042apply IH
  43. 0043exact hdecomp_witness_witness_right_left
  44. 0044cases hprevious
  45. 0045cases hprevious_witness
  46. 0046cases hprevious_witness_right
  47. 0047exists x2
  48. 0048split
  49. 0049specialize le_succ (S x2)
  50. 0050specialize le_succ l
  51. 0051apply le_succ
  52. 0052exact hprevious_witness_left
  53. 0053split
  54. 0054exact hprevious_witness_right_left
  55. 0055exact hprevious_witness_right_right
  56. 0056exists l
  57. 0057split
  58. 0058specialize le_refl (S l)
  59. 0059exact le_refl
  60. 0060split
  61. 0061rewrite hdecomp_witness_witness_right_right_left_right at hdecomp_witness_witness_left
  62. 0062rewrite hdecomp_witness_witness_right_right_left_right at hdecomp_witness_witness_left
  63. 0063exact hdecomp_witness_witness_left
  64. 0064specialize bit_count_bounded b
  65. 0065specialize bit_count_bounded c
  66. 0066specialize bit_count_bounded (S l)
  67. 0067specialize bit_count_bounded (S e)
  68. 0068apply bit_count_bounded
  69. 0069exact hcount