recognizerSetoid_iff

formal source

  40  indistinguishableSetoid r
  41
  42/-- The setoid relation unfolds to R(c₁) = R(c₂). -/
  43theorem recognizerSetoid_iff {E : Type*} (r : Recognizer C E) (c₁ c₂ : C) :
  44    (recognizerSetoid r).Rel c₁ c₂ ↔ r.R c₁ = r.R c₂ :=
  45  Iff.rfl
  46
  47/-! ## Section 2: Composition Refines Both Components
  48
  49In Mathlib's ordering on `Setoid C`, we have `s ≤ t` iff `∀ a b, s.Rel a b → t.Rel a b`.
  50This means s ≤ t when s is *at least as fine as* t (s-related implies t-related, so
  51t has at least as many related pairs, i.e., t is coarser). The composite recognizer
  52R₁ ⊗ R₂ is finer than both R₁ and R₂, so its setoid is ≤ both component setoids. -/
  53
  54/-- The composite setoid relates c₁, c₂ iff both components do. -/
  55theorem composite_setoid_iff {E₁ E₂ : Type*}
  56    (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) (c₁ c₂ : C) :
  57    (recognizerSetoid (r₁ ⊗ r₂)).Rel c₁ c₂ ↔
  58    (recognizerSetoid r₁).Rel c₁ c₂ ∧ (recognizerSetoid r₂).Rel c₁ c₂ :=
  59  composite_indistinguishable_iff r₁ r₂ c₁ c₂
  60
  61/-- **Refinement Left**: The composite setoid is at least as fine as r₁'s. -/
  62theorem composite_setoid_le_left {E₁ E₂ : Type*}
  63    (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) :
  64    recognizerSetoid (r₁ ⊗ r₂) ≤ recognizerSetoid r₁ :=
  65  fun h => ((composite_setoid_iff r₁ r₂ _ _).mp h).1
  66
  67/-- **Refinement Right**: The composite setoid is at least as fine as r₂'s. -/
  68theorem composite_setoid_le_right {E₁ E₂ : Type*}
  69    (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) :
  70    recognizerSetoid (r₁ ⊗ r₂) ≤ recognizerSetoid r₂ :=
  71  fun h => ((composite_setoid_iff r₁ r₂ _ _).mp h).2
  72
  73/-! ## Section 3: The Infimum (Meet) Property