PA004H

finite_contains_decidable

Stable checked-use theorem · independently closed

Occurrence of a value in a nonempty decoded prefix is constructively decidable.

Exact expanded PA statement

forall b c l y. ((exists fp_i_contains_l. ((exists fp_gap_contains_l_index. fp_gap_contains_l_index + S fp_i_contains_l = l) /\ (((exists ff_h_contains_l_entry. ff_h_contains_l_entry + S (y) = S ((S (fp_i_contains_l)) * c)) /\ exists ff_q_contains_l_entry. b = ff_q_contains_l_entry * S ((S (fp_i_contains_l)) * c) + (y))))) \/ ~(exists fp_i_contains_l. ((exists fp_gap_contains_l_index. fp_gap_contains_l_index + S fp_i_contains_l = l) /\ (((exists ff_h_contains_l_entry. ff_h_contains_l_entry + S (y) = S ((S (fp_i_contains_l)) * c)) /\ exists ff_q_contains_l_entry. b = ff_q_contains_l_entry * S ((S (fp_i_contains_l)) * c) + (y))))))

Structural proof guide

Generated structural guide

Occurrence of a value in a nonempty decoded prefix is constructively decidable.

Use the direct prerequisites add_eq_zero_right, succ_ne_zero, finite_lt_succ_eq_or_lt, beta_at_exists, beta_at_unique, eq_decidable, le_refl, le_succ as previously established PA formulas.

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

Referenced ingredients

PA0004 add_eq_zero_right PA0005 succ_ne_zero PA003D finite_lt_succ_eq_or_lt PA0029 beta_at_exists PA002F beta_at_unique PA004G eq_decidable PA001A le_refl PA002O le_succ

Proof neighborhood

Direct dependencies

PA0004 add_eq_zero_right PA0005 succ_ne_zero PA003D finite_lt_succ_eq_or_lt PA0029 beta_at_exists PA002F beta_at_unique PA004G eq_decidable PA001A le_refl PA002O le_succ

Direct dependents

PA004W finite_bounded_injective_surjective PA0092 finite_covers_into_or_omits

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 b
  2. 0002intro c
  3. 0003induction l
  4. 0004intro y
  5. 0005right
  6. 0006intro hcontains
  7. 0007cases hcontains
  8. 0008cases hcontains_witness
  9. 0009cases hcontains_witness_left
  10. 0010have hsi : S x = 0
  11. 0011specialize add_eq_zero_right x1
  12. 0012specialize add_eq_zero_right (S x)
  13. 0013apply add_eq_zero_right
  14. 0014exact hcontains_witness_left_witness
  15. 0015specialize succ_ne_zero x
  16. 0016apply succ_ne_zero
  17. 0017exact hsi
  18. 0018intro y
  19. 0019have hpresent : (exists i. ((exists h. h + S i = l) /\ ((exists h. h + S y = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + y))) \/ ~(exists i. ((exists h. h + S i = l) /\ ((exists h. h + S y = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + y)))
  20. 0020specialize IH y
  21. 0021exact IH
  22. 0022cases hpresent
  23. 0023left
  24. 0024cases hpresent_left
  25. 0025cases hpresent_left_witness
  26. 0026exists x
  27. 0027split
  28. 0028specialize le_succ (S x)
  29. 0029specialize le_succ l
  30. 0030apply le_succ
  31. 0031exact hpresent_left_witness_left
  32. 0032exact hpresent_left_witness_right
  33. 0033specialize beta_at_exists b
  34. 0034specialize beta_at_exists c
  35. 0035specialize beta_at_exists l
  36. 0036cases beta_at_exists
  37. 0037specialize eq_decidable x
  38. 0038specialize eq_decidable y
  39. 0039cases eq_decidable
  40. 0040left
  41. 0041exists l
  42. 0042split
  43. 0043specialize le_refl (S l)
  44. 0044exact le_refl
  45. 0045rewrite eq_decidable_left at beta_at_exists_witness
  46. 0046rewrite eq_decidable_left at beta_at_exists_witness
  47. 0047exact beta_at_exists_witness
  48. 0048right
  49. 0049intro hfull
  50. 0050cases hfull
  51. 0051cases hfull_witness
  52. 0052have hindex : x1 = l \/ exists h. h + S x1 = l
  53. 0053specialize finite_lt_succ_eq_or_lt l
  54. 0054specialize finite_lt_succ_eq_or_lt x1
  55. 0055apply finite_lt_succ_eq_or_lt
  56. 0056exact hfull_witness_left
  57. 0057cases hindex
  58. 0058have hentry : ((exists h. h + S y = S ((S l) * c)) /\ exists q. b = q * S ((S l) * c) + y)
  59. 0059rewrite hindex_left at hfull_witness_right
  60. 0060rewrite hindex_left at hfull_witness_right
  61. 0061exact hfull_witness_right
  62. 0062have hxy : x = y
  63. 0063specialize beta_at_unique b
  64. 0064specialize beta_at_unique c
  65. 0065specialize beta_at_unique l
  66. 0066specialize beta_at_unique x
  67. 0067specialize beta_at_unique y
  68. 0068apply beta_at_unique
  69. 0069exact beta_at_exists_witness
  70. 0070exact hentry
  71. 0071apply eq_decidable_right
  72. 0072exact hxy
  73. 0073apply hpresent_right
  74. 0074exists x1
  75. 0075split
  76. 0076exact hindex_right
  77. 0077exact hfull_witness_right