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

feat(frontends/lean/builtin_exprs): add 'have' notation in 'begin-end' blocks

Browse source 
It is notation for the assert tactic.
This commit is contained in:
Leonardo de Moura 2015-02-25 13:58:39 -08:00
parent daf27fd194
commit 96b54a8007
6 changed files with 149 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -20,6 +20,7 @@ Author: Leonardo de Moura
#include "library/let.h"
#include "library/constants.h"
#include "library/definitional/equations.h"
#include "library/tactic/assert_tactic.h"
#include "frontends/lean/builtin_exprs.h"
#include "frontends/lean/decl_cmds.h"
#include "frontends/lean/token_table.h"
@ -153,6 +154,14 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos, name const &
optional<expr> pre_tac = get_begin_end_pre_tactic(env);
buffer<expr> tacs;
bool first = true;
auto add_tac = [&](expr tac, pos_info const & pos) {
if (pre_tac)
tac = p.mk_app({get_and_then_tac_fn(), *pre_tac, tac}, pos);
tac = mk_begin_end_element_annotation(tac);
tacs.push_back(tac);
};
while (!p.curr_is_token(end_token)) {
if (first) {
first = false;
@ -172,18 +181,52 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos, name const &
tacs.push_back(parse_begin_end_core(p, pos, get_rcurly_tk(), true));
} else if (p.curr_is_token(end_token)) {
break;
} else {
bool use_exact = (p.curr_is_token(get_have_tk()) || p.curr_is_token(get_show_tk()) ||
p.curr_is_token(get_assume_tk()) || p.curr_is_token(get_take_tk()) ||
p.curr_is_token(get_fun_tk()));
} else if (p.curr_is_token(get_have_tk())) {
auto pos = p.pos();
expr tac = p.parse_expr();
if (use_exact)
tac = p.mk_app(get_exact_tac_fn(), tac, pos);
if (pre_tac)
tac = p.mk_app({get_and_then_tac_fn(), *pre_tac, tac}, pos);
tac = mk_begin_end_element_annotation(tac);
tacs.push_back(tac);
p.next();
name id = p.check_id_next("invalid 'have' tactic, identifier expected");
p.check_token_next(get_colon_tk(), "invalid 'have' tactic, ':' expected");
expr A = p.parse_expr();
p.check_token_next(get_comma_tk(), "invalid 'have' tactic, ',' expected");
expr assert_tac = p.save_pos(mk_assert_tactic_expr(id, A), pos);
tacs.push_back(mk_begin_end_element_annotation(assert_tac));
if (p.curr_is_token(get_from_tk())) {
// parse: 'from' expr
p.next();
auto pos = p.pos();
expr t = p.parse_expr();
t = p.mk_app(get_exact_tac_fn(), t, pos);
add_tac(t, pos);
} else if (p.curr_is_token(get_proof_tk())) {
auto pos = p.pos();
p.next();
expr t = p.parse_expr();
p.check_token_next(get_qed_tk(), "invalid proof-qed, 'qed' expected");
t = p.mk_app(get_exact_tac_fn(), t, pos);
add_tac(t, pos);
} else if (p.curr_is_token(get_begin_tk())) {
auto pos = p.pos();
tacs.push_back(parse_begin_end_core(p, pos, get_end_tk(), true));
} else if (p.curr_is_token(get_by_tk())) {
// parse: 'by' tactic
auto pos = p.pos();
p.next();
expr t = p.parse_expr();
add_tac(t, pos);
} else {
throw parser_error("invalid 'have' tactic, 'by', 'begin', 'proof', or 'from' expected", p.pos());
}
} else if (p.curr_is_token(get_show_tk()) ||
p.curr_is_token(get_assume_tk()) || p.curr_is_token(get_take_tk()) ||
p.curr_is_token(get_fun_tk())) {
auto pos = p.pos();
expr t = p.parse_expr();
t = p.mk_app(get_exact_tac_fn(), t, pos);
add_tac(t, pos);
} else {
auto pos = p.pos();
expr t = p.parse_expr();
add_tac(t, pos);
}
}
auto end_pos = p.pos();
@ -271,7 +314,7 @@ static expr parse_proof(parser & p, expr const & prop) {
}
return pr;
} else {
throw parser_error("invalid expression, 'by', 'using' or 'from' expected", p.pos());
throw parser_error("invalid expression, 'by', 'begin', 'proof', 'using' or 'from' expected", p.pos());
}
}

5
src/library/tactic/assert_tactic.cpp
View file

@ -11,6 +11,11 @@ Author: Leonardo de Moura
#include "library/tactic/expr_to_tactic.h"
namespace lean {
expr mk_assert_tactic_expr(name const & id, expr const & e) {
return mk_app(mk_constant(get_tactic_assert_hypothesis_name()),
mk_constant(id), e);
}
tactic assert_tactic(elaborate_fn const & elab, name const & id, expr const & e) {
return tactic01([=](environment const & env, io_state const & ios, proof_state const & s) {
proof_state new_s = s;

1
src/library/tactic/assert_tactic.h
View file

@ -8,6 +8,7 @@ Author: Leonardo de Moura
#include "library/tactic/tactic.h"
namespace lean {
expr mk_assert_tactic_expr(name const & id, expr const & e);
tactic assert_tactic(elaborate_fn const & elab, name const & id, expr const & e);
void initialize_assert_tactic();
void finalize_assert_tactic();

48
tests/lean/run/assert_tac.lean
View file

@ -2,7 +2,7 @@ import logic
variables {A : Type} {a a' : A}
definition to_eq (H : a == a') : a = a' :=
definition to_eq₁ (H : a == a') : a = a' :=
begin
assert (H₁ : ∀ (Ht : A = A), eq.rec_on Ht a = a),
intro Ht,
@ -10,3 +10,49 @@ begin
show a = a', from
heq.rec_on H H₁ (eq.refl A)
end
definition to_eq₂ (H : a == a') : a = a' :=
begin
have H₁ : ∀ (Ht : A = A), eq.rec_on Ht a = a,
begin
intro Ht,
exact (eq.refl (eq.rec_on Ht a))
end,
show a = a', from
heq.rec_on H H₁ (eq.refl A)
end
definition to_eq₃ (H : a == a') : a = a' :=
begin
have H₁ : ∀ (Ht : A = A), eq.rec_on Ht a = a,
by intro Ht; exact (eq.refl (eq.rec_on Ht a)),
show a = a', from
heq.rec_on H H₁ (eq.refl A)
end
definition to_eq₄ (H : a == a') : a = a' :=
begin
have H₁ : ∀ (Ht : A = A), eq.rec_on Ht a = a,
from assume Ht, eq.refl (eq.rec_on Ht a),
show a = a', from
heq.rec_on H H₁ (eq.refl A)
end
definition to_eq₅ (H : a == a') : a = a' :=
begin
have H₁ : ∀ (Ht : A = A), eq.rec_on Ht a = a,
proof
λ Ht, eq.refl (eq.rec_on Ht a)
qed,
show a = a', from
heq.rec_on H H₁ (eq.refl A)
end
definition to_eq₆ (H : a == a') : a = a' :=
begin
have H₁ : ∀ (Ht : A = A), eq.rec_on Ht a = a, from
assume Ht,
eq.refl (eq.rec_on Ht a),
show a = a', from
heq.rec_on H H₁ (eq.refl A)
end

40
tests/lean/run/assert_tac2.lean Normal file
View file

@ -0,0 +1,40 @@
import data.nat
open nat eq.ops
theorem lcm_dvd {m n k : nat} (H1 : m | k) (H2 : n | k) : lcm m n | k :=
match eq_zero_or_pos k with
@or.inl _ _ kzero :=
begin
rewrite kzero,
apply dvd_zero
end,
@or.inr _ _ kpos :=
obtain (p : nat) (km : k = m * p), from exists_eq_mul_right_of_dvd H1,
obtain (q : nat) (kn : k = n * q), from exists_eq_mul_right_of_dvd H2,
begin
have mpos : m > 0, from pos_of_dvd_of_pos H1 kpos,
have npos : n > 0, from pos_of_dvd_of_pos H2 kpos,
have gcd_pos : gcd m n > 0, from gcd_pos_of_pos_left n mpos,
have ppos : p > 0,
begin
apply pos_of_mul_pos_left,
apply (eq.rec_on km),
exact kpos
end,
have qpos : q > 0, from pos_of_mul_pos_left (kn ▸ kpos),
have H3 : p * q * (m * n * gcd p q) = p * q * (gcd m n * k),
begin
apply sorry
end,
have H4 : m * n * gcd p q = gcd m n * k, from
!eq_of_mul_eq_mul_left (mul_pos ppos qpos) H3,
have H5 : gcd m n * (lcm m n * gcd p q) = gcd m n * k,
begin
rewrite [-mul.assoc, gcd_mul_lcm],
exact H4
end,
have H6 : lcm m n * gcd p q = k, from
!eq_of_mul_eq_mul_left gcd_pos H5,
exact (dvd.intro H6)
end
end

2
tests/lean/run/vector.lean
View file

@ -115,7 +115,7 @@ namespace vector
begin
cases v with (n₂, h₂, t₂),
have r : vector B n₂ → vector C n₂, from pr₁ b,
(f h₁ h₂) :: r t₂,
exact ((f h₁ h₂) :: r t₂),
end
end) v