From c1573d15c199015a6efbf1660a15680acb460cde Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 8 Sep 2021 08:00:36 -0700
Subject: [PATCH] test: missing tests

---
 tests/lean/run/injections1.lean |  3 +++
 tests/lean/run/split3.lean      | 38 +++++++++++++++++++++++++++++++++
 2 files changed, 41 insertions(+)
 create mode 100644 tests/lean/run/injections1.lean
 create mode 100644 tests/lean/run/split3.lean

diff --git a/tests/lean/run/injections1.lean b/tests/lean/run/injections1.lean
new file mode 100644
index 0000000000..085638d14b
--- /dev/null
+++ b/tests/lean/run/injections1.lean
@@ -0,0 +1,3 @@
+example (a b c d e f : Nat) (h : [a, b, c] = [d, e, f]) : a + b + c = d + e + f := by
+  injections
+  simp [*]
diff --git a/tests/lean/run/split3.lean b/tests/lean/run/split3.lean
new file mode 100644
index 0000000000..f7137ff10a
--- /dev/null
+++ b/tests/lean/run/split3.lean
@@ -0,0 +1,38 @@
+def g (xs ys : List Nat) : Nat :=
+  match xs, ys with
+  | [a, b], _ => Nat.succ (a+b)
+  | _, [b, c] => Nat.succ b
+  | _, _   => 1
+
+example (a b : Bool) (x y z : Nat) (xs : List Nat) (h1 : (if a then x else y) = 0) (h2 : xs.head! = 0) : g [x] xs = 1 := by
+  simp [g]
+  repeat anyGoals (split at *)
+  anyGoals (first | decide | contradiction | injections)
+  next b c _ _ _ =>
+    show Nat.succ b = 1
+    subst xs; simp [List.head!] at h2; simp [h2]
+  next b c _ _ _ =>
+    show Nat.succ b = 1
+    subst xs; simp [List.head!] at h2; simp [h2]
+
+example (a : Bool) (h1 : (if a then x else y) = 1) : x + y > 0 := by
+  split at h1
+  . subst h1; rw [Nat.succ_add]; apply Nat.zero_lt_succ
+  . subst h1; apply Nat.zero_lt_succ
+
+def f (x : Nat) : Nat :=
+  match x with
+  | 100 => 0
+  | 200 => 0
+  | _   => 1
+
+example (h1 : f x = 0) (h2 : x > 300) : False := by
+  simp [f] at h1
+  split at h1
+  . contradiction
+  . contradiction
+  . contradiction
+
+example (h1 : f x = 0) (h2 : x > 300) : False := by
+  simp [f] at h1
+  split at h1 <;> contradiction