From 9210e45da0cc57f4d3a5a246d7d93748cd6550c3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 10 Feb 2017 22:30:23 -0800 Subject: [PATCH] feat(frontends/lean): add notation for ';' and '<|>' in the tactic interactive mode --- src/frontends/lean/pp.cpp | 4 + src/frontends/lean/tactic_notation.cpp | 314 ++++++++++++++++--------- src/frontends/lean/tokens.cpp | 4 + src/frontends/lean/tokens.h | 1 + src/frontends/lean/tokens.txt | 1 + src/library/constants.cpp | 8 + src/library/constants.h | 2 + src/library/constants.txt | 2 + tests/lean/run/auto_quote1.lean | 14 +- tests/lean/run/auto_quote2.lean | 14 ++ tests/lean/run/cpdt.lean | 50 ++++ 11 files changed, 298 insertions(+), 116 deletions(-) create mode 100644 tests/lean/run/auto_quote2.lean create mode 100644 tests/lean/run/cpdt.lean diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index d614f8a2b0..5d77140fcc 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -45,6 +45,7 @@ Author: Leonardo de Moura #include "library/compiler/rec_fn_macro.h" #include "frontends/lean/pp.h" #include "frontends/lean/util.h" +#include "frontends/lean/prenum.h" #include "frontends/lean/token_table.h" #include "frontends/lean/builtin_exprs.h" #include "frontends/lean/structure_cmd.h" @@ -1057,6 +1058,9 @@ auto pretty_fn::pp_equations(expr const & e) -> optional { auto pretty_fn::pp_macro_default(expr const & e) -> result { // TODO(Leo): have macro annotations // fix macro<->pp interface + if (is_prenum(e)) { + return format(prenum_value(e).to_string()); + } format r = compose(format("["), format(macro_def(e).get_name())); for (unsigned i = 0; i < macro_num_args(e); i++) r += nest(m_indent, compose(line(), pp_child(macro_arg(e, i), max_bp()).fmt())); diff --git a/src/frontends/lean/tactic_notation.cpp b/src/frontends/lean/tactic_notation.cpp index 0e1104910f..1a4713e0f3 100644 --- a/src/frontends/lean/tactic_notation.cpp +++ b/src/frontends/lean/tactic_notation.cpp @@ -106,24 +106,8 @@ static expr mk_tactic_solve1(parser & p, expr tac, pos_info const & pos, name co return r; } -static expr concat(parser & p, expr const & r, expr tac, pos_info const & pos) { - return p.save_pos(mk_app(mk_constant(get_pre_monad_seq_name()), r, tac), pos); -} - -static expr concat(parser & p, buffer const & args, unsigned start, unsigned end, pos_info const & pos) { - lean_assert(start < end); - lean_assert(end <= args.size()); - if (end == start+1) - return args[start]; - unsigned mid = (start + end)/2; - expr left = concat(p, args, start, mid, pos); - expr right = concat(p, args, mid, end, pos); - return concat(p, left, right, pos); -} - -static expr concat(parser & p, buffer const & args, pos_info const & pos) { - lean_assert(!args.empty()); - return concat(p, args, 0, args.size(), pos); +static expr concat(parser & p, expr const & tac1, expr const & tac2, pos_info const & pos) { + return p.save_pos(mk_app(mk_constant(get_pre_monad_seq_name()), tac1, tac2), pos); } static optional is_auto_quote_tactic(parser & p, name const & tac_class) { @@ -181,7 +165,11 @@ static expr parse_using_id(parser & p, name const & decl_name) { } } -static expr parse_qexpr(parser & p, unsigned rbp) { +/* Remark: rbp for '<|>' is 2, ';' is 1, and ',' is 0 + qexpr0 shoud use rbp 2. + + TODO(Leo): rename qexpr0 to something else */ +static expr parse_qexpr(parser & p, unsigned rbp = 2) { auto pos = p.pos(); expr e; /* TODO(Leo): avoid p.in_quote by improving @@ -199,7 +187,7 @@ static expr parse_qexpr_list(parser & p) { buffer result; p.check_token_next(get_lbracket_tk(), "invalid auto-quote tactic argument, '[' expected"); while (!p.curr_is_token(get_rbracket_tk())) { - result.push_back(parse_qexpr(p, 0)); + result.push_back(parse_qexpr(p)); if (!p.curr_is_token(get_comma_tk())) break; p.next(); } @@ -219,7 +207,7 @@ static expr parse_qexpr_list_or_qexpr0(parser & p) { return parse_qexpr_list(p); } else { buffer args; - args.push_back(parse_qexpr(p, 0)); + args.push_back(parse_qexpr(p)); /* Remark: We do not save position information for list.cons and list.nil. Reason: consider the tactic rw add_zero a @@ -274,7 +262,7 @@ static expr parse_qexpr_list_or_qexpr0_with_pos(parser & p) { } else { buffer args; expr pos = to_expr_pos(p.pos()); - expr tac = parse_qexpr(p, 0); + expr tac = parse_qexpr(p); args.push_back(mk_pair(tac, pos)); /* Remark: We do not save position information for list.cons and list.nil. Reason: consider the tactic @@ -351,7 +339,7 @@ static expr parse_auto_quote_tactic(parser & p, name const & decl_name, name con if (is_constant(arg_type, get_interactive_types_qexpr_name())) { args.push_back(parse_qexpr(p, get_max_prec())); } else if (is_constant(arg_type, get_interactive_types_qexpr0_name())) { - args.push_back(parse_qexpr(p, 0)); + args.push_back(parse_qexpr(p)); } else if (is_constant(arg_type, get_interactive_types_qexpr_list_name())) { args.push_back(parse_qexpr_list(p)); } else if (is_constant(arg_type, get_interactive_types_qexpr_list_with_pos_name())) { @@ -409,30 +397,115 @@ static bool is_curr_exact_shortcut(parser & p) { p.curr_is_token(get_suppose_tk()); } -static expr parse_tactic_core(parser & p, name const & tac_class, bool use_rstep, bool report_error) { - try { - p.check_break_before(); - if (p.curr_is_identifier()) - p.check_break_at_pos(); - } catch (break_at_pos_exception & e) { - e.m_token_info.m_context = break_at_pos_exception::token_context::interactive_tactic; - e.m_token_info.m_tac_class = tac_class; - throw; +struct parse_tactic_fn { + parser & m_p; + name m_tac_class; + bool m_use_rstep; + bool m_report_error; + + parse_tactic_fn(parser & p, name tac_class, bool use_rstep, bool report_error): + m_p(p), m_tac_class(tac_class), m_use_rstep(use_rstep), m_report_error(report_error) {} + + expr concat(expr const & tac1, expr const & tac2, pos_info const & pos) { + return ::lean::concat(m_p, tac1, tac2, pos); } - expr r; - auto pos = p.pos(); - if (auto dname = is_auto_quote_tactic(p, tac_class)) { - r = parse_auto_quote_tactic(p, *dname, tac_class, use_rstep, report_error); - } else if (is_curr_exact_shortcut(p)) { - expr arg = parse_qexpr(p, 0); - r = p.mk_app(p.save_pos(mk_constant(tac_class + name({"interactive", "exact"})), pos), arg, pos); - if (use_rstep) r = mk_tactic_rstep(p, r, pos, tac_class, report_error); - } else { - r = p.parse_expr(); - if (use_rstep) r = mk_tactic_rstep(p, r, pos, tac_class, report_error); + expr andthen(expr const & tac1, expr const & tac2, pos_info const & pos) { + return m_p.save_pos(mk_app(mk_constant(get_andthen_name()), tac1, tac2), pos); } - return concat(p, mk_tactic_save_info(p, pos, tac_class), r, pos); + + expr orelse(expr const & tac1, expr const & tac2, pos_info const & pos) { + return m_p.save_pos(mk_app(mk_constant(get_orelse_name()), tac1, tac2), pos); + } + + expr parse_elem_core(bool save_info) { + try { + m_p.check_break_before(); + if (m_p.curr_is_identifier()) + m_p.check_break_at_pos(); + } catch (break_at_pos_exception & e) { + e.m_token_info.m_context = break_at_pos_exception::token_context::interactive_tactic; + e.m_token_info.m_tac_class = m_tac_class; + throw; + } + expr r; + auto pos = m_p.pos(); + if (auto dname = is_auto_quote_tactic(m_p, m_tac_class)) { + r = parse_auto_quote_tactic(m_p, *dname, m_tac_class, m_use_rstep, m_report_error); + } else if (is_curr_exact_shortcut(m_p)) { + expr arg = parse_qexpr(m_p); + r = m_p.mk_app(m_p.save_pos(mk_constant(m_tac_class + name({"interactive", "exact"})), pos), arg, pos); + if (m_use_rstep) r = mk_tactic_rstep(m_p, r, pos, m_tac_class, m_report_error); + } else { + r = m_p.parse_expr(); + if (m_use_rstep) r = mk_tactic_rstep(m_p, r, pos, m_tac_class, m_report_error); + } + if (save_info) + return concat(mk_tactic_save_info(m_p, pos, m_tac_class), r, pos); + else + return r; + } + + expr parse_block(pos_info const & pos, name const & end_tk) { + return ::lean::parse_begin_end_block(m_p, pos, end_tk, m_tac_class, m_use_rstep, m_report_error); + } + + expr parse_elem(bool save_info) { + if (m_p.curr_is_token(get_begin_tk()) || + m_p.curr_is_token(get_lcurly_tk())) { + auto pos = m_p.pos(); + name const & end_tk = m_p.curr_is_token(get_begin_tk()) ? get_end_tk() : get_rcurly_tk(); + expr next_tac = parse_block(pos, end_tk); + auto block_pos = m_p.pos_of(next_tac); + next_tac = mk_tactic_solve1(m_p, next_tac, block_pos, m_tac_class, m_use_rstep && save_info, m_report_error && save_info); + if (save_info) { + expr info_tac = mk_tactic_save_info(m_p, pos, m_tac_class); + return concat(info_tac, next_tac, pos); + } else { + return next_tac; + } + } else { + return parse_elem_core(save_info); + } + } + + expr parse_orelse(expr left) { + auto start_pos = m_p.pos(); + expr r = left; + while (m_p.curr_is_token(get_orelse_tk())) { + m_p.next(); + expr curr = parse_elem(false); + r = orelse(r, curr, start_pos); + } + return r; + } + + expr parse_andthen(expr left) { + auto start_pos = m_p.pos(); + expr r = left; + while (m_p.curr_is_token(get_semicolon_tk())) { + m_p.next(); + expr curr = parse_elem(false); + if (m_p.curr_is_token(get_orelse_tk())) + curr = parse_orelse(curr); + r = andthen(r, curr, start_pos); + } + return r; + } + + expr operator()() { + expr r = parse_elem(true); + if (m_p.curr_is_token(get_semicolon_tk())) + return parse_andthen(r); + else if (m_p.curr_is_token(get_orelse_tk())) + return parse_orelse(r); + else + return r; + } +}; + +static expr parse_tactic_core(parser & p, name const & tac_class, bool use_rstep, bool report_error) { + return parse_tactic_fn(p, tac_class, use_rstep, report_error)(); } static expr parse_tactic(parser & p, name const & tac_class, bool use_rstep, bool report_error) { @@ -475,75 +548,100 @@ static name parse_tactic_class(parser & p, name tac_class) { } } -static expr parse_begin_end_block(parser & p, pos_info const & start_pos, name const & end_token, name tac_class, bool use_rstep, bool report_error) { - p.next(); - name new_tac_class = tac_class; - if (tac_class == get_tactic_name()) - new_tac_class = parse_tactic_class(p, tac_class); - optional cfg; - bool is_ext_tactic_class = tac_class == get_tactic_name() && new_tac_class != get_tactic_name(); - if (is_ext_tactic_class && p.curr_is_token(get_with_tk())) { - p.next(); - cfg = p.parse_expr(); - p.check_token_next(get_comma_tk(), "invalid begin [...] with cfg, ... end block, ',' expected"); +struct parse_begin_end_block_fn { + parser & m_p; + name m_tac_class; + bool m_use_rstep; + bool m_report_error; + + parse_begin_end_block_fn(parser & p, name tac_class, bool use_rstep, bool report_error): + m_p(p), m_tac_class(tac_class), m_use_rstep(use_rstep), m_report_error(report_error) {} + + expr concat(expr const & tac1, expr const & tac2, pos_info const & pos) { + return ::lean::concat(m_p, tac1, tac2, pos); } - tac_class = new_tac_class; - buffer to_concat; - to_concat.push_back(mk_tactic_save_info(p, start_pos, tac_class)); - try { - while (!p.curr_is_token(end_token)) { - auto pos = p.pos(); - try { - /* parse next element */ - expr next_tac; - if (p.curr_is_token(get_begin_tk()) || - p.curr_is_token(get_lcurly_tk())) { - name const & end_tk = p.curr_is_token(get_begin_tk()) ? get_end_tk() : get_rcurly_tk(); - expr info_tac = mk_tactic_save_info(p, pos, tac_class); - to_concat.push_back(info_tac); - next_tac = parse_begin_end_block(p, pos, end_tk, tac_class, use_rstep, report_error); - auto block_pos = p.pos_of(next_tac); - next_tac = mk_tactic_solve1(p, next_tac, block_pos, tac_class, use_rstep, report_error); - } else if (p.curr_is_token(get_do_tk())) { - expr tac = p.parse_expr(); - expr type = p.save_pos(mk_tactic_unit(tac_class), pos); - next_tac = p.save_pos(mk_typed_expr(type, tac), pos); - next_tac = mk_tactic_step(p, next_tac, pos, tac_class, use_rstep, report_error); - } else { - next_tac = parse_tactic(p, tac_class, use_rstep, report_error); - } - to_concat.push_back(next_tac); - if (!p.curr_is_token(end_token)) { - to_concat.push_back(mk_tactic_save_info(p, {p.pos().first, p.pos().second+1}, tac_class)); - info_tweak(p); - p.check_token_next(get_comma_tk(), "invalid 'begin-end' expression, ',' expected"); - } - } catch (break_at_pos_exception & ex) { - ex.report_goal_pos(pos); - throw ex; - } - } - } catch (exception & ex) { - if (end_token == get_end_tk()) - consume_until_end_or_command(p); - throw; + + expr concat(buffer const & args, unsigned start, unsigned end, pos_info const & pos) { + lean_assert(start < end); + lean_assert(end <= args.size()); + if (end == start+1) + return args[start]; + unsigned mid = (start + end)/2; + expr left = concat(args, start, mid, pos); + expr right = concat(args, mid, end, pos); + return concat(left, right, pos); } - auto end_pos = p.pos(); - expr r = concat(p, to_concat, start_pos); - r = concat(p, r, mk_tactic_save_info(p, end_pos, tac_class), end_pos); - try { - p.next(); - } catch (break_at_pos_exception & ex) { - ex.report_goal_pos(end_pos); - throw; + + expr concat(buffer const & args, pos_info const & pos) { + lean_assert(!args.empty()); + return concat(args, 0, args.size(), pos); } - if (!is_ext_tactic_class) { + + expr mk_save_info() { + expr r = mk_tactic_save_info(m_p, {m_p.pos().first, m_p.pos().second+1}, m_tac_class); + info_tweak(m_p); return r; - } else if (cfg) { - return copy_tag(r, mk_app(mk_constant(name(tac_class, "execute_with")), *cfg, r)); - } else { - return copy_tag(r, mk_app(mk_constant(name(tac_class, "execute")), r)); } + + expr parse_tactic() { + return ::lean::parse_tactic(m_p, m_tac_class, m_use_rstep, m_report_error); + } + + expr operator()(pos_info const & start_pos, name const & end_token) { + m_p.next(); + name new_tac_class = m_tac_class; + if (m_tac_class == get_tactic_name()) + new_tac_class = parse_tactic_class(m_p, m_tac_class); + optional cfg; + bool is_ext_tactic_class = m_tac_class == get_tactic_name() && new_tac_class != get_tactic_name(); + if (is_ext_tactic_class && m_p.curr_is_token(get_with_tk())) { + m_p.next(); + cfg = m_p.parse_expr(); + m_p.check_token_next(get_comma_tk(), "invalid begin [...] with cfg, ... end block, ',' expected"); + } + m_tac_class = new_tac_class; + buffer to_concat; + to_concat.push_back(mk_tactic_save_info(m_p, start_pos, m_tac_class)); + try { + while (!m_p.curr_is_token(end_token)) { + pos_info pos = m_p.pos(); + try { + to_concat.push_back(parse_tactic()); + if (!m_p.curr_is_token(end_token)) { + to_concat.push_back(mk_save_info()); + m_p.check_token_next(get_comma_tk(), "invalid 'begin-end' expression, ',' expected"); + } + } catch (break_at_pos_exception & ex) { + ex.report_goal_pos(pos); + throw ex; + } + } + } catch (exception & ex) { + if (end_token == get_end_tk()) + consume_until_end_or_command(m_p); + throw; + } + auto end_pos = m_p.pos(); + expr r = concat(to_concat, start_pos); + r = concat(r, mk_tactic_save_info(m_p, end_pos, m_tac_class), end_pos); + try { + m_p.next(); + } catch (break_at_pos_exception & ex) { + ex.report_goal_pos(end_pos); + throw; + } + if (!is_ext_tactic_class) { + return r; + } else if (cfg) { + return copy_tag(r, mk_app(mk_constant(name(m_tac_class, "execute_with")), *cfg, r)); + } else { + return copy_tag(r, mk_app(mk_constant(name(m_tac_class, "execute")), r)); + } + } +}; + +static expr parse_begin_end_block(parser & p, pos_info const & start_pos, name const & end_token, name tac_class, bool use_rstep, bool report_error) { + return parse_begin_end_block_fn(p, tac_class, use_rstep, report_error)(start_pos, end_token); } expr parse_begin_end_expr_core(parser & p, pos_info const & pos, name const & end_token) { diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp index c4b8b116c8..5bf272fbb9 100644 --- a/src/frontends/lean/tokens.cpp +++ b/src/frontends/lean/tokens.cpp @@ -12,6 +12,7 @@ static name const * g_placeholder_tk = nullptr; static name const * g_colon_tk = nullptr; static name const * g_semicolon_tk = nullptr; static name const * g_dcolon_tk = nullptr; +static name const * g_orelse_tk = nullptr; static name const * g_lparen_tk = nullptr; static name const * g_rparen_tk = nullptr; static name const * g_llevel_curly_tk = nullptr; @@ -134,6 +135,7 @@ void initialize_tokens() { g_colon_tk = new name{":"}; g_semicolon_tk = new name{";"}; g_dcolon_tk = new name{"::"}; + g_orelse_tk = new name{"<|>"}; g_lparen_tk = new name{"("}; g_rparen_tk = new name{")"}; g_llevel_curly_tk = new name{".{"}; @@ -257,6 +259,7 @@ void finalize_tokens() { delete g_colon_tk; delete g_semicolon_tk; delete g_dcolon_tk; + delete g_orelse_tk; delete g_lparen_tk; delete g_rparen_tk; delete g_llevel_curly_tk; @@ -379,6 +382,7 @@ name const & get_placeholder_tk() { return *g_placeholder_tk; } name const & get_colon_tk() { return *g_colon_tk; } name const & get_semicolon_tk() { return *g_semicolon_tk; } name const & get_dcolon_tk() { return *g_dcolon_tk; } +name const & get_orelse_tk() { return *g_orelse_tk; } name const & get_lparen_tk() { return *g_lparen_tk; } name const & get_rparen_tk() { return *g_rparen_tk; } name const & get_llevel_curly_tk() { return *g_llevel_curly_tk; } diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h index 9b68a9e0d7..bdbd507c92 100644 --- a/src/frontends/lean/tokens.h +++ b/src/frontends/lean/tokens.h @@ -14,6 +14,7 @@ name const & get_placeholder_tk(); name const & get_colon_tk(); name const & get_semicolon_tk(); name const & get_dcolon_tk(); +name const & get_orelse_tk(); name const & get_lparen_tk(); name const & get_rparen_tk(); name const & get_llevel_curly_tk(); diff --git a/src/frontends/lean/tokens.txt b/src/frontends/lean/tokens.txt index 90f9274b02..bfa716cb13 100644 --- a/src/frontends/lean/tokens.txt +++ b/src/frontends/lean/tokens.txt @@ -7,6 +7,7 @@ placeholder _ colon : semicolon ; dcolon :: +orelse <|> lparen ( rparen ) llevel_curly .{ diff --git a/src/library/constants.cpp b/src/library/constants.cpp index 2976cd08aa..1db9547a39 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -15,6 +15,7 @@ name const * g_and = nullptr; name const * g_and_elim_left = nullptr; name const * g_and_elim_right = nullptr; name const * g_and_intro = nullptr; +name const * g_andthen = nullptr; name const * g_auto_param = nullptr; name const * g_bit0 = nullptr; name const * g_bit1 = nullptr; @@ -331,6 +332,7 @@ name const * g_or_neg_resolve_right = nullptr; name const * g_or_rec = nullptr; name const * g_or_resolve_left = nullptr; name const * g_or_resolve_right = nullptr; +name const * g_orelse = nullptr; name const * g_out_param = nullptr; name const * g_punit = nullptr; name const * g_punit_star = nullptr; @@ -496,6 +498,7 @@ void initialize_constants() { g_and_elim_left = new name{"and", "elim_left"}; g_and_elim_right = new name{"and", "elim_right"}; g_and_intro = new name{"and", "intro"}; + g_andthen = new name{"andthen"}; g_auto_param = new name{"auto_param"}; g_bit0 = new name{"bit0"}; g_bit1 = new name{"bit1"}; @@ -812,6 +815,7 @@ void initialize_constants() { g_or_rec = new name{"or", "rec"}; g_or_resolve_left = new name{"or", "resolve_left"}; g_or_resolve_right = new name{"or", "resolve_right"}; + g_orelse = new name{"orelse"}; g_out_param = new name{"out_param"}; g_punit = new name{"punit"}; g_punit_star = new name{"punit", "star"}; @@ -978,6 +982,7 @@ void finalize_constants() { delete g_and_elim_left; delete g_and_elim_right; delete g_and_intro; + delete g_andthen; delete g_auto_param; delete g_bit0; delete g_bit1; @@ -1294,6 +1299,7 @@ void finalize_constants() { delete g_or_rec; delete g_or_resolve_left; delete g_or_resolve_right; + delete g_orelse; delete g_out_param; delete g_punit; delete g_punit_star; @@ -1459,6 +1465,7 @@ name const & get_and_name() { return *g_and; } name const & get_and_elim_left_name() { return *g_and_elim_left; } name const & get_and_elim_right_name() { return *g_and_elim_right; } name const & get_and_intro_name() { return *g_and_intro; } +name const & get_andthen_name() { return *g_andthen; } name const & get_auto_param_name() { return *g_auto_param; } name const & get_bit0_name() { return *g_bit0; } name const & get_bit1_name() { return *g_bit1; } @@ -1775,6 +1782,7 @@ name const & get_or_neg_resolve_right_name() { return *g_or_neg_resolve_right; } name const & get_or_rec_name() { return *g_or_rec; } name const & get_or_resolve_left_name() { return *g_or_resolve_left; } name const & get_or_resolve_right_name() { return *g_or_resolve_right; } +name const & get_orelse_name() { return *g_orelse; } name const & get_out_param_name() { return *g_out_param; } name const & get_punit_name() { return *g_punit; } name const & get_punit_star_name() { return *g_punit_star; } diff --git a/src/library/constants.h b/src/library/constants.h index c875c03e24..67a5262753 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -17,6 +17,7 @@ name const & get_and_name(); name const & get_and_elim_left_name(); name const & get_and_elim_right_name(); name const & get_and_intro_name(); +name const & get_andthen_name(); name const & get_auto_param_name(); name const & get_bit0_name(); name const & get_bit1_name(); @@ -333,6 +334,7 @@ name const & get_or_neg_resolve_right_name(); name const & get_or_rec_name(); name const & get_or_resolve_left_name(); name const & get_or_resolve_right_name(); +name const & get_orelse_name(); name const & get_out_param_name(); name const & get_punit_name(); name const & get_punit_star_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index c5b09815e7..84e9d1236f 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -10,6 +10,7 @@ and and.elim_left and.elim_right and.intro +andthen auto_param bit0 bit1 @@ -326,6 +327,7 @@ or.neg_resolve_right or.rec or.resolve_left or.resolve_right +orelse out_param punit punit.star diff --git a/tests/lean/run/auto_quote1.lean b/tests/lean/run/auto_quote1.lean index a3b712bc2d..b61fe4358b 100644 --- a/tests/lean/run/auto_quote1.lean +++ b/tests/lean/run/auto_quote1.lean @@ -1,19 +1,17 @@ example (a b c : nat) : a = b → b = c → c = a := -begin +by { intros, apply eq.symm, apply eq.trans, assumption, assumption -end +} example (a b c : nat) : a = b → b = c → c = a := -begin - intro h1, - intro h2, - refine eq.symm (eq.trans h1 _), - exact h2 -end +by intros; apply eq.symm; apply eq.trans; repeat {assumption} + +example (p q r : Prop) : p → q → r → p ∧ q ∧ r ∧ p ∧ q := +by intros; repeat {assumption <|> constructor} example (a b c : nat) : a = b → b = c → c = a := begin diff --git a/tests/lean/run/auto_quote2.lean b/tests/lean/run/auto_quote2.lean new file mode 100644 index 0000000000..a4f40ab093 --- /dev/null +++ b/tests/lean/run/auto_quote2.lean @@ -0,0 +1,14 @@ +example (a b c : nat) : a = b → b = c → c = a := +by { + intros, + apply eq.symm, + apply eq.trans, + assumption, + assumption +} + +example (a b c : nat) : a = b → b = c → c = a := +by intros; apply eq.symm; apply eq.trans; repeat {assumption} + +example (p q r : Prop) : p → q → r → p ∧ q ∧ r ∧ p ∧ q := +by intros; repeat {assumption <|> constructor} diff --git a/tests/lean/run/cpdt.lean b/tests/lean/run/cpdt.lean new file mode 100644 index 0000000000..d41c2c16b0 --- /dev/null +++ b/tests/lean/run/cpdt.lean @@ -0,0 +1,50 @@ +/- "Proving in the Large" chapter of CPDT -/ + +inductive exp : Type +| Const (n : nat) : exp +| Plus (e1 e2 : exp) : exp +| Mult (e1 e2 : exp) : exp + +open exp + +def exp_eval : exp → nat +| (Const n) := n +| (Plus e1 e2) := exp_eval e1 + exp_eval e2 +| (Mult e1 e2) := exp_eval e1 * exp_eval e2 + +def times (k : nat) : exp → exp +| (Const n) := Const (k * n) +| (Plus e1 e2) := Plus (times e1) (times e2) +| (Mult e1 e2) := Mult (times e1) e2 + +attribute [simp] exp_eval times mul_add + +theorem eval_times (k e) : exp_eval (times k e) = k * exp_eval e := +by induction e; simp_using_hs + +/- CPDT: induction e; crush. -/ + +def reassoc : exp → exp +| (Const n) := (Const n) +| (Plus e1 e2) := + let e1' := reassoc e1 in + let e2' := reassoc e2 in + match e2' with + | (Plus e21 e22) := Plus (Plus e1' e21) e22 + | _ := Plus e1' e2' + end +| (Mult e1 e2) := + let e1' := reassoc e1 in + let e2' := reassoc e2 in + match e2' with + | (Mult e21 e22) := Mult (Mult e1' e21) e22 + | _ := Mult e1' e2' + end + +attribute [simp] reassoc + +lemma rewr : ∀ a b c d : nat, b * c = d → a * b * c = a * d := +by intros; simp_using_hs + +theorem reassoc_correct (e) : exp_eval (reassoc e) = exp_eval e := +by induction e; simp; try {revert ih_2; cases (reassoc e2); dsimp; intros; simp_using_hs}