From 22a80a9623a77243cef2db95f79135ddef1bfb04 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 31 Aug 2021 17:09:00 -0700
Subject: [PATCH] test: `split` tactic tests

---
 tests/lean/run/def10.lean | 28 ++++++++++++++++++++--------
 tests/lean/run/def20.lean |  9 +++++++--
 tests/lean/run/def4.lean  | 24 +++++++++++-------------
 3 files changed, 38 insertions(+), 23 deletions(-)

diff --git a/tests/lean/run/def10.lean b/tests/lean/run/def10.lean
index eb0de93d1c..48f2d92654 100644
--- a/tests/lean/run/def10.lean
+++ b/tests/lean/run/def10.lean
@@ -1,18 +1,30 @@
-
-
 def f : Bool → Bool → Nat
-| _, _ => 10
+  | true, true => 0
+  | _, _       => 3
 
-example : f true true = 10 :=
-rfl
+example : f true true = 0 :=
+  rfl
 
 def g : Bool → Bool → Bool → Nat
-| true, _,    true  => 1
-| _,   false, false => 2
-| _,   _,     _     => 3
+  | true, _,    true  => 1
+  | _,   false, false => 2
+  | a,   _,     b     => f a b
 
 theorem ex1 : g true true true = 1 := rfl
 theorem ex2 : g true false true = 1 := rfl
 theorem ex3 : g true false false = 2 := rfl
 theorem ex4 : g false false false = 2 := rfl
 theorem ex5 : g false true true = 3 := rfl
+
+theorem f_eq (h : a = true → b = true → False) : f a b = 3 := by
+  simp [f]
+  split
+  . contradiction
+  . rfl
+
+theorem ex6 : g x y z > 0 := by
+  simp [g]
+  split
+  next => decide
+  next => decide
+  next a b c h₁ h₂ => simp [f_eq h₁]
diff --git a/tests/lean/run/def20.lean b/tests/lean/run/def20.lean
index 3703500041..9e1bf81d4b 100644
--- a/tests/lean/run/def20.lean
+++ b/tests/lean/run/def20.lean
@@ -1,5 +1,3 @@
-
-
 def f : Char → Nat
 | 'a' => 0
 | 'b' => 1
@@ -38,3 +36,10 @@ def r : String × String → Nat
 
 theorem ex4 : (r ("hello", "world"), r ("world", "hello"), r ("a", "b")) = (0, 1, 2) :=
 rfl
+
+example (a b : String) (h : a.length > 10) : r (a, b) = 2 := by
+  simp [r]
+  split
+  next h => injection h with h; subst h; contradiction
+  next h => injection h with h; subst h; contradiction
+  next => decide
diff --git a/tests/lean/run/def4.lean b/tests/lean/run/def4.lean
index a7f1bed40f..c2f2e9bddf 100644
--- a/tests/lean/run/def4.lean
+++ b/tests/lean/run/def4.lean
@@ -1,25 +1,23 @@
-
-
-inductive Foo : Bool → Type
-| Z  : Foo false
-| O  : Foo false → Foo true
-| E  : Foo true → Foo false
+inductive Foo : Bool → Type where
+  | Z  : Foo false
+  | O  : Foo false → Foo true
+  | E  : Foo true → Foo false
 
 open Foo
 
 def toNat : {b : Bool} → Foo b → Nat
-| _, Z   => 0
-| _, O n => toNat n + 1
-| _, E n => toNat n + 1
+  | _, Z   => 0
+  | _, O n => toNat n + 1
+  | _, E n => toNat n + 1
 
 example : toNat (E (O Z)) = 2 :=
-rfl
+  rfl
 
 example : toNat Z = 0 :=
-rfl
+  rfl
 
 example (a : Foo false) : toNat (O a) = toNat a + 1 :=
-rfl
+  rfl
 
 example (a : Foo true) : toNat (E a) = toNat a + 1 :=
-rfl
+  rfl