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

feat(frontends/lean): improved 'obtains' expression

Browse source
This commit is contained in:
Leonardo de Moura 2015-05-05 18:17:43 -07:00
parent 8aefcc182e
commit 616f49c2e4
13 changed files with 422 additions and 34 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
library/data/set/function.lean
View file

@ -45,13 +45,13 @@ lemma image_compose (f : Y → X) (g : X → Y) (a : set X) : (f ∘ g) '[a] = f
setext (take z,
iff.intro
(assume Hz : z ∈ (f ∘ g) '[a],
obtain x (Hx : x ∈ a ∧ f (g x) = z), from Hz,
have Hgx : g x ∈ g '[a], from in_image (and.left Hx) rfl,
show z ∈ f '[g '[a]], from in_image Hgx (and.right Hx))
obtain x (Hx₁ : x ∈ a) (Hx₂ : f (g x) = z), from Hz,
have Hgx : g x ∈ g '[a], from in_image Hx₁ rfl,
show z ∈ f '[g '[a]], from in_image Hgx Hx₂)
(assume Hz : z ∈ f '[g '[a]],
obtain y (Hy : y ∈ g '[a] ∧ f y = z), from Hz,
obtain x (Hz : x ∈ a ∧ g x = y), from and.left Hy,
show z ∈ (f ∘ g) '[a], from in_image (and.left Hz) ((and.right Hz)⁻¹ ▸ (and.right Hy))))
obtain y (Hy₁ : y ∈ g '[a]) (Hy₂ : f y = z), from Hz,
obtain x (Hz₁ : x ∈ a) (Hz₂ : g x = y), from Hy₁,
show z ∈ (f ∘ g) '[a], from in_image Hz₁ (Hz₂⁻¹ ▸ Hy₂)))
/- maps to -/

3
src/frontends/lean/CMakeLists.txt
View file

@ -8,6 +8,7 @@ structure_cmd.cpp info_manager.cpp info_annotation.cpp find_cmd.cpp
coercion_elaborator.cpp info_tactic.cpp
init_module.cpp elaborator_context.cpp calc_proof_elaborator.cpp
parse_tactic_location.cpp parse_rewrite_tactic.cpp builtin_tactics.cpp
type_util.cpp elaborator_exception.cpp migrate_cmd.cpp local_ref_info.cpp)
type_util.cpp elaborator_exception.cpp migrate_cmd.cpp local_ref_info.cpp
obtain_expr.cpp)
target_link_libraries(lean_frontend ${LEAN_LIBS})

57
src/frontends/lean/builtin_exprs.cpp
View file

@ -32,6 +32,7 @@ Author: Leonardo de Moura
#include "frontends/lean/info_tactic.h"
#include "frontends/lean/info_annotation.h"
#include "frontends/lean/structure_cmd.h"
#include "frontends/lean/obtain_expr.h"
namespace lean {
namespace notation {
@ -275,7 +276,7 @@ static expr parse_begin_end(parser & p, unsigned, expr const *, pos_info const &
static expr parse_proof_qed_core(parser & p, pos_info const & pos) {
expr r = p.parse_expr();
p.check_token_next(get_qed_tk(), "invalid proof-qed, 'qed' expected");
r = p.mk_by(p.mk_app(get_exact_tac_fn(), r, pos), pos);
r = p.mk_by_plus(p.mk_app(get_exact_tac_fn(), r, pos), pos);
return r;
}
@ -439,37 +440,37 @@ static expr parse_show(parser & p, unsigned, expr const *, pos_info const & pos)
}
}
static expr parse_obtain(parser & p, unsigned, expr const *, pos_info const & pos) {
if (!p.env().find(get_exists_elim_name()))
throw parser_error("invalid use of 'obtain' expression, environment does not contain 'exists.elim' theorem", pos);
// exists_elim {A : Type} {P : A → Prop} {B : Prop} (H1 : ∃ x : A, P x) (H2 : ∀ (a : A) (H : P a), B)
buffer<expr> ps;
auto b_pos = p.pos();
static obtain_struct parse_obtain_decls (parser & p, buffer<expr> & ps) {
buffer<obtain_struct> children;
while (!p.curr_is_token(get_comma_tk()) && !p.curr_is_token(get_rbracket_tk())) {
if (p.curr_is_token(get_lbracket_tk())) {
p.next();
auto s = parse_obtain_decls(p, ps);
children.push_back(s);
p.check_token_next(get_rbracket_tk(), "invalid 'obtain' expression, ']' expected");
} else {
unsigned old_sz = ps.size();
unsigned rbp = 0;
environment env = p.parse_binders(ps, rbp);
unsigned num_ps = ps.size();
if (num_ps < 2)
throw parser_error("invalid 'obtain' expression, at least 2 binders expected", b_pos);
p.parse_simple_binders(ps, rbp);
for (unsigned i = old_sz; i < ps.size(); i++)
children.push_back(obtain_struct());
}
}
if (children.empty())
throw parser_error("invalid 'obtain' expression, empty declaration block", p.pos());
return obtain_struct(to_list(children));
}
static expr parse_obtain(parser & p, unsigned, expr const *, pos_info const & pos) {
buffer<expr> ps;
obtain_struct s = parse_obtain_decls(p, ps);
p.check_token_next(get_comma_tk(), "invalid 'obtain' expression, ',' expected");
p.check_token_next(get_from_tk(), "invalid 'obtain' expression, 'from' expected");
expr H1 = p.parse_expr();
expr from = p.parse_expr();
p.check_token_next(get_comma_tk(), "invalid 'obtain' expression, ',' expected");
expr b = p.parse_scoped_expr(ps, env);
expr H = ps[num_ps-1];
name H_name = local_pp_name(H);
unsigned i = num_ps-1;
while (i > 1) {
--i;
expr a = ps[i];
expr H_aux = mk_local(p.mk_fresh_name(), H_name.append_after(i), mk_expr_placeholder(), mk_contextual_info(false));
expr H2 = Fun({a, H}, b);
b = mk_app(mk_constant(get_exists_elim_name()), H_aux, H2);
H = H_aux;
}
expr a = ps[0];
expr H2 = Fun({a, H}, b);
expr r = mk_app(mk_constant(get_exists_elim_name()), H1, H2);
return p.rec_save_pos(r, pos);
expr goal = p.parse_scoped_expr(ps);
expr r = p.rec_save_pos(mk_obtain_expr(s, ps, from, goal), pos);
return p.mk_by_plus(p.mk_app(get_exact_tac_fn(), r, pos), pos);
}
static expr * g_not = nullptr;

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

@ -285,6 +285,8 @@ expr elaborator::visit_expecting_type_of(expr const & e, expr const & t, constra
return visit_choice(e, some_expr(t), cs);
} else if (is_by(e)) {
return visit_by(e, some_expr(t), cs);
} else if (is_by_plus(e)) {
return visit_by_plus(e, some_expr(t), cs);
} else if (is_calc_annotation(e)) {
return visit_calc_proof(e, some_expr(t), cs);
} else {
@ -318,6 +320,15 @@ expr elaborator::visit_by(expr const & e, optional<expr> const & t, constraint_s
return m;
}
expr elaborator::visit_by_plus(expr const & e, optional<expr> const & t, constraint_seq & cs) {
lean_assert(is_by_plus(e));
expr tac = visit(get_by_plus_arg(e), cs);
expr m = m_full_context.mk_meta(m_ngen, t, e.get_tag());
register_meta(m);
m_local_tactic_hints.insert(mlocal_name(get_app_fn(m)), tac);
return m;
}
expr elaborator::visit_calc_proof(expr const & e, optional<expr> const & t, constraint_seq & cs) {
lean_assert(is_calc_annotation(e));
info_manager * im = nullptr;
@ -1342,6 +1353,129 @@ expr elaborator::visit_structure_instance(expr const & e, constraint_seq & cs) {
return S_mk;
}
expr elaborator::process_obtain_expr(list<obtain_struct> const & s_list, list<expr> const & from_list,
expr const & goal, bool first, constraint_seq & cs, expr const & src) {
lean_assert(length(s_list) == length(from_list));
if (!s_list && !from_list)
return visit(goal, cs);
expr from = head(from_list);
obtain_struct s = head(s_list);
lean_assert(!first || !s.is_leaf());
if (s.is_leaf()) {
lean_assert(is_local(from));
expr const & from_type = mlocal_type(from);
// fix user visible name
expr goal_domain = visit(binding_domain(goal), cs);
expr new_from = ::lean::mk_local(mlocal_name(from), binding_name(goal), goal_domain, binder_info());
if (!is_lambda(goal))
throw_elaborator_exception("invalid 'obtain' expression, insufficient number of local declarations", src);
justification j = mk_type_mismatch_jst(new_from, goal_domain, from_type, src);
if (!is_def_eq(from_type, goal_domain, j, cs))
throw unifier_exception(j, substitution());
flet<local_context> save1(m_context, m_context);
flet<local_context> save2(m_full_context, m_full_context);
m_context.add_local(new_from);
m_full_context.add_local(new_from);
expr new_goal = instantiate(binding_body(goal), new_from);
expr r = process_obtain_expr(tail(s_list), tail(from_list), new_goal, false, cs, src);
return Fun(new_from, r);
} else {
lean_assert(!first || is_local(from));
expr from_type = whnf(infer_type(from, cs), cs);
buffer<expr> I_args;
expr I = get_app_args(from_type, I_args);
if (!is_constant(I)) {
throw_elaborator_exception(src, [=](formatter const & fmt) {
format r = format("invalid 'obtain' expression, type of 'from' expression is not inductive");
r += pp_indent_expr(fmt, from_type);
return r;
});
}
name const & I_name = const_name(I);
levels const & I_lvls = const_levels(I);
if (!inductive::is_inductive_decl(env(), I_name))
throw_elaborator_exception(sstream() << "invalid 'obtain' expression, '" << I_name
<< "' is not an inductive datatype", src);
if (*inductive::get_num_intro_rules(env(), I_name) != 1)
throw_elaborator_exception(sstream() << "invalid 'obtain' expression, '" << I_name
<< "' has more than one constructor", src);
unsigned nparams = *inductive::get_num_params(env(), I_name);
unsigned nindices = *inductive::get_num_indices(env(), I_name);
declaration cases_on_decl = env().get({I_name, "cases_on"});
levels cases_on_lvls = I_lvls;
if (cases_on_decl.get_num_univ_params() != length(I_lvls))
cases_on_lvls = cons(mk_meta_univ(m_ngen.next()), cases_on_lvls);
expr cases_on = mk_constant(cases_on_decl.get_name(), cases_on_lvls);
tag g = src.get_tag();
expr R = cases_on;
for (unsigned i = 0; i < nparams; i++)
R = mk_app(R, I_args[i], g);
expr R_type = whnf(infer_type(R, cs), cs);
auto check_R_type = [&]() {
if (!is_pi(R_type))
throw_elaborator_exception(sstream() << "invalid 'obtain' expression, '"
<< I_name << "' has an ill-formed cases_on recursor", src);
};
check_R_type();
expr motive_type = binding_domain(R_type);
expr motive = m_full_context.mk_meta(m_ngen, some_expr(motive_type), g);
R = mk_app(R, motive, g);
R_type = whnf(instantiate(binding_body(R_type), motive), cs);
for (unsigned i = 0; i < nindices; i++) {
check_R_type();
expr index_type = binding_domain(R_type);
expr index = m_full_context.mk_meta(m_ngen, some_expr(index_type), g);
R = mk_app(R, index, g);
R_type = whnf(instantiate(binding_body(R_type), index), cs);
}
check_R_type();
expr major_type = binding_domain(R_type);
justification j = mk_type_mismatch_jst(from, from_type, major_type, src);
if (!is_def_eq(from_type, major_type, j, cs))
throw unifier_exception(j, substitution());
R = mk_app(R, from, g);
R_type = whnf(instantiate(binding_body(R_type), from), cs);
check_R_type();
expr minor_type = whnf(binding_domain(R_type), cs);
buffer<expr> telescope;
to_telescope(*m_tc[m_relax_main_opaque], minor_type, telescope, optional<binder_info>(), cs);
lean_assert(!s.is_leaf());
buffer<obtain_struct> s_buffer;
to_buffer(s.get_children(), s_buffer);
if (telescope.size() == 0)
throw_elaborator_exception(sstream() << "invalid 'obtain' expression, '" << I_name
<< "' is an empty type", src);
if (s_buffer.size() < telescope.size())
throw_elaborator_exception("invalid 'obtain' expression, insufficient number of local declarations", src);
if (s_buffer.size() > telescope.size()) {
obtain_struct s_tail(to_list(s_buffer.begin() + telescope.size() - 1, s_buffer.end()));
s_buffer.shrink(telescope.size() - 1);
s_buffer.push_back(s_tail);
}
lean_assert(s_buffer.size() == telescope.size());
list<obtain_struct> new_s_list = to_list(s_buffer.begin(), s_buffer.end(), tail(s_list));
list<expr> new_from_list = to_list(telescope.begin(), telescope.end(), tail(from_list));
expr minor = process_obtain_expr(new_s_list, new_from_list, goal, false, cs, src);
expr infer_minor_type = infer_type(minor, cs);
justification j2 = mk_type_mismatch_jst(minor, infer_minor_type, minor_type, src);
if (!is_def_eq(infer_minor_type, minor_type, j2, cs))
throw unifier_exception(j2, substitution());
expr r = mk_app(R, minor, g);
if (!first)
r = Fun(from, r);
return r;
}
}
expr elaborator::visit_obtain_expr(expr const & e, constraint_seq & cs) {
lean_assert(is_obtain_expr(e));
expr from, decls_goal;
obtain_struct s;
decompose_obtain(e, s, from, decls_goal);
from = visit(from, cs);
return process_obtain_expr(to_list(s), to_list(from), decls_goal, true, cs, e);
}
expr elaborator::visit_core(expr const & e, constraint_seq & cs) {
if (is_placeholder(e)) {
return visit_placeholder(e, cs);
@ -1351,6 +1485,8 @@ expr elaborator::visit_core(expr const & e, constraint_seq & cs) {
return visit_let_value(e, cs);
} else if (is_by(e)) {
return visit_by(e, none_expr(), cs);
} else if (is_by_plus(e)) {
return visit_by_plus(e, none_expr(), cs);
} else if (is_calc_annotation(e)) {
return visit_calc_proof(e, none_expr(), cs);
} else if (is_no_info(e)) {
@ -1379,6 +1515,8 @@ expr elaborator::visit_core(expr const & e, constraint_seq & cs) {
return visit_decreasing(e, cs);
} else if (is_structure_instance(e)) {
return visit_structure_instance(e, cs);
} else if (is_obtain_expr(e)) {
return visit_obtain_expr(e, cs);
} else {
switch (e.kind()) {
case expr_kind::Local: return e;

9
src/frontends/lean/elaborator.h
View file

@ -18,6 +18,7 @@ Author: Leonardo de Moura
#include "frontends/lean/coercion_elaborator.h"
#include "frontends/lean/util.h"
#include "frontends/lean/calc_proof_elaborator.h"
#include "frontends/lean/obtain_expr.h"
namespace lean {
/** \brief Mapping from metavariable names to metavariable applications (?M ...) */
@ -84,6 +85,9 @@ class elaborator : public coercion_info_manager {
pair<expr, constraint_seq> whnf(expr const & e) { return m_tc[m_relax_main_opaque]->whnf(e); }
expr infer_type(expr const & e, constraint_seq & s) { return m_tc[m_relax_main_opaque]->infer(e, s); }
expr whnf(expr const & e, constraint_seq & s) { return m_tc[m_relax_main_opaque]->whnf(e, s); }
bool is_def_eq(expr const & e1, expr const & e2, justification const & j, constraint_seq & cs) {
return m_tc[m_relax_main_opaque]->is_def_eq(e1, e2, j, cs);
}
expr mk_app(expr const & f, expr const & a, tag g) { return ::lean::mk_app(f, a, g); }
void register_meta(expr const & meta);
@ -111,6 +115,7 @@ class elaborator : public coercion_info_manager {
expr visit_expecting_type_of(expr const & e, expr const & t, constraint_seq & cs);
expr visit_choice(expr const & e, optional<expr> const & t, constraint_seq & cs);
expr visit_by(expr const & e, optional<expr> const & t, constraint_seq & cs);
expr visit_by_plus(expr const & e, optional<expr> const & t, constraint_seq & cs);
expr visit_calc_proof(expr const & e, optional<expr> const & t, constraint_seq & cs);
expr add_implict_args(expr e, constraint_seq & cs, bool relax);
pair<expr, expr> ensure_fun(expr f, constraint_seq & cs);
@ -121,6 +126,7 @@ class elaborator : public coercion_info_manager {
justification const & j);
pair<expr, constraint_seq> ensure_has_type(expr const & a, expr const & a_type, expr const & expected_type,
justification const & j, bool relax);
bool is_choice_app(expr const & e);
expr visit_choice_app(expr const & e, constraint_seq & cs);
expr visit_app(expr const & e, constraint_seq & cs);
@ -172,6 +178,9 @@ class elaborator : public coercion_info_manager {
bool is_structure(expr const & S);
expr visit_structure_instance(expr const & e, constraint_seq & cs);
expr process_obtain_expr(list<obtain_struct> const & s_list, list<expr> const & from_list,
expr const & goal, bool first, constraint_seq & cs, expr const & src);
expr visit_obtain_expr(expr const & e, constraint_seq & cs);
public:
elaborator(elaborator_context & ctx, name_generator const & ngen, bool nice_mvar_names = false);
std::tuple<expr, level_param_names> operator()(list<expr> const & ctx, expr const & e, bool _ensure_type,

3
src/frontends/lean/init_module.cpp
View file

@ -29,6 +29,7 @@ Author: Leonardo de Moura
#include "frontends/lean/pp.h"
#include "frontends/lean/server.h"
#include "frontends/lean/local_ref_info.h"
#include "frontends/lean/obtain_expr.h"
namespace lean {
void initialize_frontend_lean_module() {
@ -57,8 +58,10 @@ void initialize_frontend_lean_module() {
initialize_server();
initialize_find_cmd();
initialize_local_ref_info();
initialize_obtain_expr();
}
void finalize_frontend_lean_module() {
finalize_obtain_expr();
finalize_local_ref_info();
finalize_find_cmd();
finalize_server();

113
src/frontends/lean/obtain_expr.cpp Normal file
View file

@ -0,0 +1,113 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <string>
#include "kernel/abstract.h"
#include "kernel/instantiate.h"
#include "library/kernel_serializer.h"
#include "frontends/lean/obtain_expr.h"
namespace lean {
unsigned obtain_struct::size() const {
if (m_leaf) return 1;
unsigned r = 0;
for (auto const & o : m_children) r += o.size();
return r;
}
obtain_struct read_obtain_struct(deserializer & d);
inline serializer & operator<<(serializer & s, obtain_struct const & o) { o.write(s); return s; }
inline deserializer & operator>>(deserializer & d, obtain_struct & o) {
o = read_obtain_struct(d);
return d;
}
void obtain_struct::write(serializer & s) const {
s << m_leaf;
if (!m_leaf)
write_list(s, m_children);
}
obtain_struct read_obtain_struct(deserializer & d) {
bool leaf = d.read_bool();
if (leaf)
return obtain_struct();
return obtain_struct(read_list<obtain_struct>(d));
}
static name * g_obtain_name = nullptr;
static std::string * g_obtain_opcode = nullptr;
[[ noreturn ]] static void throw_ex() { throw exception("unexpected occurrence of 'obtain' expression"); }
class obtain_macro_cell : public macro_definition_cell {
obtain_struct m_struct;
public:
obtain_macro_cell(obtain_struct const & s):m_struct(s) {}
virtual name get_name() const { return *g_obtain_name; }
virtual pair<expr, constraint_seq> get_type(expr const &, extension_context &) const { throw_ex(); }
virtual optional<expr> expand(expr const &, extension_context &) const { throw_ex(); }
virtual void write(serializer & s) const {
s << *g_obtain_opcode << m_struct;
}
obtain_struct const & get_struct() const { return m_struct; }
};
static bool validate(obtain_struct const & s, expr const & decls_goal) {
unsigned sz = s.size();
expr it = decls_goal;
for (unsigned i = 0; i < sz; i++) {
if (!is_lambda(it))
return false;
it = binding_body(it);
}
return true;
}
static expr mk_obtain_expr_core(obtain_struct const & s, expr const & from, expr const & decls_goal) {
lean_assert(validate(s, decls_goal));
macro_definition def(new obtain_macro_cell(s));
expr args[2] = {from, decls_goal};
return mk_macro(def, 2, args);
}
expr mk_obtain_expr(obtain_struct const & s, buffer<expr> const & decls, expr const & from, expr const & goal) {
lean_assert(s.size() == decls.size());
lean_assert(std::all_of(decls.begin(), decls.end(), is_local));
return mk_obtain_expr_core(s, from, Fun(decls, goal));
}
bool is_obtain_expr(expr const & e) {
return is_macro(e) && macro_def(e).get_name() == *g_obtain_name;
}
void decompose_obtain(expr const & e, obtain_struct & s, expr & from, expr & decls_goal) {
lean_assert(is_obtain_expr(e));
s = static_cast<obtain_macro_cell const*>(macro_def(e).raw())->get_struct();
from = macro_arg(e, 0);
decls_goal = macro_arg(e, 1);
}
void initialize_obtain_expr() {
g_obtain_name = new name("obtain");
g_obtain_opcode = new std::string("Obtain");
register_macro_deserializer(*g_obtain_opcode,
[](deserializer & d, unsigned num, expr const * args) {
if (num != 2)
throw corrupted_stream_exception();
obtain_struct s;
d >> s;
if (!validate(s, args[1]))
throw corrupted_stream_exception();
return mk_obtain_expr_core(s, args[0], args[1]);
});
}
void finalize_obtain_expr() {
delete g_obtain_opcode;
delete g_obtain_name;
}
};

28
src/frontends/lean/obtain_expr.h Normal file
View file

@ -0,0 +1,28 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "kernel/expr.h"
namespace lean {
class obtain_struct {
bool m_leaf;
list<obtain_struct> m_children;
public:
obtain_struct():m_leaf(true) {}
obtain_struct(list<obtain_struct> const & c):m_leaf(false), m_children(c) {}
bool is_leaf() const { return m_leaf; }
list<obtain_struct> const & get_children() const { return m_children; }
void write(serializer & s) const;
unsigned size() const;
};
expr mk_obtain_expr(obtain_struct const & s, buffer<expr> const & decls, expr const & from, expr const & goal);
bool is_obtain_expr(expr const & e);
void decompose_obtain(expr const & e, obtain_struct & s, expr & from, expr & decls_goal);
void initialize_obtain_expr();
void finalize_obtain_expr();
}

6
src/frontends/lean/parser.cpp
View file

@ -217,6 +217,12 @@ expr parser::mk_by(expr const & t, pos_info const & pos) {
return save_pos(::lean::mk_by(t), pos);
}
expr parser::mk_by_plus(expr const & t, pos_info const & pos) {
if (!has_tactic_decls())
throw parser_error("invalid 'by+' expression, tactic module has not been imported", pos);
return save_pos(::lean::mk_by_plus(t), pos);
}
void parser::updt_options() {
m_verbose = get_verbose(m_ios.get_options());
m_show_errors = get_parser_show_errors(m_ios.get_options());

1
src/frontends/lean/parser.h
View file

@ -271,6 +271,7 @@ public:
bool has_tactic_decls();
expr mk_by(expr const & t, pos_info const & pos);
expr mk_by_plus(expr const & t, pos_info const & pos);
bool keep_new_thms() const { return m_keep_theorem_mode != keep_theorem_mode::DiscardAll; }

9
src/library/tactic/expr_to_tactic.cpp
View file

@ -324,17 +324,25 @@ void register_num_tac(name const & n, std::function<tactic(unsigned k)> f) {
}
static name * g_by_name = nullptr;
static name * g_by_plus_name = nullptr;
expr mk_by(expr const & e) { return mk_annotation(*g_by_name, e); }
bool is_by(expr const & e) { return is_annotation(e, *g_by_name); }
expr const & get_by_arg(expr const & e) { lean_assert(is_by(e)); return get_annotation_arg(e); }
expr mk_by_plus(expr const & e) { return mk_annotation(*g_by_plus_name, e); }
bool is_by_plus(expr const & e) { return is_annotation(e, *g_by_plus_name); }
expr const & get_by_plus_arg(expr const & e) { lean_assert(is_by_plus(e)); return get_annotation_arg(e); }
void initialize_expr_to_tactic() {
g_tmp_prefix = new name(name::mk_internal_unique_name());
g_by_name = new name("by");
register_annotation(*g_by_name);
g_by_plus_name = new name("by+");
register_annotation(*g_by_plus_name);
g_map = new expr_to_tactic_map();
g_tactic_expr_type = new expr(mk_constant(get_tactic_expr_name()));
@ -425,6 +433,7 @@ void finalize_expr_to_tactic() {
delete g_map;
delete g_tactic_opcode;
delete g_by_name;
delete g_by_plus_name;
delete g_tmp_prefix;
}
}

5
src/library/tactic/expr_to_tactic.h
View file

@ -61,6 +61,11 @@ bool is_by(expr const & t);
/** \see mk_by */
expr const & get_by_arg(expr const & t);
// Similar to mk_by, but instructs the elaborator to include the whole context
expr mk_by_plus(expr const & t);
bool is_by_plus(expr const & t);
expr const & get_by_plus_arg(expr const & t);
expr const & get_tactic_type();
expr const & get_and_then_tac_fn();
expr const & get_or_else_tac_fn();

74
tests/lean/run/new_obtains.lean Normal file
View file

@ -0,0 +1,74 @@
import data.nat
theorem tst2 (A B C D : Type) : (A × B) × (C × D) → C × B × A :=
assume p : (A × B) × (C × D),
obtain [a b] [c d], from p,
(c, b, a)
theorem tst (a b c d : Prop) : (a ∧ b) ∧ (c ∧ d) → c ∧ b ∧ a :=
assume H,
obtain [Ha Hb] Hc Hd, from H,
and.intro Hc (and.intro Hb Ha)
theorem tst22 (A B C D : Type) : (A × B) × (C × D) → C × B × A :=
assume p,
obtain [a b] [c d], from p,
(c, b, a)
theorem tst3 (A B C D : Type) : A × B × C × D → C × B × A :=
assume p,
obtain [[a b] c] d, from p,
(c, b, a)
example (p : nat → nat → Prop) : (∃ x, p x x) → ∃ x y, p x y :=
assume ex,
obtain x pxx, from ex,
exists.intro x (exists.intro x pxx)
example (p q : nat → nat → Prop) : (∃ x y, p x y ∧ q x y ∧ q y x) → ∃ x y, p x y :=
assume ex,
obtain x y pxy qxy qyx, from ex,
exists.intro x (exists.intro y pxy)
example (p : nat → nat → Type): (Σ x, p x x) → (Σ x y, p x y) :=
assume sig,
obtain x pxx, from sig,
⟨x, x, pxx⟩
example (p q : nat → nat → Type) : (Σ x y, p x y × q x y × q y x) → Σ x y, p x y :=
assume ex : Σ x y, p x y × q x y × q y x,
obtain x y [[pxy qxy] qyx], from ex,
⟨x, y, pxy⟩
example (p q : nat → nat → Type) : (Σ x y, p x y × q x y × q y x) → Σ x y, p x y :=
assume ex,
have ex1 : Σ x y, p x y × q x y × q y x, from ex,
obtain x y [[pxy qxy] qyx], from ex1,
⟨x, y, pxy⟩
example (p q : nat → nat → Type) : (Σ x y, p x y × q x y × q y x) → Σ x y, p x y :=
assume ex,
obtain x y [[pxy qxy] qyx], from ex,
⟨x, y, pxy⟩
open nat
definition even (a : nat) := ∃ x, a = 2*x
example (a b : nat) (H₁ : even a) (H₂ : even b) : even (a+b) :=
obtain x (Hx : a = 2*x), from H₁,
obtain y (Hy : b = 2*y), from H₂,
exists.intro
(x+y)
(calc a+b = 2*x + 2*y : by rewrite [Hx, Hy]
... = 2*(x+y) : by rewrite mul.left_distrib)
theorem dvd_of_dvd_add_left {m n₁ n₂ : ℕ} (H₁ : m ∣ n₁ + n₂) (H₂ : m ∣ n₁) : m ∣ n₂ :=
obtain (c₁ : nat) (Hc₁ : n₁ + n₂ = m * c₁), from H₁,
obtain (c₂ : nat) (Hc₂ : n₁ = m * c₂), from H₂,
have aux : m * (c₁ - c₂) = n₂, from calc
m * (c₁ - c₂) = m * c₁ - m * c₂ : by rewrite mul_sub_left_distrib
... = n₁ + n₂ - m * c₂ : Hc₁
... = n₁ + n₂ - n₁ : Hc₂
... = n₂ : add_sub_cancel_left,
dvd.intro aux