discrete_singleton_cells

formal source

  50  simp [Indistinguishable, discreteRecognizer]
  51
  52/-- **Corollary**: Each config is in its own resolution cell -/
  53theorem discrete_singleton_cells (n : ℕ) [h : NeZero n] (hn : 2 ≤ n) (c : Fin n) :
  54    ResolutionCell (discreteRecognizer n hn) c = {c} := by
  55  ext x
  56  simp [ResolutionCell, discrete_indist_iff_eq]
  57
  58/-! ## Example 2: Sign Recognizer on ℤ -/
  59
  60/-- Integer configuration space -/
  61instance : ConfigSpace ℤ where
  62  nonempty := ⟨0⟩
  63
  64/-- Three-valued sign type -/
  65inductive Sign : Type
  66  | neg : Sign
  67  | zero : Sign
  68  | pos : Sign
  69  deriving DecidableEq, Repr
  70
  71/-- Sign is nonempty -/
  72instance : Nonempty Sign := ⟨Sign.zero⟩
  73
  74/-- The sign function -/
  75def signOf : ℤ → Sign
  76  | n => if n < 0 then Sign.neg else if n = 0 then Sign.zero else Sign.pos
  77
  78/-- The sign recognizer on ℤ -/
  79def signRecognizer : Recognizer ℤ Sign where
  80  R := signOf
  81  nontrivial := by
  82    use -1, 1
  83    simp [signOf]