From 53aa3e5f4c048e61e8d63ca47ddd300a1bacfe00 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Wed, 15 Nov 2023 10:18:09 +1100
Subject: [PATCH] add more tests (#18)

---
 test/Mathlib/test/H20231115.expected.out   | 19 +++++++++++++++++++
 test/Mathlib/test/H20231115.in             |  5 +++++
 test/Mathlib/test/H20231115_2.expected.out | 18 ++++++++++++++++++
 test/Mathlib/test/H20231115_2.in           |  4 ++++
 test/Mathlib/test/H20231115_3.expected.out | 10 ++++++++++
 test/Mathlib/test/H20231115_3.in           |  4 ++++
 6 files changed, 60 insertions(+)
 create mode 100644 test/Mathlib/test/H20231115.expected.out
 create mode 100644 test/Mathlib/test/H20231115.in
 create mode 100644 test/Mathlib/test/H20231115_2.expected.out
 create mode 100644 test/Mathlib/test/H20231115_2.in
 create mode 100644 test/Mathlib/test/H20231115_3.expected.out
 create mode 100644 test/Mathlib/test/H20231115_3.in

diff --git a/test/Mathlib/test/H20231115.expected.out b/test/Mathlib/test/H20231115.expected.out
new file mode 100644
index 0000000..e310652
--- /dev/null
+++ b/test/Mathlib/test/H20231115.expected.out
@@ -0,0 +1,19 @@
+{"env": 0}
+
+{"sorries":
+ [{"proofState": 0,
+   "pos": {"line": 1, "column": 36},
+   "goal": "x : Nat ⊢ x + 1 > x",
+   "endPos": {"line": 1, "column": 41}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 0},
+   "endPos": {"line": 1, "column": 7},
+   "data": "declaration uses 'sorry'"}],
+ "env": 1}
+
+{"proofState": 1,
+ "goals":
+ ["case zero\n⊢ Nat.zero + 1 > Nat.zero",
+  "case succ\nx : Nat\nhx : x + 1 > x\n⊢ Nat.succ x + 1 > Nat.succ x"]}
+
diff --git a/test/Mathlib/test/H20231115.in b/test/Mathlib/test/H20231115.in
new file mode 100644
index 0000000..4bca3cd
--- /dev/null
+++ b/test/Mathlib/test/H20231115.in
@@ -0,0 +1,5 @@
+{"cmd": "import Mathlib.Tactic.Cases"}
+
+{"cmd": "example {x : Nat} : x + 1 > x := by sorry", "env": 0}
+
+{"tactic": "induction' x with x hx", "proofState": 0}
diff --git a/test/Mathlib/test/H20231115_2.expected.out b/test/Mathlib/test/H20231115_2.expected.out
new file mode 100644
index 0000000..db62ac8
--- /dev/null
+++ b/test/Mathlib/test/H20231115_2.expected.out
@@ -0,0 +1,18 @@
+{"env": 0}
+
+{"sorries":
+ [{"proofState": 0,
+   "pos": {"line": 3, "column": 12},
+   "goal": "case zero ⊢ Nat.zero + 1 > Nat.zero",
+   "endPos": {"line": 3, "column": 17}},
+  {"proofState": 1,
+   "pos": {"line": 3, "column": 12},
+   "goal": "case succ x : Nat hx : x + 1 > x ⊢ Nat.succ x + 1 > Nat.succ x",
+   "endPos": {"line": 3, "column": 17}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 0},
+   "endPos": {"line": 1, "column": 7},
+   "data": "declaration uses 'sorry'"}],
+ "env": 1}
+
diff --git a/test/Mathlib/test/H20231115_2.in b/test/Mathlib/test/H20231115_2.in
new file mode 100644
index 0000000..bab26d4
--- /dev/null
+++ b/test/Mathlib/test/H20231115_2.in
@@ -0,0 +1,4 @@
+{"cmd": "import Mathlib.Tactic.Cases"}
+
+{"cmd": "example {x : Nat} : x + 1 > x := by\n  induction' x with x hx\n  all_goals sorry", "env": 0}
+
diff --git a/test/Mathlib/test/H20231115_3.expected.out b/test/Mathlib/test/H20231115_3.expected.out
new file mode 100644
index 0000000..45b397f
--- /dev/null
+++ b/test/Mathlib/test/H20231115_3.expected.out
@@ -0,0 +1,10 @@
+{"env": 0}
+
+{"messages":
+ [{"severity": "error",
+   "pos": {"line": 1, "column": 33},
+   "endPos": {"line": 2, "column": 24},
+   "data":
+   "unsolved goals\ncase zero\n⊢ Nat.zero + 1 > Nat.zero\n\ncase succ\nx : Nat\nhx : x + 1 > x\n⊢ Nat.succ x + 1 > Nat.succ x"}],
+ "env": 1}
+
diff --git a/test/Mathlib/test/H20231115_3.in b/test/Mathlib/test/H20231115_3.in
new file mode 100644
index 0000000..fa42040
--- /dev/null
+++ b/test/Mathlib/test/H20231115_3.in
@@ -0,0 +1,4 @@
+{"cmd": "import Mathlib.Tactic.Cases"}
+
+{"cmd": "example {x : Nat} : x + 1 > x := by\n  induction' x with x hx", "env": 0}
+