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

feat(frontends/lean): allow user to suppress proofs in theorems, and let them be inferred automatically using tactic_hints

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-08 14:38:57 -07:00
parent a3be63af73
commit 5e836092cc
2 changed files with 36 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/frontends/lean/decl_cmds.cpp
View file

@ -245,21 +245,33 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
value = p.parse_expr();
} else if (p.curr_is_token(g_colon)) {
p.next();
auto pos = p.pos();
type = p.parse_expr();
p.check_token_next(g_assign, "invalid declaration, ':=' expected");
value = p.parse_expr();
if (is_theorem && !p.curr_is_token(g_assign)) {
value = mk_expr_placeholder();
} else {
p.check_token_next(g_assign, "invalid declaration, ':=' expected");
value = p.save_pos(p.parse_expr(), pos);
}
} else {
buffer<expr> ps;
optional<local_environment> lenv;
lenv = p.parse_binders(ps);
if (p.curr_is_token(g_colon)) {
p.next();
auto pos = p.pos();
type = p.parse_scoped_expr(ps, *lenv);
if (is_theorem && !p.curr_is_token(g_assign)) {
value = p.save_pos(mk_expr_placeholder(), pos);
} else {
p.check_token_next(g_assign, "invalid declaration, ':=' expected");
value = p.parse_scoped_expr(ps, *lenv);
}
} else {
type = p.save_pos(mk_expr_placeholder(), p.pos());
p.check_token_next(g_assign, "invalid declaration, ':=' expected");
value = p.parse_scoped_expr(ps, *lenv);
}
p.check_token_next(g_assign, "invalid declaration, ':=' expected");
value = p.parse_scoped_expr(ps, *lenv);
type = p.pi_abstract(ps, type);
value = p.lambda_abstract(ps, value);
}

20
tests/lean/run/tactic25.lean Normal file
View file

@ -0,0 +1,20 @@
import standard
using tactic
definition my_tac1 := apply @refl
definition my_tac2 := repeat (apply @and_intro; assumption)
tactic_hint my_tac1
tactic_hint my_tac2
theorem T1 {A : Type.{2}} (a : A) : a = a
theorem T2 {a b c : Bool} (Ha : a) (Hb : b) (Hc : c) : a ∧ b ∧ c
definition my_tac3 := fixpoint (λ f, [apply @or_intro_left; f |
apply @or_intro_right; f |
assumption])
tactic_hint [or] my_tac3
theorem T3 {a b c : Bool} (Hb : b) : a ∨ b ∨ c