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

fix(library/rewriter): use Abst axiom in lambda_body RW

Browse source
This commit is contained in:
Soonho Kong 2013-12-01 22:22:56 -05:00
parent 0553d29078
commit a2d6918348
2 changed files with 2 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/library/rewriter/rewriter.cpp
View file

@ -92,10 +92,7 @@ pair<expr, expr> rewrite_lambda_body(environment const & env, context & ctx, exp
expr const & new_v = mk_lambda(n, ty, new_body); expr const & new_v = mk_lambda(n, ty, new_body);
expr const & ty_body = ti(body, extend(ctx, n, ty)); expr const & ty_body = ti(body, extend(ctx, n, ty));
lean_assert_eq(ty_body, ti(new_body, ctx)); // TODO(soonhok): generalize for hetreogeneous types lean_assert_eq(ty_body, ti(new_body, ctx)); // TODO(soonhok): generalize for hetreogeneous types
expr const & proof = Subst(ty_body, body, new_body, expr const & proof = Abst(ty, mk_lambda(n, ty, ty_body), v, new_v, mk_lambda(n, ty, pf_body));
Fun({Const("e"), ty_body},
mk_eq(v, mk_lambda(n, ty, Const("e")))),
Refl(ty_v, v), pf_body);
return make_pair(new_v, proof); return make_pair(new_v, proof);
} }
} }

3
src/tests/library/rewriter/rewriter.cpp
View file

@ -725,8 +725,7 @@ static void lambda_rewriter2_tst() {
cout << "Concl = " << concl << std::endl cout << "Concl = " << concl << std::endl
<< "Proof = " << proof << std::endl; << "Proof = " << proof << std::endl;
lean_assert_eq(concl, mk_eq(v, mk_lambda("x", Nat, nAdd(a, Var(0))))); lean_assert_eq(concl, mk_eq(v, mk_lambda("x", Nat, nAdd(a, Var(0)))));
// TODO(soonhok): this one doesn't work now. env.add_theorem("lambda_rewriter2", concl, proof);
// env.add_theorem("lambda_rewriter2", concl, proof);
cout << "====================================================" << std::endl; cout << "====================================================" << std::endl;
} }