feat(library/init/meta): add 'constructor', 'split', 'left', 'right', 'constructor_idx' tactics

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

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

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