From bf5cf18d8d282fca4908d69d1f15658dc7642ace Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 18 Jun 2016 12:40:21 -0700
Subject: [PATCH] feat(library/init/meta): add 'constructor', 'split', 'left',
 'right', 'constructor_idx' tactics

---
 library/init/meta/constructor_tactic.lean | 60 +++++++++++++++++++++++
 library/init/meta/default.lean            |  2 +-
 tests/lean/run/constructor1.lean          | 19 +++++++
 3 files changed, 80 insertions(+), 1 deletion(-)
 create mode 100644 library/init/meta/constructor_tactic.lean
 create mode 100644 tests/lean/run/constructor1.lean

diff --git a/library/init/meta/constructor_tactic.lean b/library/init/meta/constructor_tactic.lean
new file mode 100644
index 0000000000..d28ed1b7e9
--- /dev/null
+++ b/library/init/meta/constructor_tactic.lean
@@ -0,0 +1,60 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import init.meta.tactic
+
+namespace tactic
+open bool option list
+
+private meta_definition get_constructors_for (e : expr) : tactic (list name) :=
+do env ← get_env,
+   I   ← return (expr.const_name (expr.get_app_fn e)),
+   when (environment.is_inductive env I = ff) (fail "constructor tactic failed, target is not an inductive datatype"),
+   return (environment.constructors_of env I)
+
+private meta_definition try_constructors : list name → tactic unit
+| []      := fail "constructor tactic failed, none of the constructors is applicable"
+| (c::cs) :=
+  do { mk_const c >>= apply } <|> try_constructors cs
+
+meta_definition constructor : tactic unit :=
+do tgt ← target,
+   cs  ← get_constructors_for tgt,
+   try_constructors cs
+
+meta_definition left : tactic unit :=
+do tgt ← target,
+   cs  ← get_constructors_for tgt,
+   match cs with
+   | [c₁, c₂] := mk_const c₁ >>= apply
+   | _        := fail "left tactic failed, target is not an inductive datatype with two constructors"
+   end
+
+meta_definition right : tactic unit :=
+do tgt ← target,
+   cs  ← get_constructors_for tgt,
+   match cs with
+   | [c₁, c₂] := mk_const c₂ >>= apply
+   | _        := fail "left tactic failed, target is not an inductive datatype with two constructors"
+   end
+
+meta_definition constructor_idx (idx : nat) : tactic unit :=
+do tgt ← target,
+   cs  ← get_constructors_for tgt,
+   match nth cs (idx - 1) with
+   | some c := mk_const c >>= apply
+   | none   := fail "constructor_idx tactic failed, target is an inductive datatype, but it does not have sufficient constructors"
+   end
+
+meta_definition split : tactic unit :=
+do tgt ← target,
+   cs  ← get_constructors_for tgt,
+   match cs with
+   | [c] := mk_const c >>= apply
+   | _   := fail "split tactic failed, target is not an inductive datatype with only one constructor"
+   end
+
+end tactic
diff --git a/library/init/meta/default.lean b/library/init/meta/default.lean
index e1f110f2f3..68fff9268b 100644
--- a/library/init/meta/default.lean
+++ b/library/init/meta/default.lean
@@ -6,4 +6,4 @@ Authors: Leonardo de Moura
 prelude
 import init.meta.name init.meta.options init.meta.format init.meta.rb_map
 import init.meta.level init.meta.expr init.meta.base_tactic init.meta.environment
-import init.meta.tactic init.meta.contradiction_tactic
+import init.meta.tactic init.meta.contradiction_tactic init.meta.constructor_tactic
diff --git a/tests/lean/run/constructor1.lean b/tests/lean/run/constructor1.lean
new file mode 100644
index 0000000000..616710a528
--- /dev/null
+++ b/tests/lean/run/constructor1.lean
@@ -0,0 +1,19 @@
+open tactic
+
+example (p q : Prop) : p → q → p ∧ q :=
+by do intros, constructor, assumption, assumption
+
+example (p q : Prop) : p → q → p ∧ q :=
+by do intros, split, assumption, assumption
+
+example (p q : Prop) : p → p ∨ q :=
+by do intros, left, assumption
+
+example (p q : Prop) : q → p ∨ q :=
+by do intros, right, assumption
+
+example (p q : Prop) : p → p ∨ q :=
+by do intros, constructor_idx 1, assumption
+
+example (p q : Prop) : q → p ∨ q :=
+by do intros, constructor_idx 2, assumption