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

fix(kernel/inductive): bug in eliminator for recursive datatypes in Prop

Browse source
This commit is contained in:
Leonardo de Moura 2014-11-06 14:03:28 -08:00
parent be52d950f0
commit af88e34588
3 changed files with 47 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
src/kernel/inductive/inductive.cpp
View file

@ -768,22 +768,20 @@ struct add_inductive_fn {
i++;
}
buffer<expr> v;
if (m_dep_elim) {
for (unsigned i = 0; i < u.size(); i++) {
expr u_i = u[i];
expr u_i_ty = whnf(mlocal_type(u_i));
buffer<expr> xs;
while (is_pi(u_i_ty)) {
expr x = mk_local_for(u_i_ty);
xs.push_back(x);
u_i_ty = whnf(instantiate(binding_body(u_i_ty), x));
}
buffer<expr> it_indices;
unsigned it_idx = get_I_indices(u_i_ty, it_indices);
expr elim_app = mk_constant(get_elim_name(it_idx), ls);
elim_app = mk_app(mk_app(mk_app(mk_app(mk_app(elim_app, m_param_consts), C), e), it_indices), mk_app(u_i, xs));
v.push_back(Fun(xs, elim_app));
for (unsigned i = 0; i < u.size(); i++) {
expr u_i = u[i];
expr u_i_ty = whnf(mlocal_type(u_i));
buffer<expr> xs;
while (is_pi(u_i_ty)) {
expr x = mk_local_for(u_i_ty);
xs.push_back(x);
u_i_ty = whnf(instantiate(binding_body(u_i_ty), x));
}
buffer<expr> it_indices;
unsigned it_idx = get_I_indices(u_i_ty, it_indices);
expr elim_app = mk_constant(get_elim_name(it_idx), ls);
elim_app = mk_app(mk_app(mk_app(mk_app(mk_app(elim_app, m_param_consts), C), e), it_indices), mk_app(u_i, xs));
v.push_back(Fun(xs, elim_app));
}
expr e_app = mk_app(mk_app(mk_app(e[minor_idx], b), u), v);
expr comp_rhs = Fun(m_param_consts, Fun(C, Fun(e, Fun(b, Fun(u, e_app)))));

22
tests/lean/acc_rec_bug.lean Normal file
View file

@ -0,0 +1,22 @@
import logic
inductive acc {A : Type} (R : A → A → Prop) : A → Prop :=
intro : ∀x, (∀ y, R y x → acc R y) → acc R x
variables {A : Type} (R : A → A → Prop) (C : A → Type) (x₁ : A) (ac : ∀y, R y x₁ → acc R y)
variable F : Πx, (Πy, R y x → C y) → C x
eval @acc.rec A R C (λ (x₂ : A)
(ac : ∀y, R y x₂ → acc R y)
(iH : Πy, R y x₂ → C y),
F x₂ iH) x₁ (acc.intro x₁ ac)
check @acc.rec A R C (λ (x₂ : A)
(ac : ∀y, R y x₂ → acc R y)
(iH : Πy, R y x₂ → C y),
F x₂ iH) x₁ (acc.intro x₁ ac)
check F x₁
(λ (y : A) (a : R y x₁),
acc.rec (λ (x₂ : A) (ac : ∀ (y : A), R y x₂ → acc R y) (iH : Π (y : A), R y x₂ → C y), F x₂ iH)
(ac y a))

12
tests/lean/acc_rec_bug.lean.expected.out Normal file
View file

@ -0,0 +1,12 @@
F x₁
(λ (y : A) (a : R y x₁),
acc.rec (λ (x₂ : A) (ac : ∀ (y : A), R y x₂ → acc R y) (iH : Π (y : A), R y x₂ → C y), F x₂ iH)
(ac y a))
acc.rec (λ (x₂ : A) (ac : ∀ (y : A), R y x₂ → acc R y) (iH : Π (y : A), R y x₂ → C y), F x₂ iH)
(acc.intro x₁ ac) :
C x₁
F x₁
(λ (y : A) (a : R y x₁),
acc.rec (λ (x₂ : A) (ac : ∀ (y : A), R y x₂ → acc R y) (iH : Π (y : A), R y x₂ → C y), F x₂ iH)
(ac y a)) :
C x₁