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

fix(frontends/lean/parser): bug in add_rewrite

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-02-09 09:46:56 -08:00
parent b24c085cb0
commit 633ed6bb69
3 changed files with 21 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/builtin/num.lean
View file

@ -74,7 +74,7 @@ theorem succ_nz (a : num) : ¬ (succ a = zero)
show false, show false,
from absurd Heq1 (S_ne_Z (rep a)) from absurd Heq1 (S_ne_Z (rep a))
add_rewrite num::succ_nz add_rewrite succ_nz
theorem induction {P : num → Bool} (H1 : P zero) (H2 : ∀ n, P n → P (succ n)) : ∀ a, P a theorem induction {P : num → Bool} (H1 : P zero) (H2 : ∀ n, P n → P (succ n)) : ∀ a, P a
:= take a, := take a,
@ -111,6 +111,8 @@ theorem sn_ne_n (n : num) : succ n ≠ n
(assume R : succ (succ n) = succ n, (assume R : succ (succ n) = succ n,
absurd (succ_inj R) iH)) absurd (succ_inj R) iH))
add_rewrite sn_ne_n
set_opaque num true set_opaque num true
set_opaque Z true set_opaque Z true
set_opaque S true set_opaque S true
@ -136,7 +138,7 @@ theorem lt_nrefl (n : num) : ¬ (n < n)
(assume N : n < n, (assume N : n < n,
lt_elim N (λ P Pred Pn nPn, absurd Pn nPn)) lt_elim N (λ P Pred Pn nPn, absurd Pn nPn))
add_rewrite num::lt_nrefl add_rewrite lt_nrefl
theorem lt_succ {m n : num} : succ m < n → m < n theorem lt_succ {m n : num} : succ m < n → m < n
:= assume H : succ m < n, := assume H : succ m < n,
@ -160,6 +162,8 @@ theorem not_lt_zero (n : num) : ¬ (n < zero)
show false, show false,
from absurd nLTzero iH)) from absurd nLTzero iH))
add_rewrite not_lt_zero
theorem zero_lt_succ_zero : zero < succ zero theorem zero_lt_succ_zero : zero < succ zero
:= let P : num → Bool := λ x, x = zero := let P : num → Bool := λ x, x = zero
in have Ppred : ∀ i, P (succ i) → P i, in have Ppred : ∀ i, P (succ i) → P i,
@ -221,6 +225,8 @@ theorem n_lt_succ_n (n : num) : n < succ n
(λ (n : num) (iH : n < succ n), (λ (n : num) (iH : n < succ n),
succ_mono_lt iH) succ_mono_lt iH)
add_rewrite n_lt_succ_n
theorem lt_to_neq {m n : num} : m < n → m ≠ n theorem lt_to_neq {m n : num} : m < n → m ≠ n
:= assume H : m < n, := assume H : m < n,
lt_elim H lt_elim H
@ -239,7 +245,7 @@ theorem zero_lt_succ_n {n : num} : zero < succ n
(λ (n : num) (iH : zero < succ n), (λ (n : num) (iH : zero < succ n),
lt_to_lt_succ iH) lt_to_lt_succ iH)
add_rewrite num::zero_lt_succ_n add_rewrite zero_lt_succ_n
theorem lt_succ_to_disj {m n : num} : m < succ n → m = n ∨ m < n theorem lt_succ_to_disj {m n : num} : m < succ n → m = n ∨ m < n
:= assume H : m < succ n, := assume H : m < succ n,
@ -508,6 +514,8 @@ theorem mul_zeror (a : num) : a * zero = zero
theorem mul_succr (a b : num) : a * (succ b) = a * b + a theorem mul_succr (a b : num) : a * (succ b) = a * b + a
:= prim_rec_succ zero (λ x n, x + a) b := prim_rec_succ zero (λ x n, x + a) b
add_rewrite add_zeror add_succr mul_zeror mul_succr
set_opaque add true set_opaque add true
set_opaque mul true set_opaque mul true
end end

BIN
src/builtin/obj/num.olean
View file

Binary file not shown.

14
src/frontends/lean/parser_cmds.cpp
View file

@ -850,7 +850,15 @@ void parser_imp::parse_rewrite_set() {
void parser_imp::parse_ids_and_rsid(buffer<name> & ids, name & rsid) { void parser_imp::parse_ids_and_rsid(buffer<name> & ids, name & rsid) {
while (curr_is_identifier()) { while (curr_is_identifier()) {
ids.push_back(curr_name()); auto p = pos();
name id = curr_name();
expr d = get_name_ref(id, p, false);
if (is_constant(d))
ids.push_back(const_name(d));
else if (is_value(d))
ids.push_back(to_value(d).get_name());
else
throw parser_error(sstream() << "'" << id << "' does not name a theorem or axiom", p);
next(); next();
} }
if (ids.empty()) if (ids.empty())
@ -869,10 +877,6 @@ void parser_imp::parse_add_rewrite() {
name rsid; name rsid;
parse_ids_and_rsid(th_names, rsid); parse_ids_and_rsid(th_names, rsid);
for (auto id : th_names) { for (auto id : th_names) {
auto it = m_using_decls.find(id);
if (it != m_using_decls.end())
add_rewrite_rules(m_env, rsid, it->second);
else
add_rewrite_rules(m_env, rsid, id); add_rewrite_rules(m_env, rsid, id);
} }
} }