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

fix(library/equations_compiler/structural_rec): missing case: reflexive inductive type eliminating into Prop

Browse source 
see #1199
This commit is contained in:
Leonardo de Moura 2016-11-23 13:56:01 -08:00
parent 21bad7cb97
commit b75e8b99f5
2 changed files with 36 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/library/equations_compiler/structural_rec.cpp
View file

@ -414,12 +414,13 @@ struct structural_rec_fn {
optional<expr> to_below(expr const & d, expr const & a, expr const & F) {
expr const & fn = get_app_fn(d);
trace_struct_aux(tout() << "d: " << d << ", a: " << a << ", F: " << F << "\n";);
if (is_constant(fn, get_prod_name())) {
if (is_constant(fn, get_prod_name()) || is_constant(fn, get_and_name())) {
bool prop = is_constant(fn, get_and_name());
expr d_arg1 = m_ctx.whnf(app_arg(app_fn(d)));
expr d_arg2 = m_ctx.whnf(app_arg(d));
if (auto r = to_below(d_arg1, a, mk_fst(m_ctx, F)))
if (auto r = to_below(d_arg1, a, mk_fst(m_ctx, F, prop)))
return r;
else if (auto r = to_below(d_arg2, a, mk_snd(m_ctx, F)))
else if (auto r = to_below(d_arg2, a, mk_snd(m_ctx, F, prop)))
return r;
else
return none_expr();
@ -551,9 +552,10 @@ struct structural_rec_fn {
expr whnf_upto_below(type_context & ctx, name const & I_name, expr const & below_type) {
name below_name(I_name, "below");
name ibelow_name(I_name, "ibelow");
return ctx.whnf_pred(below_type, [&](expr const & e) {
expr const & fn = get_app_fn(e);
return !is_constant(fn) || const_name(fn) != below_name;
return !is_constant(fn) || (const_name(fn) != below_name && const_name(fn) != ibelow_name);
});
}

30
tests/lean/run/reflexive_elim_prop_bug.lean Normal file
View file

@ -0,0 +1,30 @@
namespace tst1
inductive Foo : Type
| node : (ℕ → Foo) → Foo
| leaf : Foo
constant Bar : Type
constant P : Bar → Prop
constant Q : Bar → Type
axiom P_ax : ∀ b, P b
lemma foo_error : ∀ (foo : Foo) (b : Bar), P b
| (Foo.node f) := λ b, foo_error (f 0) b
| Foo.leaf := λ b, P_ax b
end tst1
namespace tst2
inductive Foo : Type
| node : (ℕ → Foo) → Foo
constant Bar : Type
constant P : Bar → Prop
constant Q : Bar → Type
lemma foo_error : ∀ (foo : Foo) (b : Bar), P b
| (Foo.node f) := λ b, foo_error (f 0) b
end tst2