From 633ed6bb6903e847f7b9c9d31707279f016d8a37 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 9 Feb 2014 09:46:56 -0800 Subject: [PATCH] fix(frontends/lean/parser): bug in add_rewrite Signed-off-by: Leonardo de Moura --- src/builtin/num.lean | 14 +++++++++++--- src/builtin/obj/num.olean | Bin 25180 -> 25264 bytes src/frontends/lean/parser_cmds.cpp | 16 ++++++++++------ 3 files changed, 21 insertions(+), 9 deletions(-) diff --git a/src/builtin/num.lean b/src/builtin/num.lean index cef353259..7b111fae5 100644 --- a/src/builtin/num.lean +++ b/src/builtin/num.lean @@ -74,7 +74,7 @@ theorem succ_nz (a : num) : ¬ (succ a = zero) show false, 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 := take a, @@ -111,6 +111,8 @@ theorem sn_ne_n (n : num) : succ n ≠ n (assume R : succ (succ n) = succ n, absurd (succ_inj R) iH)) +add_rewrite sn_ne_n + set_opaque num true set_opaque Z true set_opaque S true @@ -136,7 +138,7 @@ theorem lt_nrefl (n : num) : ¬ (n < n) (assume N : n < n, 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 := assume H : succ m < n, @@ -160,6 +162,8 @@ theorem not_lt_zero (n : num) : ¬ (n < zero) show false, from absurd nLTzero iH)) +add_rewrite not_lt_zero + theorem zero_lt_succ_zero : zero < succ zero := let P : num → Bool := λ x, x = zero 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), succ_mono_lt iH) +add_rewrite n_lt_succ_n + theorem lt_to_neq {m n : num} : m < n → m ≠ n := assume H : m < n, lt_elim H @@ -239,7 +245,7 @@ theorem zero_lt_succ_n {n : num} : zero < succ n (λ (n : num) (iH : zero < succ n), 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 := 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 := 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 mul true end diff --git a/src/builtin/obj/num.olean b/src/builtin/obj/num.olean index 1ecd933e5c503e620318a650c41945f4487b03bb..20099b0503a6821381f3070f03a0ca849a13c762 100644 GIT binary patch delta 2069 zcmZWqYfx2H6h7;m^a>n=i@>>P0$$~i76*>lD8F>a3wV_E-ENYT|sD))^m|AM(A2GDO_C`+L__5|Y-?v_SuYDJNr=hJ2 z+M>NiNbK(goaI%aRT8{lB3n)7B8MyV4lj=%POMJ(}dVJM)w!e!Am*Ce++;t{qd5*(=-<@V>d3kAF9eGI0$!x~8=4{x8z2wxX9jN-R%J_hEk+Io; zEd)it0fwN6XKW?7g~Njc-wbC~dW(#ae4lwg`&IxTv&Ko1v=!F{%!H4zBOrtoy%bQz z@A?qt1SY6Q$U&4picNugU_aWl$NrA5Obyrb1H)@e!p-z{}wtu;{p z)Y1cLuaWIrJRWS-kB&W{znOO?GDoh;1;%r%!UD0BW!M$WRh2q1M5Xzo=QMo z6~?daJbg%hWa#{o$$d)q&>ouNEj=Jnoa7K$$(o)@W$|oIV$goSA;S8riqsoFk^W{rW!+$ zf}f0?5gBj~M@R04Xl#uvRO1YB2Kq!LvzV`Ksk1DawCGm9{FwA2{nZ%);LCKH9 z1iTxy8sf1c`gv;#(ZZQun2CEVV5BmO!$tU8bQ*Jxi?Kp77Q`gSW*H%i35t+xBjh<^ zT@iHgETo48W@6S<4M$G?-kM9AsFz1j1m`m}RIfl+rt|@%;g#5xki+6qt^B7fVycW7 z`c)6btY9Mu#BZkFfKEIyZ9J^ROVdi#dh&JA)L^xq_|#rmO*EJ!{jaA_0c_Tf#GO?h z6Y!1MZEUo2=A31N*Og~qR^Sy}Gp|sk#W0kw0e_z7U|WPv6>p0x-b0e;@Lhu9RPQk~ z)ZzQYvW+1xtrc%VQgTQw=1T+!OOh`c8yWs6OhT*Rqiy816niVy+9J$+GR@>EUPueS zfcy3}+QCVTgmRMjLlhJL5Z_L?0*zSXSZMx;G;uA57?OA4PYXlQcfN;y*Rc%L|H}HZ z#MN%hwWLbGn>Gtpq|9JrZAz)uIw+wy{BeTf@Fy@VHSO_iYf>HZV+?+|upjp7hZkK0 zwkBNZwQvjv(;MInZp`=-y78sVH0ah(XPRMLH)ZB~H;I7}`^Yr&Yv{&1S#^H=uo5k_ zq58dg{o*Wo)`h}u08UDsO#V^8jmep>70VC0UBhf$TQ8G@xE}>6ppv)EnHIQ2p zWdXjvMBRtO?y`j2OM>AKY%i&q1%r$q-s%wlXum`9Fv=W8eZ%M~7ME6mj9-*Gygewh zi|g{@+f!0)14UO TPH02_p=9|{x3V|d%bxrf3vaO+ delta 1978 zcmZ8iYfKbZ6rMAKf@M(Nvtrn#D~db>C57S>Se`{5mGBS>EGTQLF0g=@6w{<6STGAQ zdV-BoYh#mwRvYN_M+>Rc7sixe($qqfHkQ8aLq*e9Qrmm(1*UY9J^ALG?>pztx#!*) zxCT>KVIazTsfS$OQYSUH?Am3oZ@Ii-^!i0AMy!GzTc1)W&x8w!W8#dm{GH#ywGe+Y+thq1%25D;(swZSp0@b5}H z$r(IJuK`~tn8CfL7y<`}ZxD1wP>fd+E9$}MfFIxl1_m}K^;1l&?yLdN5ftQi7=m)1 z?L5IQ4lm$HU=UCu3qB5P_v>RJ1po?MH4I78F+3dfEDYkMAPXz>RgiO;=%aJLy}rq@ z+bLmTaH={)R8f2wPY0iZKHQ?kz=yb3ONOiX#IhW(Xi+eLziKY#wVN{Ws5Mw0GmU}z zxuKoF8)mCM8gf>FTj(<9sgI1Ku*&kDYyxugD&C%3 z^dR|@;T`bA>aZ*ykjcT92?|SR#!th>WB`2g=~7iSVm_!?JHQ*=*3ID0N`>IGH9Td8 z2+}ASk@LAa7d?O<8K|kPwKp}9L)s%+)aqzzu(Ljik&`fSWsz#4xLCn*{rJi+6wq*g zM1i{A@WyDtlGszSa7GrgshQTp+tS?YZh${#RaV0~u;wn90?G!*EK8S6Aa;D3+HWE>2 zcsqrr+0g7~TM~?S}o5?++NJULA_}G8ClISJlk~nnJWNY`e?#+ zWkCQ>Y#3l$owM;e8w5RI(@P4pVfWTDwaZX<&~{x3p{uy=R4@vFK?R! z7{%VaM!1MR`5iEZJ^2q|96JhfVO;;LzzhN(~1~5*ZrIipP-B6zu^~MXiSfMMq|^v9uj7<8P&9a8ZALM>@bw z>?s?82`nx@3YYco%XiA~C+1Whfcq?KiizJ&B9RR9iDVg & ids, name & rsid) { 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(); } if (ids.empty()) @@ -869,11 +877,7 @@ void parser_imp::parse_add_rewrite() { name rsid; parse_ids_and_rsid(th_names, rsid); 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); } }