English
There is an auxiliary decidable membership relation describing the fixpoint unfolding of a partial function f, connecting to PFun.fix via a logical equivalence.
Русский
Существует вспомогательное десидируемое отношение принадлежности, связывающее разворачивание фикспойнта частичной функции f с PFun.fix через эквивалентность.
LaTeX
$$$\text{(auxiliary equivalence detailed in the statement)}$$$
Lean4
theorem fix_aux {α σ} (f : α →. σ ⊕ α) (a : α) (b : σ) :
let F : α → ℕ →. σ ⊕ α := fun a n =>
n.rec (some (Sum.inr a)) fun _ IH => IH.bind fun s => Sum.casesOn s (fun _ => Part.some s) f
(∃ n : ℕ, ((∃ b' : σ, Sum.inl b' ∈ F a n) ∧ ∀ {m : ℕ}, m < n → ∃ b : α, Sum.inr b ∈ F a m) ∧ Sum.inl b ∈ F a n) ↔
b ∈ PFun.fix f a :=
by
intro F; refine ⟨fun h => ?_, fun h => ?_⟩
· rcases h with ⟨n, ⟨_x, h₁⟩, h₂⟩
have : ∀ m a', Sum.inr a' ∈ F a m → b ∈ PFun.fix f a' → b ∈ PFun.fix f a :=
by
intro m a' am ba
induction m generalizing a' with simp [F] at am
| zero => rwa [← am]
| succ m IH =>
rcases am with ⟨a₂, am₂, fa₂⟩
exact IH _ am₂ (PFun.mem_fix_iff.2 (Or.inr ⟨_, fa₂, ba⟩))
cases n <;> simp [F] at h₂
rcases h₂ with (h₂ | ⟨a', am', fa'⟩)
· obtain ⟨a', h⟩ := h₁ (Nat.lt_succ_self _)
injection mem_unique h h₂
· exact this _ _ am' (PFun.mem_fix_iff.2 (Or.inl fa'))
· suffices
∀ a',
b ∈ PFun.fix f a' → ∀ k, Sum.inr a' ∈ F a k → ∃ n, Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
by
rcases this _ h 0 (by simp [F]) with ⟨n, hn₁, hn₂⟩
exact ⟨_, ⟨⟨_, hn₁⟩, fun {m} mn => hn₂ m mn (Nat.zero_le _)⟩, hn₁⟩
intro a₁ h₁
apply @PFun.fixInduction _ _ _ _ _ _ h₁
intro a₂ h₂ IH k hk
rcases PFun.mem_fix_iff.1 h₂ with (h₂ | ⟨a₃, am₃, _⟩)
· refine ⟨k.succ, ?_, fun m mk km => ⟨a₂, ?_⟩⟩
· simpa [F] using Or.inr ⟨_, hk, h₂⟩
· rwa [le_antisymm (Nat.le_of_lt_succ mk) km]
· rcases IH _ am₃ k.succ (by simpa [F] using ⟨_, hk, am₃⟩) with ⟨n, hn₁, hn₂⟩
grind
