CompositeRecognizer

formal source

  37
  38/-- The composite of two recognizers produces events in the product space.
  39    This is RG6: composition of recognizers. -/
  40def CompositeRecognizer (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) :
  41    Recognizer C (E₁ × E₂) where
  42  R := fun c => (r₁.R c, r₂.R c)
  43  nontrivial := by
  44    -- Use nontriviality of r₁ to construct distinct events
  45    obtain ⟨c₁, c₂, hne⟩ := r₁.nontrivial
  46    use c₁, c₂
  47    intro heq
  48    apply hne
  49    exact (Prod.mk.injEq _ _ _ _).mp heq |>.1
  50
  51/-- Notation for composite recognizer -/
  52infixl:70 " ⊗ " => CompositeRecognizer
  53
  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₂ :=