From e52cffd04d21420e7fb38765ad00ebe9bf4c78fa Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 6 Aug 2016 14:13:41 -0700
Subject: [PATCH] feat(library/init/meta/match_tactic): add helper tactics on
 top of match tactic

---
 library/init/meta/match_tactic.lean | 66 +++++++++++++++++++++++++++++
 tests/lean/run/match_expr.lean      | 12 ++++++
 2 files changed, 78 insertions(+)
 create mode 100644 tests/lean/run/match_expr.lean

diff --git a/library/init/meta/match_tactic.lean b/library/init/meta/match_tactic.lean
index c0fae27a94..fb27fc78a9 100644
--- a/library/init/meta/match_tactic.lean
+++ b/library/init/meta/match_tactic.lean
@@ -34,4 +34,70 @@ meta_constant match_pattern_core : transparency → pattern → expr → tactic
 meta_definition match_pattern : pattern → expr → tactic (list expr) :=
 match_pattern_core semireducible
 
+open expr
+
+/- Helper function for converting a term (λ x_1 ... x_n, t) into a pattern
+   where x_1 ... x_n are metavariables -/
+private meta_definition to_pattern_core : expr → tactic (expr × list expr)
+| (lam n bi d b) := do
+   id      ← mk_fresh_name,
+   x       ← return $ local_const id n bi d,
+   new_b   ← return $ instantiate_var b x,
+   (p, xs) ← to_pattern_core new_b,
+   return (p, x::xs)
+| e             := return (e, [])
+
+/- Given a pre-term of the form (λ x_1 ... x_n, t[x_1, ..., x_n]), converts it
+   into the pattern t[?x_1, ..., ?x_n] -/
+meta_definition pexpr_to_pattern (p : pexpr) : tactic pattern :=
+do e ← to_expr p,
+   (new_p, xs) ← to_pattern_core e,
+   mk_pattern [] xs new_p xs
+
+/- Convert pre-term into a pattern and try to match e.
+   Given p of the form (λ x_1 ... x_n, t[x_1, ..., x_n]), a successful
+   match will produce a list of length n. -/
+meta_definition match_expr (p : pexpr) (e : expr) : tactic (list expr) :=
+do new_p ← pexpr_to_pattern p,
+   match_pattern new_p e
+
+private meta_definition match_subexpr_core : pattern → list expr → tactic (list expr)
+| p []      := failed
+| p (e::es) :=
+  match_pattern p e
+  <|>
+  match_subexpr_core p es
+  <|>
+  if (is_app e = tt) then match_subexpr_core p (get_app_args e)
+  else failed
+
+/- Similar to match_expr, but it tries to match a subexpression of e.
+   Remark: the procedure does not go inside binders. -/
+meta_definition match_subexpr (p : pexpr) (e : expr) : tactic (list expr) :=
+do new_p ← pexpr_to_pattern p,
+   match_subexpr_core new_p [e]
+
+/- Match the main goal target. -/
+meta_definition match_target (p : pexpr) : tactic (list expr) :=
+target >>= match_expr p
+
+/- Match a subterm in the main goal target. -/
+meta_definition match_target_subexpr (p : pexpr) : tactic (list expr) :=
+target >>= match_subexpr p
+
+private meta_definition match_hypothesis_core : pattern → list expr → tactic (expr × list expr)
+| p []      := failed
+| p (h::hs) := do
+  h_type ← infer_type h,
+  (do r ← match_pattern p h_type, return (h, r))
+  <|>
+  match_hypothesis_core p hs
+
+/- Match hypothesis in the main goal target.
+   The result is pair (hypothesis, substitution). -/
+meta_definition match_hypothesis (p : pexpr) : tactic (expr × list expr) :=
+do ctx ← local_context,
+   new_p ← pexpr_to_pattern p,
+   match_hypothesis_core new_p ctx
+
 end tactic
diff --git a/tests/lean/run/match_expr.lean b/tests/lean/run/match_expr.lean
new file mode 100644
index 0000000000..1d33f37684
--- /dev/null
+++ b/tests/lean/run/match_expr.lean
@@ -0,0 +1,12 @@
+open tactic
+axiom Sorry : ∀ {A:Type}, A
+
+example (a b c : nat) (h₀ : c > 0) (h₁ : a > 1) (h₂ : b > 0) : a + b + c = 0 :=
+by do
+  [x, y] ← match_target_subexpr `(λ x y : nat, x + y) | failed,
+  trace "------ subterms -------",
+  trace x, trace y,
+  (h, [z]) ← match_hypothesis `(λ x : nat, x > 1) | failed,
+  trace "--- hypothesis of the form x > 1 ---",
+  trace h, trace z,
+  refine `(Sorry)