Various lemmas related to the dedup operation

ink

theorem dedup_not_empty : ∀ {α : Type} {ms : List Meas} {F : Factory α}, ms ≠ [] → dedup F ms ≠ []

ink

theorem dedup_member : ∀ {α : Type} {m : Meas} {F : Factory α} {ms : List Meas}, m ∈ dedup F ms → m ∈ ms

ink

theorem dedup_last_first : ∀ {α : Type} {F : Factory α} {m : Meas} {ms : List Meas} {m' : Meas} {ms' : List Meas}, dedup F (m :: ms) = m' :: ms' → last_decreasing (m :: ms) → m.last ≥ m'.last

ink

theorem dedup_last_decreasing : ∀ {α : Type} {ms : List Meas} {F : Factory α}, last_decreasing ms → last_decreasing (dedup F ms)

ink

theorem dedup_cost_first : ∀ {α : Type} {F : Factory α} {m : Meas} {ms : List Meas} {m' : Meas} {ms' : List Meas}, dedup F (m :: ms) = m' :: ms' → cost_increasing_non_strict F (m :: ms) → m.cost = m'.cost

ink

theorem dedup_cost_increasing : ∀ {α : Type} {F : Factory α} {ms : List Meas}, cost_increasing_non_strict F ms → cost_increasing F (dedup F ms)

ink

theorem dedup_cons : ∀ {α : Type} {m : Meas} {F : Factory α} {ms : List Meas} (m' : Meas), m ∈ dedup F ms → m ∈ dedup F (m' :: ms)

ink

theorem dedup_dom : ∀ {α : Type} {m : Meas} {ms : List Meas} {F : Factory α}, m ∈ ms → last_decreasing ms → cost_increasing_non_strict F ms → ∃ m_better, m_better ∈ dedup F ms ∧ dominates F m_better m = true