From 8bda71af6f8dcdd988cfaa004c2403be7cb2162e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 11 Dec 2017 13:25:37 -0800 Subject: [PATCH] feat(library/init/meta/interactive): new `case` tactic with support for `with_cases` and tagging --- library/data/rbtree/basic.lean | 2 +- library/data/rbtree/find.lean | 6 +- library/data/rbtree/insert.lean | 4 +- library/init/meta/interactive.lean | 119 ++++++++++++++++++++++------- tests/lean/case.lean | 6 +- tests/lean/case.lean.expected.out | 1 + tests/lean/guard_names.lean | 2 +- 7 files changed, 103 insertions(+), 37 deletions(-) diff --git a/library/data/rbtree/basic.lean b/library/data/rbtree/basic.lean index 97f58c80a4..5d8397ec53 100644 --- a/library/data/rbtree/basic.lean +++ b/library/data/rbtree/basic.lean @@ -105,7 +105,7 @@ end lemma range [is_strict_weak_order α lt] {t : rbnode α} {x} : ∀ {lo hi}, is_searchable lt t lo hi → mem lt x t → lift lt lo (some x) ∧ lift lt (some x) hi := begin induction t, - case leaf f{ simp [mem], intros, trivial }, + case leaf { simp [mem], intros, trivial }, all_goals { -- red_node and black_node are identical intros lo hi h₁ h₂, cases h₁, simp only [mem] at h₂, diff --git a/library/data/rbtree/find.lean b/library/data/rbtree/find.lean index aef460499d..1ab55ad83d 100644 --- a/library/data/rbtree/find.lean +++ b/library/data/rbtree/find.lean @@ -22,14 +22,14 @@ lemma find.induction {p : rbnode α → Prop} (lt) [decidable_rel lt] : p t := begin induction t, - case leaf {assumption}, - case red_node l y r { + case leaf { assumption }, + case red_node : l y r { cases h : cmp_using lt x y, case ordering.lt { apply h₂, assumption, assumption }, case ordering.eq { apply h₃, assumption }, case ordering.gt { apply h₄, assumption, assumption }, }, - case black_node l y r { + case black_node : l y r { cases h : cmp_using lt x y, case ordering.lt { apply h₅, assumption, assumption }, case ordering.eq { apply h₆, assumption }, diff --git a/library/data/rbtree/insert.lean b/library/data/rbtree/insert.lean index d55c2abe09..fc3062658e 100644 --- a/library/data/rbtree/insert.lean +++ b/library/data/rbtree/insert.lean @@ -83,13 +83,13 @@ lemma ins.induction {p : rbnode α → Prop} begin induction t, case leaf { apply h₁ }, - case red_node a y b { + case red_node : a y b { cases h : cmp_using lt x y, case ordering.lt { apply h₂; assumption }, case ordering.eq { apply h₃; assumption }, case ordering.gt { apply h₄; assumption }, }, - case black_node a y b { + case black_node : a y b { cases h : cmp_using lt x y, case ordering.lt { by_cases get_color a = red, diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index 7469b3fc95..4402922547 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -90,15 +90,14 @@ meta def itactic : Type := tactic unit meta def propagate_tags (tac : tactic unit) : tactic unit := -focus1 $ -mcond tags_enabled - (do tag ← get_main_tag, - tac, - gs ← get_goals, - when (bnot gs.empty) $ do - new_tag ← get_main_tag, - when new_tag.empty $ set_main_tag tag) - tac +do tag ← get_main_tag, + if tag = [] then tac + else focus1 $ do + tac, + gs ← get_goals, + when (bnot gs.empty) $ do + new_tag ← get_main_tag, + when new_tag.empty $ with_enable_tags (set_main_tag tag) meta def concat_tags (tac : tactic (list (name × expr))) : tactic unit := mcond tags_enabled @@ -568,6 +567,51 @@ focus1 $ do { set_induction_tags in_tag rs } +private meta def is_case_simple_tag : tag → bool +| (`_case_simple :: _) := tt +| _ := ff + +private meta def is_case_tag : tag → option nat +| (name.mk_numeral n `_case :: _) := some n.val +| _ := none + +private meta def tag_match (t : tag) (pre : list name) : bool := +pre.is_prefix_of t.reverse && +((is_case_tag t).is_some || is_case_simple_tag t) + +private meta def collect_tagged_goals (pre : list name) : tactic (list expr) := +do gs ← get_goals, + gs.mfoldr (λ g r, do + t ← get_tag g, + if tag_match t pre then return (g::r) else return r) + [] + +private meta def find_tagged_goal_aux (pre : list name) : tactic expr := +do gs ← collect_tagged_goals pre, + match gs with + | [] := fail ("invalid `case`, there is no goal tagged with prefix " ++ to_string pre) + | [g] := return g + | gs := do + tags : list (list name) ← gs.mmap get_tag, + fail ("invalid `case`, there is more than one goal tagged with prefix " ++ to_string pre ++ ", matching tags: " ++ to_string tags) + end + +private meta def find_tagged_goal (pre : list name) : tactic expr := +match pre with +| [] := do g::gs ← get_goals, return g +| _ := + find_tagged_goal_aux pre + <|> + -- try to resolve constructor names, and try again + do env ← get_env, + pre ← pre.mmap (λ id, + (do r_id ← resolve_constant id, + if (env.inductive_type_of r_id).is_none then return id + else return r_id) + <|> return id), + find_tagged_goal_aux pre +end + private meta def find_case (goals : list expr) (ty : name) (idx : nat) (num_indices : nat) : option expr → expr → option (expr × expr) | case e := if e.has_meta_var then match e with | (mvar _ _ _) := @@ -610,33 +654,54 @@ private meta def rename_lams : expr → list name → tactic unit | _ _ := skip /-- -Focuses on the `induction`/`cases` subgoal corresponding to the given introduction rule, optionally renaming introduced locals. +Focuses on the `induction`/`cases`/`with_cases` subgoal corresponding to the given tag prefix, optionally renaming introduced locals. ``` example (n : ℕ) : n = n := begin induction n, case nat.zero { reflexivity }, - case nat.succ a ih { reflexivity } + case nat.succ : a ih { reflexivity } end ``` -/ -meta def case (ctor : parse ident) (ids : parse ident_*) (tac : itactic) : tactic unit := -do r ← result, - env ← get_env, - ctor ← resolve_constant ctor - <|> fail ("'" ++ to_string ctor ++ "' is not a constructor"), - ty ← (env.inductive_type_of ctor).to_monad - <|> fail ("'" ++ to_string ctor ++ "' is not a constructor"), - let ctors := env.constructors_of ty, - let idx := env.inductive_num_params ty + /- motive -/ 1 + - list.index_of ctor ctors, - gs ← get_goals, - (case, g) ← (find_case gs ty idx (env.inductive_num_indices ty) none r ).to_monad - <|> fail "could not find open goal of given case", - set_goals $ g :: gs.filter (≠ g), - rename_lams case ids, - solve1 tac +meta def case (pre : parse ident_*) (ids : parse $ (tk ":" *> ident_*)?) (tac : itactic) : tactic unit := +do g ← find_tagged_goal pre, + tag ← get_tag g, + let ids := ids.get_or_else [], + match is_case_tag tag with + | some n := do + gs ← get_goals, + set_goals $ g :: gs.filter (≠ g), + intro_lst ids, + let m := ids.length, + when (m < n) $ intron (n - m), + solve1 tac + | none := + match is_case_simple_tag tag with + | tt := + /- Use the old `case` implementation -/ + do r ← result, + env ← get_env, + [ctor_id] ← return pre, + ctor ← resolve_constant ctor_id + <|> fail ("'" ++ to_string ctor_id ++ "' is not a constructor"), + ty ← (env.inductive_type_of ctor).to_monad + <|> fail ("'" ++ to_string ctor ++ "' is not a constructor"), + let ctors := env.constructors_of ty, + let idx := env.inductive_num_params ty + /- motive -/ 1 + + list.index_of ctor ctors, + /- Remark: we now use `find_case` just to locate the `lambda` used in `rename_lams`. + The goal is now located using tags. -/ + (case, _) ← (find_case [g] ty idx (env.inductive_num_indices ty) none r ).to_monad + <|> fail "could not find open goal of given case", + gs ← get_goals, + set_goals $ g :: gs.filter (≠ g), + rename_lams case ids, + solve1 tac + | ff := failed + end + end /-- Assuming `x` is a variable in the local context with an inductive type, `destruct x` splits the main goal, producing one goal for each constructor of the inductive type, in which `x` is assumed to be a general instance of that constructor. In contrast to `cases`, the local context is unchanged, i.e. no elements are reverted or introduced. diff --git a/tests/lean/case.lean b/tests/lean/case.lean index 67924b9024..f96715e88e 100644 --- a/tests/lean/case.lean +++ b/tests/lean/case.lean @@ -13,9 +13,9 @@ end example (xs : list ℕ) : ℕ := begin induction xs, - case list.cons x xs { + case list.cons : x xs { cases xs, - case list.cons x xs {} + case list.cons : x xs {} } end @@ -29,6 +29,6 @@ end example (xs : list ℕ) : ℕ := begin induction xs, - case list.cons x xs ih { apply ih }, + case list.cons : x xs ih { apply ih }, case list.nil { apply 0 } end diff --git a/tests/lean/case.lean.expected.out b/tests/lean/case.lean.expected.out index 1051f1d765..aad09b3300 100644 --- a/tests/lean/case.lean.expected.out +++ b/tests/lean/case.lean.expected.out @@ -13,6 +13,7 @@ xs_tl : list ℕ ⊢ ℕ case.lean:18:4: error: solve1 tactic failed, focused goal has not been solved state: +case list.cons xs_ih x x : ℕ, xs : list ℕ ⊢ ℕ diff --git a/tests/lean/guard_names.lean b/tests/lean/guard_names.lean index 631eb57b45..de82b840bb 100644 --- a/tests/lean/guard_names.lean +++ b/tests/lean/guard_names.lean @@ -8,5 +8,5 @@ example {α : Type} (a b : tree α) : foo a = a := begin with_cases { induction a }, { admit }, - { intros l v r ih_l ih_r, trace_state, admit }, + case : l v r ih_l ih_r { trace_state, admit }, end