refinement_theorem

formal source

 151
 152    This means the composite recognizer "sees" at least as much structure as
 153    either component recognizer. -/
 154theorem refinement_theorem (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) :
 155    Function.Surjective (quotientMapLeft r₁ r₂) ∧
 156    Function.Surjective (quotientMapRight r₁ r₂) :=
 157  ⟨quotientMapLeft_surjective r₁ r₂, quotientMapRight_surjective r₁ r₂⟩
 158
 159/-! ## Associativity and Commutativity -/
 160
 161/-- Composition is commutative up to isomorphism on events -/
 162theorem composite_comm_events (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) (c : C) :
 163    (r₁ ⊗ r₂).R c = Prod.swap ((r₂ ⊗ r₁).R c) := by
 164  simp [composite_R_eq]
 165
 166/-- Indistinguishability is symmetric under swap -/
 167theorem composite_comm_indistinguishable (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂)
 168    (c₁ c₂ : C) :
 169    Indistinguishable (r₁ ⊗ r₂) c₁ c₂ ↔ Indistinguishable (r₂ ⊗ r₁) c₁ c₂ := by
 170  rw [composite_indistinguishable_iff, composite_indistinguishable_iff]
 171  exact And.comm
 172
 173/-! ## N-ary Composition -/
 174
 175/-- Triple composite recognizer -/
 176def CompositeRecognizer₃ {E₃ : Type*}
 177    (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) (r₃ : Recognizer C E₃) :
 178    Recognizer C (E₁ × E₂ × E₃) where
 179  R := fun c => (r₁.R c, r₂.R c, r₃.R c)
 180  nontrivial := by
 181    obtain ⟨c₁, c₂, hne⟩ := r₁.nontrivial
 182    use c₁, c₂
 183    intro heq
 184    apply hne