composite_setoid_is_inf

formal source

  77
  78/-- **Infimum Property**: The composite setoid is the greatest setoid
  79    that is at least as fine as both r₁ and r₂. -/
  80theorem composite_setoid_is_inf {E₁ E₂ : Type*}
  81    (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) :
  82    -- (1) composite ≤ r₁
  83    recognizerSetoid (r₁ ⊗ r₂) ≤ recognizerSetoid r₁ ∧
  84    -- (2) composite ≤ r₂
  85    recognizerSetoid (r₁ ⊗ r₂) ≤ recognizerSetoid r₂ ∧
  86    -- (3) greatest: any s ≤ r₁ and s ≤ r₂ implies s ≤ composite
  87    ∀ (s : Setoid C), s ≤ recognizerSetoid r₁ → s ≤ recognizerSetoid r₂ →
  88      s ≤ recognizerSetoid (r₁ ⊗ r₂) := by
  89  refine ⟨composite_setoid_le_left r₁ r₂, composite_setoid_le_right r₁ r₂, ?_⟩
  90  intro s h₁ h₂ hs
  91  exact (composite_setoid_iff r₁ r₂ _ _).mpr ⟨h₁ hs, h₂ hs⟩
  92
  93/-! ## Section 4: Refinement as a Preorder
  94
  95We define an explicit "is at least as fine as" relation on recognizers
  96that works across different event types. -/
  97
  98/-- R₁ is *at least as fine as* R₂: whenever R₁ identifies two configurations,
  99    R₂ also identifies them. Equivalently, ~_{R₁} ⊆ ~_{R₂} as sets of pairs.
 100    This is the heterogeneous refinement relation (event types may differ). -/
 101def IsFinerThan {E₁ E₂ : Type*} (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) : Prop :=
 102  ∀ c₁ c₂ : C, Indistinguishable r₁ c₁ c₂ → Indistinguishable r₂ c₁ c₂
 103
 104/-- Refinement is reflexive. -/
 105theorem isFinerThan_refl {E : Type*} (r : Recognizer C E) : IsFinerThan r r :=
 106  fun _ _ h => h
 107
 108/-- Refinement is transitive. -/
 109theorem isFinerThan_trans {E₁ E₂ E₃ : Type*}
 110    (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) (r₃ : Recognizer C E₃)