From 2be69f1d564729bc954f12d112c3da045abde43e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 23 Feb 2020 19:30:33 -0800
Subject: [PATCH] test: add new induction tactic tests

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

diff --git a/tests/lean/run/induction1.lean b/tests/lean/run/induction1.lean
new file mode 100644
index 0000000000..4ea1e006b0
--- /dev/null
+++ b/tests/lean/run/induction1.lean
@@ -0,0 +1,51 @@
+@[recursor 4]
+def Or.elim2 {p q r : Prop} (major : p ∨ q) (left : p → r) (right : q → r) : r :=
+Or.elim major left right
+
+new_frontend
+
+theorem tst0 {p q : Prop } (h : p ∨ q) : q ∨ p :=
+begin
+  induction h;
+  { apply Or.inr; assumption };
+  { apply Or.inl; assumption }
+end
+
+theorem tst1 {p q : Prop } (h : p ∨ q) : q ∨ p :=
+begin
+  induction h with
+  | inr h2 => Or.inl h2
+  | inl h1 => Or.inr h1
+end
+
+theorem tst2 {p q : Prop } (h : p ∨ q) : q ∨ p :=
+begin
+  induction h using elim2 with
+  | left _  => Or.inr $ by assumption
+  | right _ => Or.inl $ by assumption
+end
+
+theorem tst3 {p q : Prop } (h : p ∨ q) : q ∨ p :=
+begin
+  induction h using elim2 with
+  | right h => Or.inl h
+  | left h  => Or.inr h
+end
+
+theorem tst4 {p q : Prop } (h : p ∨ q) : q ∨ p :=
+begin
+  induction h using elim2 with
+  | right h => ?myright
+  | left h  => ?myleft;
+  case myleft  { exact Or.inr h };
+  case myright { exact Or.inl h };
+end
+
+theorem tst5 {p q : Prop } (h : p ∨ q) : q ∨ p :=
+begin
+  induction h using elim2 with
+  | right h => Or.inl ?myright
+  | left h  => Or.inr ?myleft;
+  case myleft  assumption;
+  case myright exact h;
+end