Various lemmas about pareto.

ink

theorem pareto_head : ∀ {α : Type} {F : Factory α} {m m' : Meas} {ms : List Meas}, pareto F (m :: m' :: ms) → m.last > m'.last ∧ Factory.lt F m.cost m'.cost

ink

theorem pareto_rest : ∀ {α : Type} {F : Factory α} {ms : List Meas} {m : Meas}, pareto F (m :: ms) → pareto F ms

ink

theorem pareto_drop : ∀ {α : Type} {F : Factory α} {ms : List Meas} (n : ℕ), pareto F ms → pareto F (List.drop n ms)

ink

theorem pareto_rest' : ∀ {α : Type} {F : Factory α} {m m' : Meas} {ms : List Meas}, pareto F (m :: m' :: ms) → pareto F (m :: ms)

ink

theorem pareto_one : ∀ {α : Type} {F : Factory α} (m : Meas), pareto F [m]

ink

theorem pareto_cons : ∀ {α : Type} {F : Factory α} (ms : List Meas) (x y : Meas), x.last > y.last → Factory.lt F x.cost y.cost → pareto F (y :: ms) → pareto F (x :: y :: ms)

ink

theorem pareto_concat : ∀ {α : Type} {F : Factory α} {ms : List Meas} (m : Meas), pareto F ms → pareto F (dedup F (List.map (fun m' => Meas.concat F m m') ms))

ink

theorem pareto_map_lift_align : ∀ {α : Type} {F : Factory α} {ms : List Meas} (n : ℕ), pareto F ms → pareto F (List.map (Meas.adjust_align n) ms)

ink

theorem pareto_map_lift_nest : ∀ {α : Type} {F : Factory α} {ms : List Meas} (n : ℕ), pareto F ms → pareto F (List.map (Meas.adjust_nest n) ms)