From 69d7ee316f7bb83035a015e106064de0809e333f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 19 Jan 2014 23:26:34 -0800 Subject: [PATCH] feat(library/simplifier): improve simplification by evaluation Signed-off-by: Leonardo de Moura --- src/builtin/kernel.lean | 6 ++ src/builtin/obj/kernel.olean | Bin 25173 -> 25242 bytes src/kernel/kernel_decls.cpp | 2 + src/kernel/kernel_decls.h | 4 ++ src/library/simplifier/simplifier.cpp | 57 +++++++++++++-- tests/lean/simp3.lean | 100 ++++++++++++++++++++++++++ tests/lean/simp3.lean.expected.out | 35 +++++++++ 7 files changed, 198 insertions(+), 6 deletions(-) create mode 100644 tests/lean/simp3.lean create mode 100644 tests/lean/simp3.lean.expected.out diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean index 4475f913cb..941989026c 100644 --- a/src/builtin/kernel.lean +++ b/src/builtin/kernel.lean @@ -298,6 +298,12 @@ theorem imp_falser (a : Bool) : (a → false) ↔ ¬ a theorem imp_falsel (a : Bool) : (false → a) ↔ true := case (λ x, (false → x) ↔ true) trivial trivial a +theorem not_true : ¬ true ↔ false +:= trivial + +theorem not_false : ¬ false ↔ true +:= trivial + theorem not_and (a b : Bool) : ¬ (a ∧ b) ↔ ¬ a ∨ ¬ b := case (λ x, ¬ (x ∧ b) ↔ ¬ x ∨ ¬ b) (case (λ y, ¬ (true ∧ y) ↔ ¬ true ∨ ¬ y) trivial trivial b) diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean index fd632297616f7d5aed5a592df2618236685eda88..a3d87a9decae28863288c4787458b553b976755d 100644 GIT binary patch delta 4796 zcmai13s6+o8NTPT_p-c1WEW(W1r$UP1rd|TjB|a1DBT2V{2_EX?4b)?>~3s|ch zgNAIw*86B{L2c|&_!x#9#4!>j>2$B4JX+2oHb7BC$BJ_XW7^IUhX8J(XD8N*&Gi06 z_wb*>O1Zyj!?$3zd3&MTxhGSXSiDNrr9;IVR9x5)`!n0_ZI1YIVU=k|BTrGh*hD!+ z4;38Xn8~oeiD3|@c^XiKJY&PN5=I=Ly+v;4Nfq-1$2>(>iXM)A$2L62F+VDfrk>(P zv4IX3H<+8Cj-;&H_gy+N z$shYG+wlG4qQn%*S8T~u8(t%CsmB?i7I=>r_>kt5jxRVLmWra_H@4?*ZTOLd5$EYd zX|A|VpOtRS{unyJ$^Q;8m*MXLy$nB*$dODhl%<(N0X=l4EXSpwoNJK{OP1qT+@O19 zvorq4m_0uO%pENUy$KLPM-FX^aMQQSqY`toxa`-V(psULKnKfnJ^6;dhGlW1HJF~M>8Grr90bI z_`h-Zf6(W?3eicUD{Cvif_W-0@^3)p`5!>lSa&3HbY?SSTyD(=3726Z9jf$+rSzxD z3~`sDtMX!(8oK|{74UW}rMjxMVhx?D${M;3g4LsVkvwPxlk#=CTQy01NrlxfBG8_BF09od%+$r386@r~Ifp%!WA ztMRM(WrBh+Ub{=*mP-en959)(GE7!!AZDLOt820xZ`^!SBq>Hj1(_!i5w?6H!i{%hQlCz zm-N~kaf!y&rX{==Y=5=AOEj-GE%{oovy~KQ)p03{K8bVDOSSRlbm{Rj@#5z ze=I4ILk?%L90V>7p^_g%TQ0hQ)wU2+N(Jfn^*m5DgobViqZq&;e%0Y|c1F{|vDH$$0 z;m?gt!n_RkfsszP{6%ANfS7)*j2E!y;R_^DOGAqA(&G*J=@kJl17$a|!(zGV?S^#W zq8kk(((N7Kjxk0Ai>}ftBJb463Dr`?+YoJ>MK!IMnj(tmxv6!d65*C0JGJ`}SZV%n zBA|EE^UWR_-01P91W1j9oYPB{NcvBuwknDq@S2=gDjjR~PRNHHN+d3$eU>uuMjzHy zG@{wH8}h%wO}1$JbWaFZ)ut^)?@4xJ0M6XeO>1&$icmuMbkwB(Cf)Y?*)>a_Y_skYKi_d(30zsz~Nc>CRgJc zeKjlCnp@$dX!tfzDCbsdu9BP&C;x1hc#h`HUSGWfF6y=N9YE#%T|h6+48NJoAtnSk zof&9|-6xF(%}EtRxpNi`p!C*T z@rQu?c+`IcsM7c`pcm`dC*3TNQ@)1GiT_J8gw;shQ78v31N3TL4CP?*E1u_(8b~%1 zXjn&@yke1=NFuk7^bo7r)dhM^4RP9eT3mRKB9O zb&eCm=u~I2=%Z_$l`-6cXlqkmpz}sdn6K=lKs|Q(d!wfW=H|jI300CH$APtyoZ3w0 zb0ck=SL@;r9k*xjz`iE)_EKb5>p(A7;=e}p(|~FlX8_eU&H{#)bhDJ1xc|&8VI^fv z53AKf9iJmvR7h};%0&ntfN0p}ckCgw-{W2g9rsTsS n=}2#K)0>by`1hPv8Me(6uv6>4Ad$IW4%Xs<0-mG6^XvW#NnBR7 delta 4762 zcmbVQdr*|u760zXcRvU$0I@owQA2OefFjbb5d1?y}o8?H|ny z*WW$o+;h(TopbMZH{U)ZF1;*{j?baD=QKE;GSq)kszLmOyp^kxra_Q|p^o-d)KCyoy{JyG!j>8<@1=FbTFGiN0jKEV0#vP6cFWMk| zL5F{i!=Iq6>K@0>BMVO}M)D}HCXpVmZc}O8sBTqh+^7Z%UU8O!H5oa-h?t*?z*ph? zEFG)KOZbBh@e+r4g+8bWIDQ#1{1t~-H}5aCzljJhM&KpD&th^n9#BF{XvgQ-@dbLM zwrtKBW@Q%EM6vQZ=9r3m(r1>S5C1d+y92j1#GN5v9B;Hy%?>Y!6>q}@^Lz#-QdB92E zYDlg9D>QmTe*@GT`ny6_aV)dlkTz>(uQ9W4(*q^Qr9Q zV?e#~6ToDaeyWhwSHuJ|3q~U(T#I#d-Pb5aX?9b-_>4N5${nN942*2SYHO74Z@Not zC#$*8eGdfNX0VfTXa%#dljb+qh!0gdF51_;w%3J-rhoybWMY9%$&3T!luSz@>p-y@ z#qAg_U_OGur3NEj9oMe~@=_|CTrDXj%uHL8~5sKrY ziHvylXPpP3X1f~n=5MlRQ=KgAFHM{oZT~ui=L+d+vXkCvNwIO-tcxW4oi?jZQLlfh zNTY53foYrs-xp?~GSgRw$tOk5#NN#``pCbxU}i*F5`ldCNa(B^^s#?Bom;rKRI(#J z^Vqq-9V7U(ntYmdG;Tggql-Mr(q@L{DmxiZqRlB1==7q1NFhgHp>MKn-ljB$F^Zv1 z{mJwRg4nHO@>%1I)zH4c7pByrkrS|TimgVomLctKb&ARKuRy88sRTwHZW)<0c#aMc-7%gk>9xgvJ58x%3T3xt+3+vZslIJ)t}DzR zR_esE;p5ksdTDQ4b`@JA5pgA!KPA+hSH^1St+s+x9S5EkV^~Bf?d4^qfGrqMWZB5P zqPm)!Y6zP`-wks%z0{dOr+X@r$JQ!^VN^ja>16wq9JGZ@;O6i{r8{RKL%PzgI;WqN z_`J&jnz|%Qb)pCzO0@xVlhj}YFmP2o3djNkH15EFT`}!!Ba0v^ruKZdDaYv8 zt=W!D$kYH(rZsygt`0+(13h=$DTcGEX4X{=CCyb$%_Z{Sn51`jbBf%I5~) zeehdRJ_%{~>1M8_`m6sou?yyTifDc;M@@1`r<& zITF4C@nF)FBx%mWCMMPNY!_SUsh+N48I>C&TDTp*LT@hj=Wr1&u}hqqP`o`1si^n!dvdFy+AHp($9jX! z2Vkn-A$-SZ!oCSV4o*3Eu7FHI?}gsb{Z$} z1FY9P{SZ*U8jk=*@zg@it7eK8+PJD)`03=T;xacZ^wSI3#4%i6MW3PXzu3nd}2|dtIR#b?RWx%B1J}r-~q5?r(A89dB@(P8`{zY8#si z2BFZ;{ucrDZcYN~-JC)p8@{UM_7H}z#T1e?dW-t`{f4sAvFv-Xpr29)J>n>N2R(^{ zVGd8w%E3Dq_CY_$m3tYBbnr8Px^ia$qo^ELQ~O|;%JC4DlZJ|OT}os9H$J~h-9xnv z%mID}?5KcS`w;jtAI0^~Eb^D#+QID@RKn0)AtRs8H)Ybbp{!l#Fq{8RgcVefZR{r$ z3b7l`?I394FEamVvN9*aaPjO%ums6)E|x1&+kjG7;}P=!^K%aNf$6mKw$e301w}W+ zd{#p5#>r}G;gU7+GBc9(?jU>=^LX`VA5sDNq*<9!0mHx25!vv;?iorPo>~@EP;c-# Wg+d new_rhs = to_value(f).normalize(num_args(rhs.m_out), &arg(rhs.m_out, 0)); - if (new_rhs) { + if (evaluate_app(rhs.m_out)) { + // try to evaluate if all arguments are values. + expr new_rhs = normalize(rhs.m_out); + if (is_value(new_rhs)) { // We don't need to create a new proof term since rhs.m_out and new_rhs are // definitionally equal. - return rewrite(lhs, result(*new_rhs, rhs.m_proof, rhs.m_heq_proof)); + return rewrite(lhs, result(new_rhs, rhs.m_proof, rhs.m_heq_proof)); } } + expr f = arg(rhs.m_out, 0); if (m_beta && is_lambda(f)) { expr new_rhs = head_beta_reduce(rhs.m_out); // rhs.m_out and new_rhs are also definitionally equal @@ -492,7 +531,12 @@ class simplifier_fn { } } } - return rhs; + if (!m_single_pass && lhs != rhs.m_out) { + result new_rhs = simplify(rhs.m_out); + return mk_trans_result(lhs, rhs, new_rhs); + } else { + return rhs; + } } result simplify_var(expr const & e) { @@ -604,6 +648,7 @@ class simplifier_fn { result simplify_pi(expr const & e) { lean_assert(is_pi(e)); + // TODO(Leo): handle implication, i.e., e is_proposition and is_arrow if (m_has_heq) { // TODO(Leo) return result(e); diff --git a/tests/lean/simp3.lean b/tests/lean/simp3.lean new file mode 100644 index 0000000000..089071fe95 --- /dev/null +++ b/tests/lean/simp3.lean @@ -0,0 +1,100 @@ +definition double x := x + x + +(* +function show(x) print(x) end +local t1 = parse_lean("0 ≠ 1") +show(simplify(t1)) +local t2 = parse_lean("3 ≥ 2") +show(simplify(t2)) +local t3 = parse_lean("double (double 2) + 1") +show(simplify(t3)) +local t4 = parse_lean("0 = 1") +show(simplify(t4)) +*) + +(* +local opt = options({"simplifier", "unfold"}, true, {"simplifier", "eval"}, false) +local t1 = parse_lean("double (double 2) + 1 ≥ 3") +show(simplify(t1, 'default', get_environment(), context(), opt)) +*) + +set_opaque Nat::ge false +add_rewrite Nat::add_assoc +add_rewrite Nat::distributer +add_rewrite Nat::distributel + +(* +local opt = options({"simplifier", "unfold"}, true, {"simplifier", "eval"}, false) +local t1 = parse_lean("2 * double (double 2) + 1 ≥ 3") +show(simplify(t1, 'default', get_environment(), context(), opt)) +*) + +variables a b c d : Nat + +import if_then_else +add_rewrite if_true +add_rewrite if_false +add_rewrite if_a_a +add_rewrite Nat::add_zeror +add_rewrite Nat::add_zerol +add_rewrite eq_id + +(* +local t1 = parse_lean("(a + b) * (c + d)") +local r, pr = simplify(t1) +print(r) +print(pr) +*) + +theorem congr2_congr1 {A B C : TypeU} {f g : A → B} (h : B → C) (Hfg : f = g) (a : A) : + congr2 h (congr1 a Hfg) = congr2 (λ x, h (x a)) Hfg +:= proof_irrel (congr2 h (congr1 a Hfg)) (congr2 (λ x, h (x a)) Hfg) + +theorem congr2_congr2 {A B C : TypeU} {a b : A} (f : A → B) (h : B → C) (Hab : a = b) : + congr2 h (congr2 f Hab) = congr2 (λ x, h (f x)) Hab +:= proof_irrel (congr2 h (congr2 f Hab)) (congr2 (λ x, h (f x)) Hab) + +theorem congr1_congr2 {A B C : TypeU} {a b : A} (f : A → B → C) (Hab : a = b) (c : B): + congr1 c (congr2 f Hab) = congr2 (λ x, f x c) Hab +:= proof_irrel (congr1 c (congr2 f Hab)) (congr2 (λ x, f x c) Hab) + +rewrite_set proofsimp +add_rewrite congr2_congr1 congr2_congr2 congr1_congr2 : proofsimp + +(* +local t2 = parse_lean("(if a > 0 then b else b + 0) + 10 = (if a > 0 then b else b) + 10") +local r, pr = simplify(t2) +print(r) +print(pr) +show(simplify(pr, 'proofsimp')) +*) + + +(* +local t1 = parse_lean("(a + b) * (a + b)") +local t2 = simplify(t1) +print(t2) +*) + +-- add_rewrite imp_truer imp_truel imp_falsel imp_falser not_true not_false +-- print rewrite_set + +(* +local t1 = parse_lean("true → false") +print(simplify(t1)) +*) + +(* +local t1 = parse_lean("true → true") +print(simplify(t1)) +*) + +(* +local t1 = parse_lean("false → false") +print(simplify(t1)) +*) + +(* +local t1 = parse_lean("true ↔ false") +print(simplify(t1)) +*) \ No newline at end of file diff --git a/tests/lean/simp3.lean.expected.out b/tests/lean/simp3.lean.expected.out new file mode 100644 index 0000000000..24877ac4e7 --- /dev/null +++ b/tests/lean/simp3.lean.expected.out @@ -0,0 +1,35 @@ + Set: pp::colors + Set: pp::unicode + Defined: double +⊤ +⊤ +9 +⊥ +2 + 2 + (2 + 2) + 1 ≥ 3 +3 ≤ 2 * 2 + 2 * 2 + 2 * 2 + 2 * 2 + 1 + Assumed: a + Assumed: b + Assumed: c + Assumed: d + Imported 'if_then_else' +a * c + a * d + b * c + b * d +trans (Nat::distributel a b (c + d)) + (trans (congr (congr2 Nat::add (Nat::distributer a c d)) (Nat::distributer b c d)) + (Nat::add_assoc (a * c + a * d) (b * c) (b * d))) + Proved: congr2_congr1 + Proved: congr2_congr2 + Proved: congr1_congr2 +⊤ +trans (congr (congr2 eq + (congr1 10 + (congr2 Nat::add (trans (congr2 (ite (a > 0) b) (Nat::add_zeror b)) (if_a_a (a > 0) b))))) + (congr1 10 (congr2 Nat::add (if_a_a (a > 0) b)))) + (eq_id (b + 10)) +let κ::1 := congr2 (λ x : ℕ → ℕ, eq (x 10)) + (congr2 Nat::add (trans (congr2 (ite (a > 0) b) (Nat::add_zeror b)) (if_a_a (a > 0) b))) +in trans (congr κ::1 (congr1 10 (congr2 Nat::add (if_a_a (a > 0) b)))) (eq_id (b + 10)) +a * a + a * b + b * a + b * b +⊤ → ⊥ refl (⊤ → ⊥) +⊤ → ⊤ refl (⊤ → ⊤) +⊥ → ⊥ refl (⊥ → ⊥) +⊥ refl ⊥