From e8751413223e33bf92f7075c81fca2bd21c39f76 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 9 Mar 2017 16:03:18 -0800 Subject: [PATCH] feat(library/tactic/intro_tactic): make sure unused names are used if the user did not provide them --- src/library/tactic/intro_tactic.cpp | 2 +- src/library/tactic/intro_tactic.h | 5 +- tests/lean/cases_induction_fresh.lean | 19 ++++++++ .../cases_induction_fresh.lean.expected.out | 13 +++++ tests/lean/run/aexp.lean | 4 +- tests/lean/run/quote_bas.lean | 2 +- tests/lean/run/smt_tests3.lean | 2 +- tests/lean/whnf.lean.expected.out | 24 +++++----- tests/lean/whnf_cache_bug.lean.expected.out | 12 ++--- tests/lean/whnf_core1.lean.expected.out | 48 +++++++++---------- 10 files changed, 83 insertions(+), 48 deletions(-) create mode 100644 tests/lean/cases_induction_fresh.lean create mode 100644 tests/lean/cases_induction_fresh.lean.expected.out diff --git a/src/library/tactic/intro_tactic.cpp b/src/library/tactic/intro_tactic.cpp index 0338ec00b1..99fc3eece1 100644 --- a/src/library/tactic/intro_tactic.cpp +++ b/src/library/tactic/intro_tactic.cpp @@ -20,7 +20,7 @@ static name mk_aux_name(local_context const & lctx, list & given_names, na given_names = tail(given_names); return r == "_" ? lctx.get_unused_name(default_name) : r; } else { - return default_name; + return lctx.get_unused_name(default_name); } } diff --git a/src/library/tactic/intro_tactic.h b/src/library/tactic/intro_tactic.h index d05d7667da..b3f090c408 100644 --- a/src/library/tactic/intro_tactic.h +++ b/src/library/tactic/intro_tactic.h @@ -13,7 +13,10 @@ optional intron(unsigned n, tactic_state const & s); The new hypotheses "user names" are generated using \c new_hs_names (when available). After execution, the buffer \c new_Hns stores the new interal names for the new hypotheses. - \remark new_hs_names is an input/output parameter. The procedure will "consume" n elements from the list. */ + \remark new_hs_names is an input/output parameter. The procedure will "consume" n elements from the list. + + \remark if new_hs_names doesn't have sufficient names, then the procedure + will create unused local context names using the binder names. */ optional intron(environment const & env, options const & opts, metavar_context & mctx, expr const & mvar, unsigned n, list & new_hs_names, buffer & new_Hns); optional intron(environment const & env, options const & opts, metavar_context & mctx, diff --git a/tests/lean/cases_induction_fresh.lean b/tests/lean/cases_induction_fresh.lean new file mode 100644 index 0000000000..c3319a4348 --- /dev/null +++ b/tests/lean/cases_induction_fresh.lean @@ -0,0 +1,19 @@ +example (p q r s: Prop): p ∧ q → r ∧ s → s ∧ q := +begin + intros h1 h2, + cases h1, + cases h2, + trace_state, + constructor; assumption +end + +print "------------" + +example (p q r s: Prop): p ∧ q → r ∧ s → s ∧ q := +begin + intros h1 h2, + induction h1, + induction h2, + trace_state, + constructor; assumption +end diff --git a/tests/lean/cases_induction_fresh.lean.expected.out b/tests/lean/cases_induction_fresh.lean.expected.out new file mode 100644 index 0000000000..6bcd41bc57 --- /dev/null +++ b/tests/lean/cases_induction_fresh.lean.expected.out @@ -0,0 +1,13 @@ +p q r s : Prop, +a : p, +a_1 : q, +a_2 : r, +a_3 : s +⊢ s ∧ q +------------ +p q r s : Prop, +a : p, +a_1 : q, +a_2 : r, +a_3 : s +⊢ s ∧ q diff --git a/tests/lean/run/aexp.lean b/tests/lean/run/aexp.lean index 96a60a33ad..e8d8362ed8 100644 --- a/tests/lean/run/aexp.lean +++ b/tests/lean/run/aexp.lean @@ -58,13 +58,13 @@ meta def not_done : tactic unit := fail_if_success now lemma aval_asimp_const (a : aexp) (s : state) : aval (asimp_const a) s = aval a s := begin [smt] induction a, - all_goals {destruct (asimp_const a), all_goals {destruct (asimp_const a_1), eblast}} + all_goals {destruct (asimp_const a_1), all_goals {destruct (asimp_const a_2), eblast}} end lemma ex2 (a : aexp) (s : state) : aval (asimp_const a) s = aval a s := begin [smt] induction a, - all_goals {destruct (asimp_const a), all_goals {destruct (asimp_const a_1), eblast_using [asimp_const, aval]}} + all_goals {destruct (asimp_const a_1), all_goals {destruct (asimp_const a_2), eblast_using [asimp_const, aval]}} end end imp diff --git a/tests/lean/run/quote_bas.lean b/tests/lean/run/quote_bas.lean index 7ec2db38cc..ccef44518d 100644 --- a/tests/lean/run/quote_bas.lean +++ b/tests/lean/run/quote_bas.lean @@ -54,7 +54,7 @@ end begin induction e, reflexivity, - { cases v with v₁, cases v₁, all_goals {simp} }, + { cases v_1 with v₁, cases v₁, all_goals {simp} }, { simp_using_hs } end diff --git a/tests/lean/run/smt_tests3.lean b/tests/lean/run/smt_tests3.lean index 61ef65195c..7815a0371d 100644 --- a/tests/lean/run/smt_tests3.lean +++ b/tests/lean/run/smt_tests3.lean @@ -7,7 +7,7 @@ begin induction a, dsimp [f], intro x, contradiction, dsimp [f], - change nat.succ (f a) ≠ 0, + change nat.succ (f a_1) ≠ 0, apply nat.succ_ne_zero end diff --git a/tests/lean/whnf.lean.expected.out b/tests/lean/whnf.lean.expected.out index 2250065628..fbe027a2f7 100644 --- a/tests/lean/whnf.lean.expected.out +++ b/tests/lean/whnf.lean.expected.out @@ -1,24 +1,24 @@ succ ((⟨nat.rec - ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), + ⟨(λ (a_1 : ℕ) (_F : nat.below a_1) (a : ℕ), (λ (a a_1 : ℕ) (_F : nat.below a_1), nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (succ a_1)), succ ((_F^.fst)^.fst a)) + (λ (a_2 : ℕ) (_F : nat.below (succ a_2)), succ ((_F^.fst)^.fst a)) _F) - a_1 a + a_1 _F) 0 punit.star, punit.star⟩ (λ (a : ℕ) (ih_1 : pprod ((λ (a : ℕ), ℕ → ℕ) a) (nat.below a)), - ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), + ⟨(λ (a_1 : ℕ) (_F : nat.below a_1) (a : ℕ), (λ (a a_1 : ℕ) (_F : nat.below a_1), nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (succ a_1)), succ ((_F^.fst)^.fst a)) + (λ (a_2 : ℕ) (_F : nat.below (succ a_2)), succ ((_F^.fst)^.fst a)) _F) - a_1 a + a_1 _F) (succ a) ⟨ih_1, punit.star⟩, @@ -29,25 +29,25 @@ succ 3 succ ((⟨nat.rec - ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), + ⟨(λ (a_1 : ℕ) (_F : nat.below a_1) (a : ℕ), (λ (a a_1 : ℕ) (_F : nat.below a_1), nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (succ a_1)), succ ((_F^.fst)^.fst a)) + (λ (a_2 : ℕ) (_F : nat.below (succ a_2)), succ ((_F^.fst)^.fst a)) _F) - a_1 a + a_1 _F) 0 punit.star, punit.star⟩ (λ (a : ℕ) (ih_1 : pprod ((λ (a : ℕ), ℕ → ℕ) a) (nat.below a)), - ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), + ⟨(λ (a_1 : ℕ) (_F : nat.below a_1) (a : ℕ), (λ (a a_1 : ℕ) (_F : nat.below a_1), nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (succ a_1)), succ ((_F^.fst)^.fst a)) + (λ (a_2 : ℕ) (_F : nat.below (succ a_2)), succ ((_F^.fst)^.fst a)) _F) - a_1 a + a_1 _F) (succ a) ⟨ih_1, punit.star⟩, diff --git a/tests/lean/whnf_cache_bug.lean.expected.out b/tests/lean/whnf_cache_bug.lean.expected.out index 3476f290bf..98c16b6e4c 100644 --- a/tests/lean/whnf_cache_bug.lean.expected.out +++ b/tests/lean/whnf_cache_bug.lean.expected.out @@ -1,25 +1,25 @@ ?m_1 nat.succ ((⟨nat.rec - ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), + ⟨(λ (a_1 : ℕ) (_F : nat.below a_1) (a : ℕ), (λ (a a_1 : ℕ) (_F : nat.below a_1), nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F^.fst)^.fst a)) + (λ (a_2 : ℕ) (_F : nat.below (nat.succ a_2)), nat.succ ((_F^.fst)^.fst a)) _F) - a_1 a + a_1 _F) 0 punit.star, punit.star⟩ (λ (a : ℕ) (ih_1 : pprod ((λ (a : ℕ), ℕ → ℕ) a) (nat.below a)), - ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), + ⟨(λ (a_1 : ℕ) (_F : nat.below a_1) (a : ℕ), (λ (a a_1 : ℕ) (_F : nat.below a_1), nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F^.fst)^.fst a)) + (λ (a_2 : ℕ) (_F : nat.below (nat.succ a_2)), nat.succ ((_F^.fst)^.fst a)) _F) - a_1 a + a_1 _F) (nat.succ a) ⟨ih_1, punit.star⟩, diff --git a/tests/lean/whnf_core1.lean.expected.out b/tests/lean/whnf_core1.lean.expected.out index 0b1e48c7bb..2ccf7fece4 100644 --- a/tests/lean/whnf_core1.lean.expected.out +++ b/tests/lean/whnf_core1.lean.expected.out @@ -1,48 +1,48 @@ nat.succ ((⟨nat.rec - ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), + ⟨(λ (a_1 : ℕ) (_F : nat.below a_1) (a : ℕ), (λ (a a_1 : ℕ) (_F : nat.below a_1), nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F^.fst)^.fst a)) + (λ (a_2 : ℕ) (_F : nat.below (nat.succ a_2)), nat.succ ((_F^.fst)^.fst a)) _F) - a_1 a + a_1 _F) 0 punit.star, punit.star⟩ (λ (a : ℕ) (ih_1 : pprod ((λ (a : ℕ), ℕ → ℕ) a) (nat.below a)), - ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), + ⟨(λ (a_1 : ℕ) (_F : nat.below a_1) (a : ℕ), (λ (a a_1 : ℕ) (_F : nat.below a_1), nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F^.fst)^.fst a)) + (λ (a_2 : ℕ) (_F : nat.below (nat.succ a_2)), nat.succ ((_F^.fst)^.fst a)) _F) - a_1 a + a_1 _F) (nat.succ a) ⟨ih_1, punit.star⟩, ⟨ih_1, punit.star⟩⟩) ((⟨nat.rec - ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), + ⟨(λ (a_1 : ℕ) (_F : nat.below a_1) (a : ℕ), (λ (a a_1 : ℕ) (_F : nat.below a_1), nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F^.fst)^.fst a)) + (λ (a_2 : ℕ) (_F : nat.below (nat.succ a_2)), nat.succ ((_F^.fst)^.fst a)) _F) - a_1 a + a_1 _F) 0 punit.star, punit.star⟩ (λ (a : ℕ) (ih_1 : pprod ((λ (a : ℕ), ℕ → ℕ) a) (nat.below a)), - ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), + ⟨(λ (a_1 : ℕ) (_F : nat.below a_1) (a : ℕ), (λ (a a_1 : ℕ) (_F : nat.below a_1), nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F^.fst)^.fst a)) + (λ (a_2 : ℕ) (_F : nat.below (nat.succ a_2)), nat.succ ((_F^.fst)^.fst a)) _F) - a_1 a + a_1 _F) (nat.succ a) ⟨ih_1, punit.star⟩, @@ -54,49 +54,49 @@ nat.succ a) nat.succ ((⟨nat.rec - ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), + ⟨(λ (a_1 : ℕ) (_F : nat.below a_1) (a : ℕ), (λ (a a_1 : ℕ) (_F : nat.below a_1), nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F^.fst)^.fst a)) + (λ (a_2 : ℕ) (_F : nat.below (nat.succ a_2)), nat.succ ((_F^.fst)^.fst a)) _F) - a_1 a + a_1 _F) 0 punit.star, punit.star⟩ (λ (a : ℕ) (ih_1 : pprod ((λ (a : ℕ), ℕ → ℕ) a) (nat.below a)), - ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), + ⟨(λ (a_1 : ℕ) (_F : nat.below a_1) (a : ℕ), (λ (a a_1 : ℕ) (_F : nat.below a_1), nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F^.fst)^.fst a)) + (λ (a_2 : ℕ) (_F : nat.below (nat.succ a_2)), nat.succ ((_F^.fst)^.fst a)) _F) - a_1 a + a_1 _F) (nat.succ a) ⟨ih_1, punit.star⟩, ⟨ih_1, punit.star⟩⟩) ((⟨nat.rec - ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), + ⟨(λ (a_1 : ℕ) (_F : nat.below a_1) (a : ℕ), (λ (a a_1 : ℕ) (_F : nat.below a_1), nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F^.fst)^.fst a)) + (λ (a_2 : ℕ) (_F : nat.below (nat.succ a_2)), nat.succ ((_F^.fst)^.fst a)) _F) - a_1 a + a_1 _F) 0 punit.star, punit.star⟩ (λ (a : ℕ) (ih_1 : pprod ((λ (a : ℕ), ℕ → ℕ) a) (nat.below a)), - ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), + ⟨(λ (a_1 : ℕ) (_F : nat.below a_1) (a : ℕ), (λ (a a_1 : ℕ) (_F : nat.below a_1), nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F^.fst)^.fst a)) + (λ (a_2 : ℕ) (_F : nat.below (nat.succ a_2)), nat.succ ((_F^.fst)^.fst a)) _F) - a_1 a + a_1 _F) (nat.succ a) ⟨ih_1, punit.star⟩,