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

fix(library/equations_compiler/structural_rec): reflexive type support

Browse source
This commit is contained in:
Leonardo de Moura 2016-09-18 16:15:31 -07:00
parent 06df5fef1d
commit 194d1be0dd
2 changed files with 15 additions and 9 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

@ -345,6 +345,7 @@ struct structural_rec_fn {
I_params.shrink(I_params.size() - nindices);
expr motive = ctx.mk_pi(other_args, fn_type);
level u = get_level(ctx, motive);
m_use_ibelow = m_reflexive && is_zero(u);
if (m_reflexive) {
if (!is_zero(u) && !is_not_zero(u))
throw_error(sstream() << "invalid equations, "
@ -376,7 +377,6 @@ struct structural_rec_fn {
}
}
}
m_use_ibelow = m_reflexive && is_zero(u);
motive = ctx.mk_lambda(idx_args, ctx.mk_lambda(rec_arg, motive));
lean_assert(is_constant(I));
buffer<level> below_lvls;
@ -410,6 +410,7 @@ struct structural_rec_fn {
and m_C (the abstract local). */
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())) {
expr d_arg1 = m_ctx.whnf(app_arg(app_fn(d)));
expr d_arg2 = m_ctx.whnf(app_arg(d));
@ -439,7 +440,7 @@ struct structural_rec_fn {
return std::find(m_indices_pos.begin(), m_indices_pos.end(), idx) != m_indices_pos.end();
}
expr elim(buffer<expr> const & args, tag g) {
expr elim(expr const & e, buffer<expr> const & args, tag g) {
/* Replace motives with abstract one m_C.
We use the abstract motive m_C as "marker". */
buffer<expr> below_args;
@ -457,6 +458,8 @@ struct structural_rec_fn {
}
return r;
} else {
trace_struct_aux(tout() << "failed to eliminate recursive application using 'below'\n" <<
e << "\n";);
throw elim_rec_apps_failed();
}
}
@ -464,6 +467,7 @@ struct structural_rec_fn {
virtual expr visit_local(expr const & e) {
if (mlocal_name(e) == mlocal_name(m_fn)) {
/* unexpected occurrence of recursive function */
trace_struct_aux(tout() << "unexpected occurrence of recursive function: " << e << "\n";);
throw elim_rec_apps_failed();
}
return e;
@ -478,7 +482,7 @@ struct structural_rec_fn {
buffer<expr> new_args;
for (expr const & arg : args)
new_args.push_back(visit(arg));
return elim(new_args, e.get_tag());
return elim(e, new_args, e.get_tag());
} else {
return replace_visitor_with_tc::visit_app(e);
}

14
tests/lean/run/eq10.lean
View file

@ -1,3 +1,5 @@
set_option new_elaborator true
inductive formula
| eqf : nat → nat → formula
| andf : formula → formula → formula
@ -10,12 +12,12 @@ namespace formula
definition implies (a b : Prop) : Prop := a → b
definition denote : formula → Prop
| denote (eqf n1 n2) := n1 = n2
| denote (andf f1 f2) := denote f1 ∧ denote f2
| denote (impf f1 f2) := implies (denote f1) (denote f2)
| denote (orf f1 f2) := denote f1 ∨ denote f2
| denote (notf f) := ¬ denote f
| denote (allf f) := ∀ n : nat, denote (f n)
| (eqf n1 n2) := n1 = n2
| (andf f1 f2) := denote f1 ∧ denote f2
| (impf f1 f2) := implies (denote f1) (denote f2)
| (orf f1 f2) := denote f1 ∨ denote f2
| (notf f) := ¬ denote f
| (allf f) := ∀ n : nat, denote (f n)
theorem denote_eqf (n1 n2 : nat) : denote (eqf n1 n2) = (n1 = n2) :=
rfl