def
definition
signRecognizer
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.RecogGeom.Examples on GitHub at line 79.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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]
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