prefer_refl

formal source

  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. -/
  52theorem prefer_comp_mono (M : CostModel A) (C : Composable M)
  53  {a₁ a₂ b₁ b₂ : A}
  54  (ha : Prefer M a₁ a₂) (hb : Prefer M b₁ b₂) :
  55  Prefer M (C.comp a₁ b₁) (C.comp a₂ b₂) := by
  56  dsimp [Prefer] at ha hb ⊢
  57  exact C.mono a₁ a₂ b₁ b₂ ha hb
  58
  59/-- Composition preserves improvement. -/