OraclePartialMinimizationTraces.lean

1 import RealizationBoundaries.ComputablePresentations
2 
3 /-! # Exact finite value traces for native partial minimization -/
4 set_option autoImplicit false
5 set_option backward.isDefEq.respectTransparency false
6 noncomputable section
7 namespace RealizationBoundaries
8 
9 /-- A successful native minimization has exactly a finite trace of defined,
10 nonzero earlier outputs followed by a zero output. No behavior after the
11 successful bound is required. -/
12 theorem oracle_partial_minimization_trace (f : ℕ →. ℕ) (a y : ℕ) :
13     y ∈ Nat.rfind (fun i => (fun m => decide (m = 0)) <$> f (Nat.pair a i)) ↔
14       ∃ s : ℕ → ℕ, s y = 0 ∧
15         (∀ i ≤ y, s i ∈ f (Nat.pair a i)) ∧ ∀ i < y, s i ≠ 0 := by
16   classical
17   rw [Nat.mem_rfind]
18   constructor
19   · rintro ⟨hy, hmin⟩
20     have hz : 0 ∈ f (Nat.pair a y) := by
21       obtain ⟨v, hv, hzero⟩ := (Part.mem_map_iff _).mp hy
22       have hv0 : v = 0 := by simpa using hzero
23       exact hv0 ▸ hv
24     have hdom : ∀ i ≤ y, (f (Nat.pair a i)).Dom := by
25       intro i hi
26       rcases lt_or_eq_of_le hi with hlt | rfl
27       · obtain ⟨v, hv, _⟩ := (Part.mem_map_iff _).mp (hmin hlt)
28         exact Part.dom_iff_mem.mpr ⟨v, hv⟩
29       · exact Part.dom_iff_mem.mpr ⟨0, hz⟩
30     let s : ℕ → ℕ := fun i => if hi : i ≤ y then (f (Nat.pair a i)).get (hdom i hi) else 0
31     have hs : ∀ i ≤ y, s i ∈ f (Nat.pair a i) := by
32       intro i hi
33       dsimp [s]
34       rw [dite_eq_left hi]
35       exact Part.get_mem _
36     refine ⟨s, Part.mem_unique (hs y le_rfl) hz, hs, ?_⟩
37     intro i hi
38     obtain ⟨v, hv, hfalse⟩ := (Part.mem_map_iff _).mp (hmin hi)
39     have hv0 : v ≠ 0 := by simpa using hfalse
40     have he : s i = v := Part.mem_unique (hs i hi.le) hv
41     exact he ▸ hv0
42   · rintro ⟨s, hy, hs, hn⟩
43     constructor
44     · apply (Part.mem_map_iff _).mpr
45       exact ⟨s y, hs y le_rfl, by simp [hy]⟩
46     · intro i hi
47       apply (Part.mem_map_iff _).mpr
48       exact ⟨s i, hs i hi.le, by simp [hn i hi]⟩
49 
50 end RealizationBoundaries

Back to source controls