michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean/elaborator): distribute application over choice, this feature improves the support for overloaded aliases

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-24 23:43:40 -07:00
parent 905a1095f9
commit 15c1e39f88
2 changed files with 53 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
src/frontends/lean/elaborator.cpp
View file

@ -736,7 +736,35 @@ public:
return update_app(e, app_fn(e), m);
}
bool is_choice_app(expr const & e) {
expr const & f = get_app_fn(e);
return is_choice(f) || (is_explicit(f) && is_choice(get_explicit_arg(f)));
}
/** \brief Process ((choice f_1 ... f_n) a_1 ... a_k) as
(choice (f_1 a_1 ... a_k) ... (f_n a_1 ... a_k))
*/
expr visit_choice_app(expr const & e) {
buffer<expr> args;
expr f = get_app_rev_args(e, args);
bool expl = is_explicit(f);
if (expl)
f = get_explicit_arg(f);
lean_assert(is_choice(f));
buffer<expr> new_choices;
unsigned num = get_num_choices(f);
for (unsigned i = 0; i < num; i++) {
expr f_i = get_choice(f, i);
if (expl)
f_i = mk_explicit(f_i);
new_choices.push_back(mk_rev_app(f_i, args));
}
return visit_choice(mk_choice(new_choices.size(), new_choices.data()), none_expr());
}
expr visit_app(expr const & e) {
if (is_choice_app(e))
return visit_choice_app(e);
bool expl = is_explicit(get_app_fn(e));
expr f = visit(app_fn(e));
auto f_t = ensure_fun(f);

25
tests/lean/run/nat_bug.lean Normal file
View file

@ -0,0 +1,25 @@
import logic decidable
using decidable
inductive nat : Type :=
| zero : nat
| succ : nat → nat
theorem induction_on {P : nat → Prop} (a : nat) (H1 : P zero) (H2 : ∀ (n : nat) (IH : P n), P (succ n)) : P a
:= nat_rec H1 H2 a
definition pred (n : nat) := nat_rec zero (fun m x, m) n
theorem pred_zero : pred zero = zero := refl _
theorem pred_succ (n : nat) : pred (succ n) = n := refl _
theorem zero_or_succ (n : nat) : n = zero ∨ n = succ (pred n)
:= induction_on n
(or_intro_left _ (refl zero))
(take m IH, or_intro_right _
(show succ m = succ (pred (succ m)), from congr2 succ (symm (pred_succ m))))
theorem zero_or_succ2 (n : nat) : n = zero ∨ n = succ (pred n)
:= @induction_on _ n
(or_intro_left _ (refl zero))
(take m IH, or_intro_right _
(show succ m = succ (pred (succ m)), from congr2 succ (symm (pred_succ m))))