From a509b0c615f2b33c8277db404ab3f2d9bf982f02 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 30 Mar 2022 13:33:29 -0700
Subject: [PATCH] test: `Sign`

---
 tests/lean/run/sign.lean | 50 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 50 insertions(+)
 create mode 100644 tests/lean/run/sign.lean

diff --git a/tests/lean/run/sign.lean b/tests/lean/run/sign.lean
new file mode 100644
index 0000000000..e0b080a9ee
--- /dev/null
+++ b/tests/lean/run/sign.lean
@@ -0,0 +1,50 @@
+inductive Sign where
+  | zero | neg | pos
+  deriving DecidableEq
+
+instance : OfNat Sign (nat_lit 0) where
+  ofNat := .zero
+
+instance : OfNat Sign (nat_lit 1) where
+  ofNat := .pos
+
+instance : Neg Sign where
+  neg | .zero => .zero
+      | .pos  => .neg
+      | .neg  => .pos
+
+namespace Sign
+
+@[simp] theorem zero_eq : zero = 0 := rfl
+@[simp] theorem neg_eq : neg  = -1 := rfl
+@[simp] theorem pos_eq : pos = 1 := rfl
+
+def mul : Sign → Sign → Sign
+  | neg,  neg  => pos
+  | neg,  pos  => neg
+  | neg,  zero => zero
+  | zero, _    => zero
+  | pos,  s    => s
+
+instance : Mul Sign where
+  mul a b := Sign.mul a b
+
+def le : Sign → Sign → Bool
+  | neg,  _    => true
+  | zero, zero => true
+  | _,    pos  => true
+  | _,    _    => false
+
+instance : LE Sign where
+  le a b := Sign.le a b
+
+instance : DecidableRel (· ≤ · : Sign → Sign → Prop) :=
+  fun a b => inferInstanceAs (Decidable (le a b = true))
+
+theorem neg_bot {s : Sign} : s ≤ -1 → s = -1 := by
+  cases s <;> decide
+
+theorem pos_top {s : Sign} : 1 ≤ s → s = 1 := by
+  cases s <;> decide
+
+end Sign