ResolutionCell

formal source

  68/-- The resolution cell of a configuration c is its equivalence class
  69    under indistinguishability. This is the set of all configurations
  70    that produce the same event as c. -/
  71def ResolutionCell {C E : Type*} (r : Recognizer C E) (c : C) : Set C :=
  72  {c' : C | c' ~[r] c}
  73
  74/-- A configuration is in its own resolution cell -/
  75theorem mem_resolutionCell_self (c : C) : c ∈ ResolutionCell r c :=
  76  Indistinguishable.refl r c
  77
  78/-- Resolution cells are exactly the fibers of the recognizer -/
  79theorem resolutionCell_eq_fiber (c : C) :
  80    ResolutionCell r c = r.fiber (r.R c) := by
  81  ext c'
  82  simp [ResolutionCell, Indistinguishable, Recognizer.fiber]
  83
  84/-- Two configurations have the same resolution cell iff they're indistinguishable -/
  85theorem resolutionCell_eq_iff {c₁ c₂ : C} :
  86    ResolutionCell r c₁ = ResolutionCell r c₂ ↔ c₁ ~[r] c₂ := by
  87  constructor
  88  · intro h
  89    have : c₂ ∈ ResolutionCell r c₁ := by
  90      rw [h]
  91      exact mem_resolutionCell_self r c₂
  92    exact (Indistinguishable.symm' r this)
  93  · intro h
  94    ext c
  95    simp [ResolutionCell, Indistinguishable]
  96    constructor
  97    · intro hc
  98      exact Eq.trans hc h
  99    · intro hc
 100      exact Eq.trans hc (Eq.symm h)
 101