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

feat(library/tactic/intro_tactic): make sure unused names are used if the user did not provide them

Browse source
This commit is contained in:
Leonardo de Moura 2017-03-09 16:03:18 -08:00
parent 3e757d890a
commit e875141322
10 changed files with 83 additions and 48 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/tactic/intro_tactic.cpp
View file

@ -20,7 +20,7 @@ static name mk_aux_name(local_context const & lctx, list<name> & 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);
}
}

5
src/library/tactic/intro_tactic.h
View file

@ -13,7 +13,10 @@ optional<tactic_state> 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<expr> intron(environment const & env, options const & opts, metavar_context & mctx,
expr const & mvar, unsigned n, list<name> & new_hs_names, buffer<name> & new_Hns);
optional<expr> intron(environment const & env, options const & opts, metavar_context & mctx,

19
tests/lean/cases_induction_fresh.lean Normal file
View file

@ -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

13
tests/lean/cases_induction_fresh.lean.expected.out Normal file
View file

@ -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

4
tests/lean/run/aexp.lean
View file

@ -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

2
tests/lean/run/quote_bas.lean
View file

@ -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

2
tests/lean/run/smt_tests3.lean
View file

@ -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

24
tests/lean/whnf.lean.expected.out
View file

@ -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⟩,

12
tests/lean/whnf_cache_bug.lean.expected.out
View file

@ -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⟩,

48
tests/lean/whnf_core1.lean.expected.out
View file

@ -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⟩,