composite_R_eq

formal source

  54/-! ## Refinement Properties -/
  55
  56/-- The composite recognizer's map is the product of component maps -/
  57theorem composite_R_eq (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) (c : C) :
  58    (r₁ ⊗ r₂).R c = (r₁.R c, r₂.R c) := rfl
  59
  60/-- Indistinguishability under composite iff indistinguishable under both -/
  61theorem composite_indistinguishable_iff (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂)
  62    (c₁ c₂ : C) :
  63    Indistinguishable (r₁ ⊗ r₂) c₁ c₂ ↔
  64    Indistinguishable r₁ c₁ c₂ ∧ Indistinguishable r₂ c₁ c₂ := by
  65  simp only [Indistinguishable, composite_R_eq, Prod.mk.injEq]
  66
  67/-- If configs are indistinguishable under composite, they are under r₁ -/
  68theorem composite_refines_left (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂)
  69    {c₁ c₂ : C} (h : Indistinguishable (r₁ ⊗ r₂) c₁ c₂) :
  70    Indistinguishable r₁ c₁ c₂ :=
  71  ((composite_indistinguishable_iff r₁ r₂ c₁ c₂).mp h).1
  72
  73/-- If configs are indistinguishable under composite, they are under r₂ -/
  74theorem composite_refines_right (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂)
  75    {c₁ c₂ : C} (h : Indistinguishable (r₁ ⊗ r₂) c₁ c₂) :
  76    Indistinguishable r₂ c₁ c₂ :=
  77  ((composite_indistinguishable_iff r₁ r₂ c₁ c₂).mp h).2
  78
  79/-- The composite distinguishes configs that either component distinguishes -/
  80theorem composite_distinguishes (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂)
  81    {c₁ c₂ : C} (h : Distinguishable r₁ c₁ c₂ ∨ Distinguishable r₂ c₁ c₂) :
  82    Distinguishable (r₁ ⊗ r₂) c₁ c₂ := by
  83  unfold Distinguishable at *
  84  intro heq
  85  rw [composite_R_eq] at heq
  86  have ⟨h1, h2⟩ := (Prod.mk.injEq _ _ _ _).mp heq
  87  cases h with