Markov.lean

import Batteries.WF

abbrev ExistsAfter (P : Nat → Prop) := Acc fun y x => y = x.succ ∧ ¬P x

inductive Nat.ge (n : Nat) : Nat → Prop
  | refl : ge n n
  | step : ge n m.succ → ge n m

theorem Nat.ge_succ : ge n m → ge n.succ m
  | .refl   => .step .refl
  | .step h => .step <| ge_succ h

theorem Nat.ge_zero : ∀ n, ge n 0
  | zero   => .refl
  | succ n => ge_succ (ge_zero n)

theorem ExistsAfter.mk (hn : P n) (hnm : n.ge m) : ExistsAfter P m :=
  by induction hnm <;> constructor <;> rintro _ ⟨rfl, _⟩ <;> trivial

theorem ExistsAfter.ofExists : (∃ n, P n) → ExistsAfter P 0
  | ⟨n, hn⟩ => mk hn n.ge_zero

variable {P : Nat → Prop} [DecidablePred P]

def markovAfter : ExistsAfter P n → { n // P n } :=
  Acc.rec fun n _ ih => if hn : P n then ⟨n, hn⟩ else ih _ ⟨rfl, hn⟩

def markov (h : ∃ n, P n) : { n // P n } :=
  markovAfter <| .ofExists h