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

fix(kernel/quotient/quotient): bug in reduction rule for quot.ind

Browse source
This commit is contained in:
Leonardo de Moura 2015-05-09 00:04:46 -07:00
parent 4e35afedcc
commit d217655a62
3 changed files with 15 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/kernel/quotient/quotient.cpp
View file

@ -59,10 +59,13 @@ optional<pair<expr, constraint_seq>> quotient_normalizer_extension::operator()(e
if (!ext.m_initialized) if (!ext.m_initialized)
return none_ecs(); return none_ecs();
unsigned mk_pos; unsigned mk_pos;
unsigned arg_pos;
if (const_name(fn) == *g_quotient_lift) { if (const_name(fn) == *g_quotient_lift) {
mk_pos = 5; mk_pos = 5;
arg_pos = 3;
} else if (const_name(fn) == *g_quotient_ind) { } else if (const_name(fn) == *g_quotient_ind) {
mk_pos = 4; mk_pos = 4;
arg_pos = 3;
} else { } else {
return none_ecs(); return none_ecs();
} }
@ -80,7 +83,7 @@ optional<pair<expr, constraint_seq>> quotient_normalizer_extension::operator()(e
if (const_name(mk_fn) != *g_quotient_mk) if (const_name(mk_fn) != *g_quotient_mk)
return none_ecs(); return none_ecs();
expr const & f = args[mk_pos-2]; expr const & f = args[arg_pos];
expr r = mk_app(f, app_arg(mk)); expr r = mk_app(f, app_arg(mk));
unsigned elim_arity = mk_pos+1; unsigned elim_arity = mk_pos+1;
if (args.size() > elim_arity) if (args.size() > elim_arity)

6
tests/lean/quot_ind_bug.lean Normal file
View file

@ -0,0 +1,6 @@
open quot
variables {A : Type} [s : setoid A] {B : quot s → Prop} (c : ∀ (a : A), B (quot.mk a)) (a : A)
check quot.ind c ⟦a⟧
check c a
eval quot.ind c ⟦a⟧

3
tests/lean/quot_ind_bug.lean.expected.out Normal file
View file

@ -0,0 +1,3 @@
ind c ⟦a⟧ : B ⟦a⟧
c a : B ⟦a⟧
c a