From 91ce99d9215ead7c92bc7461cda9564fe57cc113 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 11 Dec 2014 17:32:39 -0800 Subject: [PATCH] feat(frontends/lean): type check 'decreasing' proofs in definition using well-founded recursion --- src/frontends/lean/elaborator.cpp | 22 +++++++++++++++++++--- tests/lean/extra/rec.lean | 20 +++++++++++++------- 2 files changed, 32 insertions(+), 10 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 1df7c78e2..f1d79f694 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -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 ts; + type_checker & tc = *m_tc[m_relax_main_opaque]; + to_telescope(tc, f_type, ts, optional(), cs); + buffer old_args; + buffer 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); } diff --git a/tests/lean/extra/rec.lean b/tests/lean/extra/rec.lean index da24a61b5..459a839ec 100644 --- a/tests/lean/extra/rec.lean +++ b/tests/lean/extra/rec.lean @@ -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,