sign_indistinguishable

formal source

  83    simp [signOf]
  84
  85/-- **Theorem**: Two integers are indistinguishable iff same sign -/
  86theorem sign_indistinguishable (n m : ℤ) :
  87    Indistinguishable signRecognizer n m ↔ signOf n = signOf m := by
  88  rfl
  89
  90/-- **Theorem**: -5 ~ -3 (both negative) -/
  91theorem neg_indist : Indistinguishable signRecognizer (-5) (-3) := by
  92  simp [Indistinguishable, signRecognizer, signOf]
  93
  94/-- **Theorem**: -1 ≁ 1 (different signs) -/
  95theorem neg_pos_dist : ¬Indistinguishable signRecognizer (-1) 1 := by
  96  simp [Indistinguishable, signRecognizer, signOf]
  97
  98/-- **Theorem**: 0 ≁ 1 (different signs) -/
  99theorem zero_pos_dist : ¬Indistinguishable signRecognizer 0 1 := by
 100  simp [Indistinguishable, signRecognizer, signOf]
 101
 102/-! ## Example 3: Magnitude Recognizer on ℤ -/
 103
 104/-- The magnitude recognizer: n ↦ |n| -/
 105def magnitudeRecognizer : Recognizer ℤ ℕ where
 106  R := fun n => n.natAbs
 107  nontrivial := by
 108    use 0, 1
 109    simp
 110
 111/-- **Theorem**: n ~ m iff |n| = |m| -/
 112theorem magnitude_indistinguishable (n m : ℤ) :
 113    Indistinguishable magnitudeRecognizer n m ↔ n.natAbs = m.natAbs := by
 114  rfl
 115
 116/-- **Theorem**: 3 ~ -3 (same magnitude) -/