Optimality theorems

ink

theorem Resolve_optimal : ∀ {α : Type} {F : Factory α} {d : Doc} {c i : ℕ} {ml : MeasureSet} {D : List Doc} {d_choiceless : Doc} {m : Meas}, Resolve F d c i ml → Widen d D → d_choiceless ∈ D → MeasRender F d_choiceless c i m → m.y ≤ F.W → m.x ≤ F.W → ∃ ms h, ml = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = true

The optimality theorem (Theorem 5.7)

ink

theorem ResolveConcat_optimal : ∀ {α : Type} {F : Factory α} {ms : List Meas} {d₂ : Doc} {i : ℕ} {ml : MeasureSet} {L₂ : List Doc} {d_right : Doc} {m₂ m_better_left m₁ : Meas}, ResolveConcat F ms d₂ i ml → Widen d₂ L₂ → d_right ∈ L₂ → MeasRender F d_right m₁.last i m₂ → m₁.x ≤ F.W ∧ m₂.x ≤ F.W → m₁.y ≤ F.W ∧ m₂.y ≤ F.W → dominates F m_better_left m₁ = true → m_better_left ∈ ms → ∃ ms h, ml = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better (Meas.concat F m₁ m₂) = true

ink

theorem ResolveConcatOne_optimal {d₂ : Doc} {L₂ : List Doc} {d_right : Doc} : ∀ {α : Type} {F : Factory α} {m_better : Meas} {i : ℕ} {ml : MeasureSet} {m₂ m₁ : Meas}, Widen d₂ L₂ → d_right ∈ L₂ → ResolveConcatOne F d₂ m_better i ml → MeasRender F d_right m₁.last i m₂ → m₁.x ≤ F.W ∧ m₂.x ≤ F.W → m₁.y ≤ F.W ∧ m₂.y ≤ F.W → dominates F m_better m₁ = true → ∃ ms h, ml = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better (Meas.concat F m₁ m₂) = true