RSDecidable

formal source

 150
 151/-- A predicate is **RS-decidable** at `(c_star, B, c₀)` when the background
 152    conditions for Boolean reasoning hold: existence and stabilization. -/
 153def RSDecidable {C : Type*}
 154    (bridge : CostBridge C) (B : C → C) (c₀ c_star : C) (P : C → Bool) : Prop :=
 155  RSExists_cfg bridge c_star ∧ Stabilizes B P c₀ c_star
 156
 157/-- One direction always holds: RSTrue(¬P) ⟹ ¬RSTrue(P). -/
 158theorem rs_true_neg_imp_neg_rs_true {C : Type*}
 159    {bridge : CostBridge C} {B : C → C} {c₀ c_star : C} {P : C → Bool} :
 160    RSTrue bridge B c₀ c_star (fun c => !P c) → ¬RSTrue bridge B c₀ c_star P := by
 161  intro ⟨_, hval, _⟩ ⟨_, hval', _⟩
 162  simp at hval
 163  rw [hval] at hval'
 164  exact Bool.false_ne_true hval'
 165
 166/-- Under RS-decidability the full negation law holds. -/
 167theorem rs_true_neg_iff_neg_rs_true {C : Type*}
 168    {bridge : CostBridge C} {B : C → C} {c₀ c_star : C} {P : C → Bool}
 169    (hdec : RSDecidable bridge B c₀ c_star P) :
 170    RSTrue bridge B c₀ c_star (fun c => !P c) ↔ ¬RSTrue bridge B c₀ c_star P := by
 171  constructor
 172  · exact rs_true_neg_imp_neg_rs_true
 173  · intro hnotP
 174    have ⟨hexists, hstab⟩ := hdec
 175    by_cases hv : P c_star = true
 176    · exfalso; exact hnotP ⟨hexists, hv, hstab⟩
 177    · push_neg at hv
 178      have hv' : P c_star = false := Bool.eq_false_iff.mpr hv
 179      refine ⟨hexists, ?_, ?_⟩
 180      · simp [hv']
 181      · obtain ⟨N, hN⟩ := hstab
 182        exact ⟨N, fun n hn => by simp [hN n hn, hv']⟩
 183