Various lemmas about list of measures when they are decreasing in last length and increasing in cost.

ink

theorem last_decreasing_head : ∀ {α : Type} {x y : Meas} {xs : List Meas}, last_decreasing (x :: y :: xs) → x.last > y.last

ink

theorem last_decreasing_rest : ∀ {α : Type} {x : Meas} {xs : List Meas}, last_decreasing (x :: xs) → last_decreasing xs

ink

theorem last_decreasing_empty {α : Type} : last_decreasing []

ink

theorem last_decreasing_one : ∀ {α : Type} {x : Meas}, last_decreasing [x]

ink

theorem last_decreasing_cons {α : Type} (x : Meas) (y : Meas) (xs : List Meas) (h_last : x.last > y.last) (h : last_decreasing (y :: xs)) : last_decreasing (x :: y :: xs)

ink

theorem last_decreasing_strong : ∀ {α : Type} {ms : List Meas}, last_decreasing ms → ∀ (i j : ℕ) (h_i : i < List.length ms) (h_j : j < List.length ms), i < j → (List.get ms { val := i, isLt := h_i }).last > (List.get ms { val := j, isLt := h_j }).last

ink

theorem cost_increasing_head : ∀ {α : Type} {F : Factory α} {x y : Meas} {xs : List Meas}, cost_increasing F (x :: y :: xs) → Factory.lt F x.cost y.cost

ink

theorem cost_increasing_rest : ∀ {α : Type} {F : Factory α} {x : Meas} {xs : List Meas}, cost_increasing F (x :: xs) → cost_increasing F xs

ink

theorem cost_increasing_empty : ∀ {α : Type} {F : Factory α}, cost_increasing F []

ink

theorem cost_increasing_one : ∀ {α : Type} {F : Factory α} {x : Meas}, cost_increasing F [x]

ink

theorem cost_increasing_cons : ∀ {α : Type} {F : Factory α} (x y : Meas) (xs : List Meas), Factory.lt F x.cost y.cost → cost_increasing F (y :: xs) → cost_increasing F (x :: y :: xs)

ink

theorem cost_increasing_strong : ∀ {α : Type} {F : Factory α} {ms : List Meas}, cost_increasing F ms → ∀ (i j : ℕ) (h_i : i < List.length ms) (h_j : j < List.length ms), i < j → Factory.lt F (List.get ms { val := i, isLt := h_i }).cost (List.get ms { val := j, isLt := h_j }).cost

ink

theorem cost_increasing_non_strict_head : ∀ {α : Type} {F : Factory α} {x y : Meas} {xs : List Meas}, cost_increasing_non_strict F (x :: y :: xs) → Factory.le F x.cost y.cost = true

ink

theorem cost_increasing_non_strict_rest : ∀ {α : Type} {F : Factory α} {x : Meas} {xs : List Meas}, cost_increasing_non_strict F (x :: xs) → cost_increasing_non_strict F xs

ink

theorem cost_increasing_non_strict_empty : ∀ {α : Type} {F : Factory α}, cost_increasing_non_strict F []

ink

theorem cost_increasing_non_strict_one : ∀ {α : Type} {F : Factory α} {x : Meas}, cost_increasing_non_strict F [x]

ink

theorem cost_increasing_non_strict_cons : ∀ {α : Type} {F : Factory α} (x y : Meas) (xs : List Meas), Factory.le F x.cost y.cost = true → cost_increasing_non_strict F (y :: xs) → cost_increasing_non_strict F (x :: y :: xs)

ink

theorem last_decreasing_concat {α : Type} {ms : List Meas} (F : Factory α) (m : Meas) (h : last_decreasing ms) : last_decreasing (List.map (fun m' => Meas.concat F m m') ms)

ink

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

ink

theorem last_decreasing_bound : ∀ {α : Type} {ms : List Meas}, last_decreasing ms → ∀ (i : ℕ) (hi : List.length ms - 1 - i < List.length ms), i < List.length ms → (List.get ms { val := List.length ms - 1 - i, isLt := hi }).last ≥ i