composite_refines_left

formal source

  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
  88  | inl h₁ => exact h₁ h1
  89  | inr h₂ => exact h₂ h2
  90
  91/-! ## Resolution Cell Refinement -/
  92
  93/-- Resolution cells under composite are intersections of component cells -/
  94theorem composite_resolutionCell (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) (c : C) :
  95    ResolutionCell (r₁ ⊗ r₂) c = ResolutionCell r₁ c ∩ ResolutionCell r₂ c := by
  96  ext c'
  97  simp only [ResolutionCell, Set.mem_setOf_eq, Set.mem_inter_iff,
  98             composite_indistinguishable_iff]