Prefer

formal source

  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. -/
  45structure Composable (M : CostModel A) where
  46  comp : A → A → A
  47  subadd : ∀ a b, M.cost (comp a b) ≤ M.cost a + M.cost b
  48  mono : ∀ a a' b b', Prefer M a a' → Prefer M b b' → Prefer M (comp a b) (comp a' b')
  49  strict_mono_left : ∀ a a' x, Improves M a a' → Improves M (comp a x) (comp a' x)
  50
  51/-- Monotonicity of composition w.r.t. preference. -/