From 666d454b429c39b334f8057a02c20b8774088f94 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Tue, 2 Jan 2024 05:17:52 -0800
Subject: [PATCH] test: `Int` `simproc`s

---
 tests/lean/simprocEval4.lean              | 73 +++++++++++++++++++++++
 tests/lean/simprocEval4.lean.expected.out | 28 +++++++++
 2 files changed, 101 insertions(+)
 create mode 100644 tests/lean/simprocEval4.lean
 create mode 100644 tests/lean/simprocEval4.lean.expected.out

diff --git a/tests/lean/simprocEval4.lean b/tests/lean/simprocEval4.lean
new file mode 100644
index 0000000000..4252686e08
--- /dev/null
+++ b/tests/lean/simprocEval4.lean
@@ -0,0 +1,73 @@
+def foo (_ : Nat) : Int := 10
+
+example : foo x = 8 + 2 := by
+  simp
+  trace_state
+  rw [foo]
+
+example : foo x = 12 + (- 2) := by
+  simp
+  trace_state
+  rw [foo]
+
+example : foo x = 5 * 2 := by
+  simp
+  trace_state
+  rw [foo]
+
+example : foo x = 12 - 2 := by
+  simp
+  trace_state
+  rw [foo]
+
+example : foo x = 20 / 2 := by
+  simp
+  trace_state
+  rw [foo]
+
+example : foo x = 110 % 100 := by
+  simp
+  trace_state
+  rw [foo]
+
+example : foo x = (3+2)*2 := by
+  simp
+  trace_state
+  rw [foo]
+
+example : foo x * foo x = 10 ^ 2 := by
+  simp
+  trace_state
+  simp [foo]
+
+example : foo x = - (- 10) := by
+  simp
+  trace_state
+  simp [foo]
+
+example : Int.natAbs (foo x) = Int.natAbs (- (8 + 2)) := by
+  simp
+  trace_state
+  simp [foo]
+
+def boo (_ : Nat) := True
+
+example : boo x ↔ (2 : Int) < 3 := by
+  simp
+  trace_state
+  trivial
+
+example : boo x ↔ (3 : Int) > 2 := by
+  simp
+  trace_state
+  trivial
+
+example : boo x ↔ (2 : Int) ≤ 3 := by
+  simp
+  trace_state
+  trivial
+
+example : boo x ↔ (3 : Int) ≥ 2 := by
+  simp
+  trace_state
+  trivial
diff --git a/tests/lean/simprocEval4.lean.expected.out b/tests/lean/simprocEval4.lean.expected.out
new file mode 100644
index 0000000000..46f3a0ec71
--- /dev/null
+++ b/tests/lean/simprocEval4.lean.expected.out
@@ -0,0 +1,28 @@
+x : Nat
+⊢ foo x = 10
+x : Nat
+⊢ foo x = 10
+x : Nat
+⊢ foo x = 10
+x : Nat
+⊢ foo x = 10
+x : Nat
+⊢ foo x = 10
+x : Nat
+⊢ foo x = 10
+x : Nat
+⊢ foo x = 10
+x : Nat
+⊢ foo x * foo x = 100
+x : Nat
+⊢ foo x = 10
+x : Nat
+⊢ Int.natAbs (foo x) = 10
+x : Nat
+⊢ boo x
+x : Nat
+⊢ boo x
+x : Nat
+⊢ boo x
+x : Nat
+⊢ boo x