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

feat(frontends/lean): type check 'decreasing' proofs in definition using well-founded recursion

Browse source
This commit is contained in:
Leonardo de Moura 2014-12-11 17:32:39 -08:00
parent 8b3e97d285
commit 91ce99d921
2 changed files with 32 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
src/frontends/lean/elaborator.cpp
View file

@ -31,6 +31,7 @@ Author: Leonardo de Moura
#include "library/metavar_closure.h"
#include "library/typed_expr.h"
#include "library/local_context.h"
#include "library/util.h"
#include "library/tactic/expr_to_tactic.h"
#include "library/error_handling/error_handling.h"
#include "library/definitional/equations.h"
@ -957,9 +958,24 @@ expr elaborator::visit_decreasing(expr const & e, constraint_seq & cs) {
"application of the recursive function being defined", e);
expr dec_app = visit(decreasing_app(e), cs);
expr dec_proof = visit(decreasing_proof(e), cs);
// Remark: perhaps we should enforce the type of dec_proof here.
// We may have enough information to wrap the arguments in a sigma type (reason: the type of the function being elaborated has holes).
// Possible solution: create a constraint that enforces the type as soon the type of function has been elaborated.
expr f_type = mlocal_type(get_app_fn(*m_equation_lhs));
buffer<expr> ts;
type_checker & tc = *m_tc[m_relax_main_opaque];
to_telescope(tc, f_type, ts, optional<binder_info>(), cs);
buffer<expr> old_args;
buffer<expr> new_args;
get_app_args(*m_equation_lhs, old_args);
get_app_args(dec_app, new_args);
if (new_args.size() != old_args.size() || new_args.size() != ts.size())
throw_elaborator_exception(env(), "invalid recursive application, mistmatch in the number of arguments", e);
expr old_tuple = mk_sigma_mk(tc, ts, old_args, cs);
expr new_tuple = mk_sigma_mk(tc, ts, new_args, cs);
expr expected_dec_proof_type = mk_app(mk_app(*m_equation_R, new_tuple, e.get_tag()), old_tuple, e.get_tag());
expr dec_proof_type = infer_type(dec_proof, cs);
justification j = mk_type_mismatch_jst(dec_proof, dec_proof_type, expected_dec_proof_type, decreasing_proof(e));
auto new_dec_proof_cs = ensure_has_type(dec_proof, dec_proof_type, expected_dec_proof_type, j, m_relax_main_opaque);
dec_proof = new_dec_proof_cs.first;
cs += new_dec_proof_cs.second;
return mk_decreasing(dec_app, dec_proof);
}

20
tests/lean/extra/rec.lean
View file

@ -1,8 +1,19 @@
import data.vector
open nat vector
check lt.base
set_option pp.implicit true
definition fib : nat → nat,
fib 0 := 1,
fib 1 := 1,
fib (a+2) := (fib a ↓ lt.step (lt.base a)) + (fib (a+1) ↓ lt.base (a+1))
[wf] lt.wf
definition gcd : nat → nat → nat,
gcd 0 x := x,
gcd x 0 := x,
gcd (succ x) (succ y) := if y ≤ x
then gcd (x - y) (succ y) ↓ !sigma.lex.left (lt_succ_of_le (sub_le x y))
else gcd (succ x) (y - x) ↓ !sigma.lex.right (lt_succ_of_le (sub_le y x))
[wf] sigma.lex.wf lt.wf (λ x, lt.wf)
definition add : nat → nat → nat,
add zero b := b,
@ -12,11 +23,6 @@ definition map {A B C : Type} (f : A → B → C) : Π {n}, vector A n → vecto
map nil nil := nil,
map (a :: va) (b :: vb) := f a b :: map va vb
definition fib : nat → nat,
fib 0 := 1,
fib 1 := 1,
fib (a+2) := (fib a ↓ lt.step (lt.base a)) + (fib (a+1) ↓ lt.base (a+1))
[wf] lt.wf
definition half : nat → nat,
half 0 := 0,