[Merged by Bors] - refactor(library/init/meta/*): refactor case tags

library/data/rbtree/insert.lean

@@ -132,16 +132,16 @@ end
 lemma is_searchable_ins {t x} [is_strict_weak_order α lt] : ∀ {lo hi} (h : is_searchable lt t lo hi), lift lt lo (some x) → lift lt (some x) hi → is_searchable lt (ins lt t x) lo hi :=
 begin
   with_cases { apply ins.induction lt t x; intros; simp! [*] at * {eta := ff}; is_searchable_tactic },
-  case is_red_lt { apply ih h_hs₁, assumption, simp [*] },
+  case is_red_lt hs₁ { apply ih h_hs₁, assumption, simp [*] },
   case is_red_eq hs₁ { apply is_searchable_of_is_searchable_of_incomp hc, assumption },
   case is_red_eq hs₂ { apply is_searchable_of_incomp_of_is_searchable hc, assumption },
-  case is_red_gt { apply ih h_hs₂, cases hi; simp [*], assumption },
+  case is_red_gt hs₂ { apply ih h_hs₂, cases hi; simp [*], assumption },
   case is_black_lt_red { apply is_searchable_balance1_node, apply ih h_hs₁, assumption, simp [*], assumption },
-  case is_black_lt_not_red { apply ih h_hs₁, assumption, simp [*] },
+  case is_black_lt_not_red hs₁ { apply ih h_hs₁, assumption, simp [*] },
   case is_black_eq hs₁ { apply is_searchable_of_is_searchable_of_incomp hc, assumption },
   case is_black_eq hs₂ { apply is_searchable_of_incomp_of_is_searchable hc, assumption },
   case is_black_gt_red { apply is_searchable_balance2_node, assumption, apply ih h_hs₂, simp [*], assumption },
-  case is_black_gt_not_red { apply ih h_hs₂, assumption, simp [*] }
+  case is_black_gt_not_red hs₂ { apply ih h_hs₂, assumption, simp [*] }
 end
 
 lemma is_searchable_mk_insert_result {c t} : is_searchable lt t none none → is_searchable lt (mk_insert_result c t) none none :=

library/init/meta/case_tag.lean

@@ -0,0 +1,289 @@
+/-
+Copyright (c) 2020 Jannis Limperg. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jannis Limperg
+-/
+prelude
+import init.meta.tactic
+
+/-!
+# Case tags
+
+Case tags are an internal mechanism used by certain tactics to communicate with
+each other. They are generated by the tactics `cases`, `induction` and
+`with_cases` ('cases-like tactics'), which generate goals corresponding to the
+'cases' of an inductive hypothesis. Each of these goals carries a case tag. They
+are consumed by the `case` tactic, which focuses on one of these cases. Their
+purpose is twofold:
+
+1. Give intuitive names to case goals. For example, when performing induction on
+   a natural number, two cases are generated: one tagged with `nat.zero` and
+   one tagged with `nat.succ`. Users can then focus on e.g. the second goal with
+   `case succ {...}`.
+2. Communicate which new hypotheses were introduced by the cases-like tactic
+   that generated the goal. For example, when performing induction on a
+   `list α`, the `cons` case introduces two hypotheses corresponding to the two
+   arguments of the `cons` constructor. `case` allows users to name these with
+   `case cons : x xs {...}`. To perform this renaming, `case` needs to know
+   which hypotheses to rename; this information is contained in the case tag for
+   the `cons` goal.
+
+## Module contents
+
+This module defines
+
+1. what a case tag is (see `case_tag`);
+2. how to render a `case_tag` as a list of names (see `render`);
+3. how to parse  a `case_tag` from a list of names (see `parse`);
+4. how to match a `case_tag` with a sequence of names given by the user
+   (see `match_tag`).
+-/
+
+namespace tactic
+namespace interactive
+
+/--
+A case tag carries the following information:
+
+1. A list of names identifying the case ('case names'). This is usually a list
+   of constructor names, one for each case split that was performed. For
+   example, the sequence of tactics `cases n; cases xs`, where `n` is a natural
+   number and `xs` is a list, will generate four cases tagged as follows:
+
+   ```
+   nat.zero, list.nil
+   nat.zero, list.cons
+   nat.succ, list.nil
+   nat.succ, list.cons
+   ```
+
+   Note: In the case tag, the case names are stored in reverse order. Thus, the
+   case names of the first case tag would be `list.nil, nat.zero`. This is
+   because when printing a goal tag (as part of a goal state), Lean prints all
+   non-internal names in reverse order.
+
+2. Information about the arguments introduced by the cases-like tactic.
+   Different tactics work slightly different in this regard:
+
+   1. The `with_cases` tactic generates goals where the target quantifies over
+      any added hypotheses. For example, `with_cases { cases xs }`, where `xs`
+      is a `list α`, will generate a target of the form `α → list α → ...` in
+      the `cons` case, where the two arguments correspond to the two arguments
+      of the `cons` constructor. Goals of this form are tagged with a `pi` case
+      tag (since the target is a pi type). In addition to the case names, it
+      contains a natural number, `num_arguments`, which specifies how many of
+      the arguments that the target quantifies over were introduced by
+      `with_cases`.
+
+      For example, given `n : ℕ` and `xs : list α`, the fourth goal generated by
+      `with_cases { cases n; induction xs }` has this form:
+
+      ```
+      ...
+      ⊢ ℕ → α → ∀ (xs' : list α), P xs' → ...
+      ```
+
+      The corresponding case tag is
+
+      ```
+      pi [`list.cons, `nat.succ] 4
+      ```
+
+      since the first four arguments of the target were introduced by
+      `with_cases {...}`.
+
+   2. The `cases` and `induction` tactics do not add arguments to the target,
+      but rather introduce them as hypotheses in the local context. Goals of
+      this form are tagged with a `hyps` case tag. In addition to the case
+      names, it contains a list of *unique* names of the hypotheses that were
+      introduced.
+
+      For example, given `xs : list α`, the second goal generated by
+      `induction xs` has this form:
+
+      ```
+      ...
+      x : α
+      xs' : list α
+      ih_xs' : P xs'
+      ⊢ ...
+      ```
+
+      The corresponding goal tag is
+
+      ```
+      hyps [`list.cons] [`<x>, `<xs'>, `<ih_xs'>]
+      ```
+
+      where ````<h>``` denotes the unique name of a hypothesis `h`.
+
+      Note: Many tactics do not preserve the unique names of hypotheses
+      (particularly those tactics that use `revert`). Therefore, a `hyps` case
+      tag is only guaranteed to be valid directly after it was generated.
+-/
+inductive case_tag
+| pi (names : list name) (num_arguments : ℕ)
+| hyps (names : list name) (arguments : list name)
+
+/--
+Display a case tag.
+-/
+protected def case_tag.to_string : case_tag → string
+| (case_tag.pi names num_arguments) :=
+  "(case_tag.pi " ++ to_string names ++ " " ++ to_string num_arguments ++ ")"
+| (case_tag.hyps names arguments) :=
+  "(case_tag.hyps " ++ to_string names ++ " " ++ to_string arguments ++ ")"
+
+namespace case_tag
+
+open name (mk_string mk_numeral)
+
+instance : has_to_string case_tag :=
+⟨case_tag.to_string⟩
+
+/--
+The constructor names associated with a case tag.
+-/
+meta def case_names : case_tag → list name
+| (pi ns _) := ns
+| (hyps ns _) := ns
+
+private meta def render_arguments (args : list name) : list name :=
+args.map (name.mk_string "_arg")
+
+/--
+Renders a case tag to a goal tag (i.e. a list of names), according to the
+following schema:
+
+- A `pi` tag with names `N₀ ... Nₙ` and number of arguments `a` is rendered as
+  ```
+  [`_case.pi.a, N₀, ..., Nₙ]
+  ```
+- A `hyps` tag with names `N₀ ... Nₙ` and argument names `A₀ ... Aₘ` is rendered
+  as
+  ```
+  [`_case.hyps, A₀._arg, ..., Aₘ._arg, N₀, ..., Nₙ]
+  ```
+-/
+meta def render : case_tag → list name
+| (pi names num_arguments) :=
+  mk_numeral (unsigned.of_nat' num_arguments) `_case.pi :: names
+| (hyps names arguments) :=
+  `_case.hyps :: render_arguments arguments ++ names
+
+/--
+Creates a `pi` case tag from an input tag `in_tag`. The `names` of the resulting
+tag are the non-internal names in `in_tag` (in the order in which they appear in
+`in_tag`). `num_arguments` is the number of arguments of the resulting tag.
+-/
+meta def from_tag_pi (in_tag : tag) (num_arguments : ℕ) : case_tag :=
+pi (in_tag.filter (λ n, ¬ n.is_internal)) num_arguments
+
+/--
+Creates a `hyps` case tag from an input tag `in_tag`. The `names` of the
+resulting tag are the non-internal names in `in_tag` (in the order in which they
+appear in `in_tag`). `arguments` is the list of unique hypothesis names of the
+resulting tag.
+-/
+meta def from_tag_hyps (in_tag : tag) (arguments : list name) : case_tag :=
+hyps (in_tag.filter (λ n, ¬ n.is_internal)) arguments
+
+private meta def parse_marker : name → option (option nat)
+| (mk_numeral n `_case.pi) := some (some n.to_nat)
+| `_case.hyps := some none
+| _ := none
+
+private meta def parse_arguments : list name → list name × list name
+| [] := ⟨[], []⟩
+| (mk_string "_arg" n :: ns) :=
+  let ⟨args, rest⟩ := parse_arguments ns in
+  ⟨n :: args, rest⟩
+| ns := ⟨[], ns⟩
+
+/--
+Parses a case tag from the list of names produced by `render`.
+-/
+meta def parse : list name → option case_tag
+| [] := none
+| (mk_numeral n `_case.pi :: ns) := do
+  guard $ ns.all (λ n, ¬ n.is_internal),
+  some $ pi ns n.to_nat
+| (`_case.hyps :: ns) := do
+  let ⟨args, ns⟩ := parse_arguments ns,
+  guard $ ns.all (λ n, ¬ n.is_internal),
+  some $ hyps ns args
+| _ := none
+
+/--
+Indicates the result of matching a list of names against the names of a case
+tag. See `match_tag`.
+-/
+inductive match_result
+| exact_match
+| fuzzy_match
+| no_match
+
+open match_result
+
+namespace match_result
+
+/--
+The 'minimum' of two match results:
+
+- If any of the arguments is `no_match`, the result is `no_match`.
+- Otherwise, if any of the arguments is `fuzzy_match`, the result is `fuzzy_match`.
+- Otherwise (iff both arguments are `exact_match`), the result is `exact_match`.
+-/
+def combine : match_result → match_result → match_result
+| exact_match exact_match := exact_match
+| exact_match fuzzy_match := fuzzy_match
+| exact_match no_match := no_match
+| fuzzy_match no_match := no_match
+| fuzzy_match _ := fuzzy_match
+| no_match _ := no_match
+
+end match_result
+
+private meta def name_match (suffix : name) (n : name) : match_result :=
+if suffix = n
+  then exact_match
+  else if suffix.is_suffix_of n
+         then fuzzy_match
+         else no_match
+
+private meta def names_match : list name → list name → match_result
+| [] [] := exact_match
+| [] _ := fuzzy_match
+| (_ :: _) [] := no_match
+| (n :: ns) (n' :: ns') := (name_match n n').combine (names_match ns ns')
+
+/--
+Match the `names` of a case tag against a user-supplied list of names `ns`. For
+this purpose, we consider the `names` in reverse order, i.e. in the order in
+which they are displayed to the user. The matching then uses the following
+rules:
+
+- If `ns` is exactly the same sequence of names as `names`, this is an exact
+  match.
+- If `ns` is a *suffix* of `names`, this is a fuzzy match. Additionally, each of
+  the names in `ns` may be a suffix of the corresponding name in `names`.
+- Otherwise, we have no match.
+
+Thus, the tag
+```
+nat.zero, list.nil
+```
+is matched by any of these tags:
+```
+nat.zero, list.nil (exact match)
+nat.zero, nil      (fuzzy match)
+zero, nil          (fuzzy match)
+nil                (fuzzy match)
+```
+-/
+meta def match_tag (ns : list name) (t : case_tag) : match_result :=
+names_match ns.reverse t.case_names
+
+end case_tag
+end interactive
+end tactic