max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/init/meta/interactive): remove buggy generalizing param from with_cases

Browse source
This commit is contained in:
Leonardo de Moura 2017-12-11 16:16:57 -08:00
parent b778d77c0c
commit 533ddc0279
4 changed files with 83 additions and 46 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
doc/changes.md
View file

@ -48,8 +48,6 @@ master branch (aka work in progress branch)
and reverts any new hypothesis in the resulting subgoals. `with_cases` also enable "goal tagging".
Remark: `induction` and `cases` tag goals using constructor names. `apply` and `constructor` tag goals
using parameter names. The `case` tactic can select goals using tags.
`with_cases generalizing id_1 ... id_n { t }` reverts hypotheses `id_1` ... `id_n` before executing `t`.
The hypotheses are automatically re-introduced by `case`. The user can optionally rename them at each `case`.
* Add `cases_matching p` tactic for applying the `cases` tactic to a hypothesis `h : t` s.t.
`t` matches the pattern `p`. Alternative versions: `cases_matching* p` and `cases_matching [p_1, ..., p_n]`.

66
library/data/rbtree/insert.lean
View file

@ -408,12 +408,12 @@ variable [is_strict_weak_order α lt]
lemma find_balance1_lt {l r t v x y lo hi}
(h : lt x y)
: ∀ (hl : is_searchable lt l lo (some v))
(hr : is_searchable lt r (some v) (some y))
(ht : is_searchable lt t (some y) hi),
find lt (balance1 l v r y t) x = find lt (red_node l v r) x :=
(hl : is_searchable lt l lo (some v))
(hr : is_searchable lt r (some v) (some y))
(ht : is_searchable lt t (some y) hi)
: find lt (balance1 l v r y t) x = find lt (red_node l v r) x :=
begin
with_cases { apply balance.cases l v r; intros; simp [*]; is_searchable_tactic },
with_cases { revert hl hr ht, apply balance.cases l v r; intros; simp [*]; is_searchable_tactic },
case red_left : _ _ _ z r { apply weak_trichotomous lt z x; intros; simp [*] },
case red_right : l_left l_val l_right z r {
with_cases { apply weak_trichotomous lt z x; intro h' },
@ -437,12 +437,12 @@ end
lemma find_balance1_gt {l r t v x y lo hi}
(h : lt y x)
: ∀ (hl : is_searchable lt l lo (some v))
(hr : is_searchable lt r (some v) (some y))
(ht : is_searchable lt t (some y) hi),
find lt (balance1 l v r y t) x = find lt t x :=
(hl : is_searchable lt l lo (some v))
(hr : is_searchable lt r (some v) (some y))
(ht : is_searchable lt t (some y) hi)
: find lt (balance1 l v r y t) x = find lt t x :=
begin
with_cases { apply balance.cases l v r; intros; simp [*]; is_searchable_tactic },
with_cases { revert hl hr ht, apply balance.cases l v r; intros; simp [*]; is_searchable_tactic },
case red_left : _ _ _ z {
have := trans_of lt (lo_lt_hi hr) h, simp [*] },
case red_right : _ _ _ z {
@ -460,13 +460,13 @@ begin
end
lemma find_balance1_eqv {l r t v x y lo hi}
(h : ¬ lt x y ∧ ¬ lt y x) :
∀ (hl : is_searchable lt l lo (some v))
(hr : is_searchable lt r (some v) (some y))
(ht : is_searchable lt t (some y) hi),
find lt (balance1 l v r y t) x = some y :=
(h : ¬ lt x y ∧ ¬ lt y x)
(hl : is_searchable lt l lo (some v))
(hr : is_searchable lt r (some v) (some y))
(ht : is_searchable lt t (some y) hi)
: find lt (balance1 l v r y t) x = some y :=
begin
with_cases { apply balance.cases l v r; intros; simp [*]; is_searchable_tactic },
with_cases { revert hl hr ht, apply balance.cases l v r; intros; simp [*]; is_searchable_tactic },
case red_left : _ _ _ z {
have : lt z x := lt_of_lt_of_incomp (lo_lt_hi hr) h.swap,
simp [*] },
@ -489,12 +489,12 @@ end
lemma find_balance2_lt {l v r t x y lo hi}
(h : lt x y)
: ∀ (hl : is_searchable lt l (some y) (some v))
(hr : is_searchable lt r (some v) hi)
(ht : is_searchable lt t lo (some y)),
find lt (balance2 l v r y t) x = find lt t x :=
(hl : is_searchable lt l (some y) (some v))
(hr : is_searchable lt r (some v) hi)
(ht : is_searchable lt t lo (some y))
: find lt (balance2 l v r y t) x = find lt t x :=
begin
with_cases { apply balance.cases l v r; intros; simp [*]; is_searchable_tactic },
with_cases { revert hl hr ht, apply balance.cases l v r; intros; simp [*]; is_searchable_tactic },
case red_left { have := trans h (lo_lt_hi hl_hs₁), simp [*] },
case red_right { have := trans h (lo_lt_hi hl), simp [*] }
end
@ -511,13 +511,13 @@ begin
end
lemma find_balance2_gt {l v r t x y lo hi}
(h : lt y x) :
∀ (hl : is_searchable lt l (some y) (some v))
(hr : is_searchable lt r (some v) hi)
(ht : is_searchable lt t lo (some y)),
find lt (balance2 l v r y t) x = find lt (red_node l v r) x :=
(h : lt y x)
(hl : is_searchable lt l (some y) (some v))
(hr : is_searchable lt r (some v) hi)
(ht : is_searchable lt t lo (some y))
: find lt (balance2 l v r y t) x = find lt (red_node l v r) x :=
begin
with_cases { apply balance.cases l v r; intros; simp [*]; is_searchable_tactic },
with_cases { revert hl hr ht, apply balance.cases l v r; intros; simp [*]; is_searchable_tactic },
case red_left : _ val _ z {
with_cases { apply weak_trichotomous lt val x; intro h'; simp [*] },
case is_lt { apply weak_trichotomous lt z x; intros; simp [*] },
@ -540,13 +540,13 @@ begin
end
lemma find_balance2_eqv {l v r t x y lo hi}
(h : ¬ lt x y ∧ ¬ lt y x) :
∀ (hl : is_searchable lt l (some y) (some v))
(hr : is_searchable lt r (some v) hi)
(ht : is_searchable lt t lo (some y)),
find lt (balance2 l v r y t) x = some y :=
(h : ¬ lt x y ∧ ¬ lt y x)
(hl : is_searchable lt l (some y) (some v))
(hr : is_searchable lt r (some v) hi)
(ht : is_searchable lt t lo (some y))
: find lt (balance2 l v r y t) x = some y :=
begin
with_cases { apply balance.cases l v r; intros; simp [*]; is_searchable_tactic },
with_cases { revert hl hr ht, apply balance.cases l v r; intros; simp [*]; is_searchable_tactic },
case red_left { have := lt_of_incomp_of_lt h (lo_lt_hi hl_hs₁), simp [*] },
case red_right { have := lt_of_incomp_of_lt h (lo_lt_hi hl), simp [*] }
end

20
library/init/meta/interactive.lean
View file

@ -401,16 +401,16 @@ private meta def collect_hyps_uids : tactic name_set :=
do ctx ← local_context,
return $ ctx.foldl (λ r h, r.insert h.local_uniq_name) mk_name_set
private meta def revert_new_hyps (num_reverted : nat) (input_hyp_uids : name_set) : tactic unit :=
private meta def revert_new_hyps (input_hyp_uids : name_set) : tactic unit :=
do ctx ← local_context,
let to_revert := ctx.foldr (λ h r, if input_hyp_uids.contains h.local_uniq_name then r else h::r) [],
tag ← get_main_tag,
m ← revert_lst to_revert,
set_main_tag (mk_num_name `_case (m + num_reverted) :: tag)
set_main_tag (mk_num_name `_case m :: tag)
/--
Apply `t` to main goal, and revert any new hypothesis in the generated goals,
and tag generated goals when using supported tactics such as: `induction`, `apply`, ...
and tag generated goals when using supported tactics such as: `induction`, `apply`, `cases`, `constructor`, ...
This tactic is useful for writing robust proof scripts that are not sensitive
to the name generation strategy used by `t`.
@ -426,13 +426,11 @@ end
TODO(Leo): improve docstring
-/
meta def with_cases (revert : parse $ (tk "generalizing" *> ident*)?) (t : itactic) : tactic unit :=
do -- revert `generalizing` params
n ← mmap tactic.get_local (revert.get_or_else []) >>= revert_lst,
with_enable_tags $ focus1 $ do
input_hyp_uids ← collect_hyps_uids,
t,
all_goals (revert_new_hyps n input_hyp_uids)
meta def with_cases (t : itactic) : tactic unit :=
with_enable_tags $ focus1 $ do
input_hyp_uids ← collect_hyps_uids,
t,
all_goals (revert_new_hyps input_hyp_uids)
private meta def get_type_name (e : expr) : tactic name :=
do e_type ← infer_type e >>= whnf,
@ -679,10 +677,10 @@ do g ← find_tagged_goal pre,
let ids := ids.get_or_else [],
match is_case_tag tag with
| some n := do
let m := ids.length,
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 :=

41
tests/lean/run/with_cases1.lean Normal file
View file

@ -0,0 +1,41 @@
example (n : nat) (m : nat) : n > m → m < n :=
begin
with_cases { revert m, induction n },
case nat.zero : m' { show 0 > m' → m' < 0, admit },
case nat.succ : n' ih m' { show nat.succ n' > m' → m' < nat.succ n', admit }
end
example (n : nat) (m : nat) : n > m → m < n :=
begin
with_cases { revert m, induction n },
case nat.zero { show ∀ m, 0 > m → m < 0, admit },
case nat.succ { show ∀ m, nat.succ n_n > m → m < nat.succ n_n, admit }
end
example (n : nat) (m : nat) : n > m → m < n :=
begin
with_cases { induction n generalizing m },
case nat.zero { show 0 > m → m < 0, admit },
case nat.succ { show nat.succ n_n > m → m < nat.succ n_n, admit }
end
example (n : nat) (m : nat) : n > m → m < n :=
begin
with_cases { induction n generalizing m },
case nat.zero : m' { show 0 > m' → m' < 0, admit },
case nat.succ : n' ih m' { show nat.succ n' > m' → m' < nat.succ n', admit }
end
example (n : nat) (m : nat) : n > m → m < n :=
begin
with_cases { induction n generalizing m },
case nat.zero : m' { show 0 > m' → m' < 0, admit },
case nat.succ : n' ih { show nat.succ n' > m → m < nat.succ n', admit }
end
example (n : nat) (m : nat) : n > m → m < n :=
begin
with_cases { induction n generalizing m },
case nat.zero { show 0 > m → m < 0, admit },
case nat.succ : n' ih { show nat.succ n' > m → m < nat.succ n', admit }
end