CostModel

formal source

  11universe w
  12
  13/-- A minimal cost model over actions of type `A`. Costs are nonnegative reals. -/
  14structure CostModel (A : Type u) where
  15  cost : A → ℝ
  16  nonneg : ∀ a, 0 ≤ cost a
  17
  18variable {A : Type u}
  19
  20/-- Ethical preference: `a ≼ b` iff `cost a ≤ cost b` (lower cost is better). -/
  21def Prefer (M : CostModel A) (a b : A) : Prop := M.cost a ≤ M.cost b
  22
  23infix:50 "≼" => Prefer
  24
  25/-- Net improvement predicate: `a` strictly improves on `b`. -/
  26def Improves (M : CostModel A) (a b : A) : Prop := M.cost a < M.cost b
  27
  28/-- Reflexivity: every action is at least as good as itself. -/
  29lemma prefer_refl (M : CostModel A) (a : A) : Prefer M a a := by
  30  dsimp [Prefer]
  31  exact le_rfl
  32
  33/-- Transitivity: if `a ≼ b` and `b ≼ c`, then `a ≼ c`. -/
  34lemma prefer_trans (M : CostModel A) {a b c : A}
  35  (hab : Prefer M a b) (hbc : Prefer M b c) : Prefer M a c := by
  36  dsimp [Prefer] at hab hbc ⊢; exact le_trans hab hbc
  37
  38/-- Preorder instance for preference. -/
  39instance (M : CostModel A) : Preorder A where
  40  le := fun a b => Prefer M a b
  41  le_refl := fun a => prefer_refl M a
  42  le_trans := fun a b c hab hbc => prefer_trans M hab hbc
  43
  44/-- Composable actions under a cost model: binary composition with subadditivity and monotonicity. -/