From 97ead50a3e98637262b7a0601d7dc45dc8008298 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 20 Jan 2014 15:38:00 -0800 Subject: [PATCH] feat(builtin/Nat): flip orientation of associativity axioms for + and * Signed-off-by: Leonardo de Moura --- examples/lean/even.lean | 2 +- src/builtin/Nat.lean | 82 ++++++++++++++++------------- src/builtin/obj/Nat.olean | Bin 22458 -> 22960 bytes src/library/arith/Nat_decls.cpp | 2 + src/library/arith/Nat_decls.h | 6 +++ tests/lean/simp3.lean.expected.out | 8 +-- tests/lean/simp8.lean | 10 ++++ tests/lean/simp8.lean.expected.out | 11 ++++ tests/lean/using.lean.expected.out | 2 +- 9 files changed, 79 insertions(+), 44 deletions(-) create mode 100644 tests/lean/simp8.lean create mode 100644 tests/lean/simp8.lean.expected.out diff --git a/examples/lean/even.lean b/examples/lean/even.lean index a6134a68aa..15081fa686 100644 --- a/examples/lean/even.lean +++ b/examples/lean/even.lean @@ -54,7 +54,7 @@ theorem OddPlusOne {a : Nat} (H : odd a) : even (a + 1) := obtain (w : Nat) (Hw : a = 2*w + 1), from H, exists_intro (w + 1) (calc a + 1 = 2*w + 1 + 1 : { Hw } - ... = 2*w + (1 + 1) : symm (add_assoc _ _ _) + ... = 2*w + (1 + 1) : add_assoc _ _ _ ... = 2*w + 2*1 : refl _ ... = 2*(w + 1) : symm (distributer _ _ _)) diff --git a/src/builtin/Nat.lean b/src/builtin/Nat.lean index f1c042d0cd..92c94d0395 100644 --- a/src/builtin/Nat.lean +++ b/src/builtin/Nat.lean @@ -83,15 +83,15 @@ theorem add_comm (a b : Nat) : a + b = b + a ... = (n + a) + 1 : { iH } ... = (n + 1) + a : symm (add_succl n a)) -theorem add_assoc (a b c : Nat) : a + (b + c) = (a + b) + c -:= induction_on a +theorem add_assoc (a b c : Nat) : (a + b) + c = a + (b + c) +:= symm (induction_on a (calc 0 + (b + c) = b + c : add_zerol (b + c) ... = (0 + b) + c : { symm (add_zerol b) }) (λ (n : Nat) (iH : n + (b + c) = (n + b) + c), calc (n + 1) + (b + c) = (n + (b + c)) + 1 : add_succl n (b + c) ... = ((n + b) + c) + 1 : { iH } ... = ((n + b) + 1) + c : symm (add_succl (n + b) c) - ... = ((n + 1) + b) + c : { have (n + b) + 1 = (n + 1) + b : symm (add_succl n b) }) + ... = ((n + 1) + b) + c : { have (n + b) + 1 = (n + 1) + b : symm (add_succl n b) })) theorem mul_zerol (a : Nat) : 0 * a = 0 := induction_on a @@ -109,12 +109,12 @@ theorem mul_succl (a b : Nat) : (a + 1) * b = a * b + b (λ (n : Nat) (iH : (a + 1) * n = a * n + n), calc (a + 1) * (n + 1) = (a + 1) * n + (a + 1) : mul_succr (a + 1) n ... = a * n + n + (a + 1) : { iH } - ... = a * n + n + a + 1 : add_assoc (a * n + n) a 1 - ... = a * n + (n + a) + 1 : { have a * n + n + a = a * n + (n + a) : symm (add_assoc (a * n) n a) } + ... = a * n + n + a + 1 : symm (add_assoc (a * n + n) a 1) + ... = a * n + (n + a) + 1 : { have a * n + n + a = a * n + (n + a) : add_assoc (a * n) n a } ... = a * n + (a + n) + 1 : { add_comm n a } - ... = a * n + a + n + 1 : { add_assoc (a * n) a n } + ... = a * n + a + n + 1 : { symm (add_assoc (a * n) a n) } ... = a * (n + 1) + n + 1 : { symm (mul_succr a n) } - ... = a * (n + 1) + (n + 1) : symm (add_assoc (a * (n + 1)) n 1)) + ... = a * (n + 1) + (n + 1) : add_assoc (a * (n + 1)) n 1) theorem mul_onel (a : Nat) : 1 * a = a := induction_on a @@ -148,12 +148,12 @@ theorem distributer (a b c : Nat) : a * (b + c) = a * b + a * c (λ (n : Nat) (iH : n * (b + c) = n * b + n * c), calc (n + 1) * (b + c) = n * (b + c) + (b + c) : mul_succl n (b + c) ... = n * b + n * c + (b + c) : { iH } - ... = n * b + n * c + b + c : add_assoc (n * b + n * c) b c - ... = n * b + (n * c + b) + c : { symm (add_assoc (n * b) (n * c) b) } + ... = n * b + n * c + b + c : symm (add_assoc (n * b + n * c) b c) + ... = n * b + (n * c + b) + c : { add_assoc (n * b) (n * c) b } ... = n * b + (b + n * c) + c : { add_comm (n * c) b } - ... = n * b + b + n * c + c : { add_assoc (n * b) b (n * c) } + ... = n * b + b + n * c + c : { symm (add_assoc (n * b) b (n * c)) } ... = (n + 1) * b + n * c + c : { symm (mul_succl n b) } - ... = (n + 1) * b + (n * c + c) : symm (add_assoc ((n + 1) * b) (n * c) c) + ... = (n + 1) * b + (n * c + c) : add_assoc ((n + 1) * b) (n * c) c ... = (n + 1) * b + (n + 1) * c : { symm (mul_succl n c) }) theorem distributel (a b c : Nat) : (a + b) * c = a * c + b * c @@ -162,8 +162,8 @@ theorem distributel (a b c : Nat) : (a + b) * c = a * c + b * c ... = a * c + c * b : { mul_comm c a } ... = a * c + b * c : { mul_comm c b } -theorem mul_assoc (a b c : Nat) : a * (b * c) = a * b * c -:= induction_on a +theorem mul_assoc (a b c : Nat) : (a * b) * c = a * (b * c) +:= symm (induction_on a (calc 0 * (b * c) = 0 : mul_zerol (b * c) ... = 0 * c : symm (mul_zerol c) ... = (0 * b) * c : { symm (mul_zerol b) }) @@ -171,7 +171,13 @@ theorem mul_assoc (a b c : Nat) : a * (b * c) = a * b * c calc (n + 1) * (b * c) = n * (b * c) + (b * c) : mul_succl n (b * c) ... = n * b * c + (b * c) : { iH } ... = (n * b + b) * c : symm (distributel (n * b) b c) - ... = (n + 1) * b * c : { symm (mul_succl n b) }) + ... = (n + 1) * b * c : { symm (mul_succl n b) })) + +theorem add_left_comm (a b c : Nat) : a + (b + c) = b + (a + c) +:= left_comm add_comm add_assoc a b c + +theorem mul_left_comm (a b c : Nat) : a * (b * c) = b * (a * c) +:= left_comm mul_comm mul_assoc a b c theorem add_injr {a b c : Nat} : a + b = a + c → b = c := induction_on a @@ -181,13 +187,13 @@ theorem add_injr {a b c : Nat} : a + b = a + c → b = c ... = c : add_zerol c) (λ (n : Nat) (iH : n + b = n + c → b = c) (H : n + 1 + b = n + 1 + c), let L1 : n + b + 1 = n + c + 1 - := (calc n + b + 1 = n + (b + 1) : symm (add_assoc n b 1) + := (calc n + b + 1 = n + (b + 1) : add_assoc n b 1 ... = n + (1 + b) : { add_comm b 1 } - ... = n + 1 + b : add_assoc n 1 b + ... = n + 1 + b : symm (add_assoc n 1 b) ... = n + 1 + c : H - ... = n + (1 + c) : symm (add_assoc n 1 c) + ... = n + (1 + c) : add_assoc n 1 c ... = n + (c + 1) : { add_comm 1 c } - ... = n + c + 1 : add_assoc n c 1), + ... = n + c + 1 : symm (add_assoc n c 1)), L2 : n + b = n + c := succ_inj L1 in iH L2) @@ -202,9 +208,9 @@ theorem add_eqz {a b : Nat} (H : a + b = 0) : a = 0 (λ (n : Nat) (H1 : a = n + 1), absurd_elim (a = 0) H (calc a + b = n + 1 + b : { H1 } - ... = n + (1 + b) : symm (add_assoc n 1 b) + ... = n + (1 + b) : add_assoc n 1 b ... = n + (b + 1) : { add_comm 1 b } - ... = n + b + 1 : add_assoc n b 1 + ... = n + b + 1 : symm (add_assoc n b 1) ... ≠ 0 : succ_nz (n + b))) theorem le_intro {a b c : Nat} (H : a + c = b) : a ≤ b @@ -221,22 +227,22 @@ theorem le_zero (a : Nat) : 0 ≤ a := le_intro (add_zerol a) theorem le_trans {a b c : Nat} (H1 : a ≤ b) (H2 : b ≤ c) : a ≤ c := obtain (w1 : Nat) (Hw1 : a + w1 = b), from (le_elim H1), obtain (w2 : Nat) (Hw2 : b + w2 = c), from (le_elim H2), - le_intro (calc a + (w1 + w2) = a + w1 + w2 : add_assoc a w1 w2 + le_intro (calc a + (w1 + w2) = a + w1 + w2 : symm (add_assoc a w1 w2) ... = b + w2 : { Hw1 } ... = c : Hw2) theorem le_add {a b : Nat} (H : a ≤ b) (c : Nat) : a + c ≤ b + c := obtain (w : Nat) (Hw : a + w = b), from (le_elim H), - le_intro (calc a + c + w = a + (c + w) : symm (add_assoc a c w) + le_intro (calc a + c + w = a + (c + w) : add_assoc a c w ... = a + (w + c) : { add_comm c w } - ... = a + w + c : add_assoc a w c + ... = a + w + c : symm (add_assoc a w c) ... = b + c : { Hw }) theorem le_antisym {a b : Nat} (H1 : a ≤ b) (H2 : b ≤ a) : a = b := obtain (w1 : Nat) (Hw1 : a + w1 = b), from (le_elim H1), obtain (w2 : Nat) (Hw2 : b + w2 = a), from (le_elim H2), let L1 : w1 + w2 = 0 - := add_injr (calc a + (w1 + w2) = a + w1 + w2 : { add_assoc a w1 w2 } + := add_injr (calc a + (w1 + w2) = a + w1 + w2 : { symm (add_assoc a w1 w2) } ... = b + w2 : { Hw1 } ... = a : Hw2 ... = a + 0 : symm (add_zeror a)), @@ -249,9 +255,9 @@ theorem not_lt_0 (a : Nat) : ¬ a < 0 := not_intro (λ H : a + 1 ≤ 0, obtain (w : Nat) (Hw1 : a + 1 + w = 0), from (le_elim H), absurd - (calc a + w + 1 = a + (w + 1) : symm (add_assoc _ _ _) + (calc a + w + 1 = a + (w + 1) : add_assoc _ _ _ ... = a + (1 + w) : { add_comm _ _ } - ... = a + 1 + w : add_assoc _ _ _ + ... = a + 1 + w : symm (add_assoc _ _ _) ... = 0 : Hw1) (succ_nz (a + w))) @@ -263,7 +269,7 @@ theorem lt_elim {a b : Nat} (H : a < b) : ∃ x, a + 1 + x = b theorem lt_le {a b : Nat} (H : a < b) : a ≤ b := obtain (w : Nat) (Hw : a + 1 + w = b), from (le_elim H), - le_intro (calc a + (1 + w) = a + 1 + w : add_assoc _ _ _ + le_intro (calc a + (1 + w) = a + 1 + w : symm (add_assoc _ _ _) ... = b : Hw) theorem lt_ne {a b : Nat} (H : a < b) : a ≠ b @@ -271,7 +277,7 @@ theorem lt_ne {a b : Nat} (H : a < b) : a ≠ b obtain (w : Nat) (Hw : a + 1 + w = b), from (lt_elim H), absurd (calc w + 1 = 1 + w : add_comm _ _ ... = 0 : - add_injr (calc b + (1 + w) = b + 1 + w : add_assoc b 1 w + add_injr (calc b + (1 + w) = b + 1 + w : symm (add_assoc b 1 w) ... = a + 1 + w : { symm H1 } ... = b : Hw ... = b + 0 : symm (add_zeror b))) @@ -284,40 +290,40 @@ theorem lt_nrefl (a : Nat) : ¬ a < a theorem lt_trans {a b c : Nat} (H1 : a < b) (H2 : b < c) : a < c := obtain (w1 : Nat) (Hw1 : a + 1 + w1 = b), from (lt_elim H1), obtain (w2 : Nat) (Hw2 : b + 1 + w2 = c), from (lt_elim H2), - lt_intro (calc a + 1 + (w1 + 1 + w2) = a + 1 + (w1 + (1 + w2)) : { symm (add_assoc w1 1 w2) } - ... = (a + 1 + w1) + (1 + w2) : add_assoc _ _ _ + lt_intro (calc a + 1 + (w1 + 1 + w2) = a + 1 + (w1 + (1 + w2)) : { add_assoc w1 1 w2 } + ... = (a + 1 + w1) + (1 + w2) : symm (add_assoc _ _ _) ... = b + (1 + w2) : { Hw1 } - ... = b + 1 + w2 : add_assoc _ _ _ + ... = b + 1 + w2 : symm (add_assoc _ _ _) ... = c : Hw2) theorem lt_le_trans {a b c : Nat} (H1 : a < b) (H2 : b ≤ c) : a < c := obtain (w1 : Nat) (Hw1 : a + 1 + w1 = b), from (lt_elim H1), obtain (w2 : Nat) (Hw2 : b + w2 = c), from (le_elim H2), - lt_intro (calc a + 1 + (w1 + w2) = a + 1 + w1 + w2 : add_assoc _ _ _ + lt_intro (calc a + 1 + (w1 + w2) = a + 1 + w1 + w2 : symm (add_assoc _ _ _) ... = b + w2 : { Hw1 } ... = c : Hw2) theorem le_lt_trans {a b c : Nat} (H1 : a ≤ b) (H2 : b < c) : a < c := obtain (w1 : Nat) (Hw1 : a + w1 = b), from (le_elim H1), obtain (w2 : Nat) (Hw2 : b + 1 + w2 = c), from (lt_elim H2), - lt_intro (calc a + 1 + (w1 + w2) = a + 1 + w1 + w2 : add_assoc _ _ _ - ... = a + (1 + w1) + w2 : { symm (add_assoc a 1 w1) } + lt_intro (calc a + 1 + (w1 + w2) = a + 1 + w1 + w2 : symm (add_assoc _ _ _) + ... = a + (1 + w1) + w2 : { add_assoc a 1 w1 } ... = a + (w1 + 1) + w2 : { add_comm 1 w1 } - ... = a + w1 + 1 + w2 : { add_assoc a w1 1 } + ... = a + w1 + 1 + w2 : { symm (add_assoc a w1 1) } ... = b + 1 + w2 : { Hw1 } ... = c : Hw2) theorem ne_lt_succ {a b : Nat} (H1 : a ≠ b) (H2 : a < b + 1) : a < b := obtain (w : Nat) (Hw : a + 1 + w = b + 1), from (lt_elim H2), - let L : a + w = b := add_injl (calc a + w + 1 = a + (w + 1) : symm (add_assoc _ _ _) + let L : a + w = b := add_injl (calc a + w + 1 = a + (w + 1) : add_assoc _ _ _ ... = a + (1 + w) : { add_comm _ _ } - ... = a + 1 + w : add_assoc _ _ _ + ... = a + 1 + w : symm (add_assoc _ _ _) ... = b + 1 : Hw) in discriminate (λ Hz : w = 0, absurd_elim (a < b) (calc a = a + 0 : symm (add_zeror _) ... = a + w : { symm Hz } ... = b : L) H1) - (λ (p : Nat) (Hp : w = p + 1), lt_intro (calc a + 1 + p = a + (1 + p) : symm (add_assoc _ _ _) + (λ (p : Nat) (Hp : w = p + 1), lt_intro (calc a + 1 + p = a + (1 + p) : add_assoc _ _ _ ... = a + (p + 1) : { add_comm _ _ } ... = a + w : { symm Hp } ... = b : L)) diff --git a/src/builtin/obj/Nat.olean b/src/builtin/obj/Nat.olean index d8d5b4879a2bb3ae4f14f151e345f29a361eaca9..79f555851ebe20febc8c6508cd5ad3c8306bdc58 100644 GIT binary patch literal 22960 zcmb7M4UApIb-pwA-u3PxVMDO_DU|Kniy>~nSe6>hPYCfNb|7Ad@RzjGX6=2(FRb6% zyK8W8DRk>rp#dC7a7ZALaDO1AG?gl)2|vLy>z_b=DA3R-D!8bGV1kG$rELGVy zSQ7(`U6xq+_x-4(CDbk3Mkd3lk$)D}b7pyI#5NZ-c&(`lck~ zlCG;KU3M4)64PZjD3IDq#>Pg42C6+M48dN4OHk%upNyIEL>Co2P%zyQgRk87cb@Cx~D4=(I zK(8_4MTW5|n-dA5D6wVjpCVq24;)i^UGz zR39H3_Y(x;Bi=}=r!*F83&uL;Dv8jpPE(?uG+TA;j_!DD<i7H$>E}a{7leBV#O{t4UbOLhw7t^Err?4VPXyzs)ed^s2YDG6%#QS z*fUc*HeSpUEu|kL?P7^Vveof#TPOgua5HKX0kNo-8j$7-iMlKTf7^tS`nKf?pV2b@ zp+<9Ze2k5Snr9y#3GH;MBL-`O|sMBk0fpp z<|aP1rC^&)Tue*CYnt`tvFcP{OWmqecO==-Tm}QN0{dnZt8;rJ{zXh!qtIv0K>a3d zMA=D7V6+QJT;YN<0sa{Zu4Mtb^G*`-a^kW`r4SaVOrZ$&CR!8wds=RGF)+NFjWi}U zjyJY6BrQU&aR~?{T`uG>XgSa8Lnk>^&qK98j$?(F_Mwxw-d^f;7qC@1fbK@&WO{6@ljo@y^Nd;bv=pi^wd{deq7- zgSNClCCQLpBr1_19|YIE!BX195D}-1v>7s}9754k5;4+*K*XK17rFpt{fFe|deBpA zqk!7Q-o`6Nd=5pA=bGD`dKT9{js8HzoR<1%lcw&yz?T?|fBpbP5(fjKy;Lnj;FBXw z%cf9QBaMvqCG_-CQ%4B4??OMWetW{&<6hNF)F9=mi06C z9|o%SaJ&zYZ=vUnYMI2OcLH~2yZSl0dm{R8pz+Pw>HD<~VuYWC0*RIKvu+^O;~iNi zixl=IP~Y%k@UkxZz{WAz1%oiX0pm)s0rh2`QM!P-!WjL}a*LmEAOH zp-@u;MDKq!S{NI9)!;V*OX5SE5t;eaho||bPVA?rsZb_`)qxOAtribO4@7Jhp-3W4 zA4TKBYE4U5@+%avBB`;S^1{rCf@l_LNc<#5CCX$eWDQSDjBTvYSJ#Xu3%_Pcn>2&? z!^UOge>>*Xh<1YqxwENecd->n5Q16C1%w;T01*061Q84dW6p4Fm}AjTHu?imyMEmW zmH{cSI%>TK@y8s;u1F1}cW_2Ekbl$5Nv1HKK@O9ccePv3IhA}BK@6j7DEb}Cw2ZJ0 zRVLx;q-s_vz8|%aSSaA_=KNq*)MI?g%<$Yq{EI-zFdxF|&3R>!80`J#!fKI3tOUF# z3`AUDRSYs03)LhxU7THv=f~*EB7W#TC(h1~6Oe{O@rS2K{BH0Thevf= zI@jsw_u;Q~%Mhdh1HkA*p$41*v?w^ECHLGA+GCv{nNJY4oey&EiIF0U{T$G4f}f!9 zrqLU7!YH*5JvKlB;wDa$Mw8JsIN3f8E*w>vZ<*^zc2*tvmGpA}ilv-(3Lu=zYz9QB z?ROCj5}#|*#W}dvAX=>?QSx^SK#f+n5}Y*}kz$yCkz=-U8Dv(AK(HQ(%vfJn!Lpu$ z7p^_l$)AHa%WmDX$Y!#D|Lj61rKMvT-`E%(8q8lP1>hec*lsenR5Cq7{*{4J4Fy-l zrTCrD+`*oJpw!Lny41GP(;^vCRe~6`yAu^4+=aQ0qJWp1&(8&4BMkBPbi!9&L6)<4 z{y6mB>Y+gYq7+OW&3)BKq|BB3)Dw`oA3dhg8lUuXyh}aJm(l&jxw)86J$Jg5s84B~ zRzv&w3g(N$@_m@<{s9=Lrop-_Do8UV&(@cK`-NHA(%=$=m_ZQlcLl2uZk+R&`?}HE z7M*q80qHUip@{SpCDy9I?0n#^g^9Up1-J+C-;`n`M78=O42QEff$O^ayPkQ`()@0 z?*4AZ!!XxKkrzixvf^7Yi@BLg;Xb6AC4&kwd+exWPZ5g^&b=1)XpfPibTah#7F|4& zZe}BMN*cgW;9P=ZR{(RL{BJf_^^nj$*(YXC*5vAq&KR}DzXw3CY}u64L57vAhgfw_KGrrHu?FeuN8P-ZAtr)~yO z1!UH<+p~J5XDCog#1Mwt%V%c@Xd_NGwl4MJaz`6|*9f{8o1-fg`w<|SC#5J1B;p0x zwf)dL<%Mi0Lp9Kk#jvg%9PEcM%ZCSm`Vc_Krf`#pAG+O1v-1P`WOso| zaFU@@#@iXE?Q`yf*DOZsnmzP?DdyICT+us$^t%vVRET+J5zgKYlhzI|XU|UR* zw~LYiboH@c3O^FFT=XhdsK@OaqC!q~4xJ^ucNYy>=b-(o*E#%W^ufl0@Wc+ z3Y7Mhms&zn(j7UZ;6f(uMt!~)2NoG8Y3W($XD+SLbAH(%QdHacbIVJ5 zBF@=U}2ku|2LgW!2mq}O^GdtYQKrpBQ(S`zpMhQt!6 zZwo#r2x4a(BlPOW3JG~N7v4N03UtTAyZyRdXhr*W%g#$h4^Vp}E>onMc#hT(K1$7Dz zLCY+PLP3N?H%Yg|NEnG6Ep3*)O5Jq<1=t}TFbH5V_GB7_^D13-;J;+_9s4ghBV+m& zl_Q@v(Q{GRQ~B0Ix&@-vXvaBgQf<8~cnV;%uw`eDNiBQ@Rlar5*S0(46@{ZE7jnIn z4`p>45^59{B7veSXZTLKeM9%l!%Lxvk>?247##@>UBL(J5Kke7v#X5?+ z^kldUL)G>By8+f2=S& z6{70>j@clMoANBB!OU^?XQTmh)W=#KCH#EpTI3MBJ%#9jF`Kmv`^wD=P&7GjfX>MHGvTpgbK&8VodipR#Pbc8;qi2FLHLd4#tSWs9jYoBrz@LXYY%aMo zz?W(|tw>HFIn;zyM@XU}DqLZ>uV-5lH02ew#!1eq&1u(NU$FgTi2xvxw zNj2wnKK;D3#6B%Y5^u(V!L7mYWR*J!k~$bu7uJ*COTbYVe%XUZ0IuR9{*$eN&ZV9r z|X*Q%t;(l`V)3(-L>jaYE;Kl_|rgT zD15DqnO-X$>Fb@5cs5IqVllei&>nR$9O-ncnAcJ)Gw2qaz(6%!`Zn2_LL=FG19i=m zls+T*F4zCMKy94pYRjCYKgF2APMmm2&|x?q)D+)Xr{0}c!!}( zjPD#kS04%}Ld_@$L5x1CcbO>;LD?}?$5Vap%hI@!d8P+I`6!Ao(Q|t6{po?IF~pbQ zS@9YNNKttZXL^7pFpWm6p@kHYs-YkF+3{tQ$rhkd)iJa2YG9*VMpwC6^x9tr#bgU0 zSPh9>zD^&_{4T*s?#xlnFtc9-L%41Rf*yxNPFjS-vhQTa33_^9F(x@eP!DwguOGnf zkRVMgb~k!MbQhaG6J)$KX6FBr6 z99Y&BzkEpEs_b!64X;Ax1C>&LtBTT_(wnUZv${{z9D4N95AU?Hj?o!IY2~;xO7A2) zQ)py(;wK-$i8{J&;hNew@!T^vO}T9y^$BlFbDeY3Sg=%-etbZy;G#7_{a^B%qx?S) zGInTu|CO|6bq2_XfiQ`p9|eW%lA8aKmU2=v+3BF-O;pLSKJ%HytD5sO=h6kd4OW!Z z-+1u10%lvGX0=J)>XjM(wRDEgB#tD%bWtT(^@*(@#!TH%zns(1OBFvg@p>1Hd4xN1+)jn6lu78RU=HteMUwp`F=ND@k0TuPf5RK8@E>NGi02~jNVbn z@S<@t=ypH_H6*ou(8F{IN^C{tqkiR<#LtEGODrD!Xd&6xTl>$~D|JWzjlZGlr9qI7 zLcZ$eVa%M{d7i>zd{onJ9qqG6eUAzYHmeU!)aZ|gpcG`9q##ITj}mtw!MR(#s*_f) zJ`XDD^Su1dnC6n18hWbE_}Tus&zI~570wr&@!7}(Tj%qW%FS$hf_+GDZmq7@vN%|xHegJaMI{x%<lWgG^-A0e@dw3kN)1z|!3sx}HKYjpBgVvmS!|9a+hLFnk{{zXNE0h54tv z;>w_LJ%7>oE3ddzk4J%dP>T3oD|_493iQfdBfiYaknCh{JK1~Nh(FbsgKdD+OPC3P zukE)j0*Ghk)f=qAfxds`mJ>$>Jvi z1jtW{B2*>5K6OQy%uk8&rIDtR!$q>+vD@VqG>sg7#NS!VQ)fbB<9q){CWGiOeAQc=?wigQiQ*M{|3Kav*R z?e}y>;wd1%!r4J^O&!_69Ipnr0YDCEbcLLM6g=^ik?ayslXE2hZPQZ(s#aKSs$W=B zuOyGv$#XorhEEccZA5Bd4gSod+p=CyU}RA*OM{IWv)3rq(w^gFAiJ{x4s^4WuKh@g|fLE@X&d`rX& zJ>=A~P+}z7QQmYW5=2Sm!AXUf$!w488L6_Dg}pouf@5G$Z;#XlBB_Jj&d&~{Un3z* zu#JAR90c{0NuoRjw0_LaoGpXH^PPP5G}gRM?hmVe7Er=eQ}Bgx#H%j5#a93=T#T}Y zLVwAJ@vqm#Hgv3pA(>SG`Qv=%e1Y=2+%I-^TjfB$yTV=OaB~ExGH!<12GOY>vxjd8 zL%KQ7w`*q@NY7Hw>jsTF<8yuw*FeVQR|m@r%vOWyo^HEQUPJ=;K;FU-57i$Z%~q?6 zf`Np7%sDJaqOC{2t9uJ@(kry&l{zms^&p)d2t9b=rHQv0`3rYMB8u}G#d*?6za%tVbTwhwTUjj{rX7)(8{3f7qEXesD-1G`>cwJ!>!=TAAcN)Z?|VZHZL%me-p*+q_Wym0jK%5P<#oE?vQbwRE!ziI-F!^pNB`} nK~=sz2&-~;8+0~GsPgN>L7zBcP?MkS4Qd!yYmQusUuph-?R`;i literal 22458 zcmb7M50G6|dB5k}`!>64WyAm0%CNq$kP(3-WTujTg~)Rfge+hxZO6&ZX7?pL*z6{| zFA)Azbd57XkYFevP!v!=62*u*owi~zjYz4rRV!_^r5P%nX##~>r~=yQ_xpYKopbJa zci(Py;N&~!`_6a1^Zh%2?!9kftUf%xsWDbh@;}qqvUOsznOt3;9IuZh*9=c4cHM9@ znP(EaaiWdnNA3+19DZ(((4cyu&bH_;q!HYUc= z!PqksEB{`AN?IV@vVANfeK$$p57MkaDgqaou2`8Ep;`jcN)h$K&0h#`qxDTm#wl&C zCtY?J9TL-JH!6_Y)e{qA!UNSF6oz0g!P8JyAU*{%#er7kGEgzyk$^AU{IHke7)k*) z^TwL^C+V)VM5(ky(ZN`fV=vXanB+ahkyj{dk{y$H=9@b+KLNZr$=)KrRRO=_0)CBA zuQK#i-JDDiML{fUZ%pLBdD8wnlpi!D)Q;D;0ViDjoGDx% z8f~#}WBe-L*;%j4u1N+=&IkUG%tvv`0Lp$82F9ZSd)IE+ik9RQv>4;~i^mRKU!Re4!ddwk>XG*Pj>c4T3c|vL?1%!T`l$jJ4cQnU-9Ey6(q%7Y z-+5yA#mNFkYo)$KWMalabT`&0R@p6pdgzk#o!snPBZrn_Ak>U$UYYx>8+J%CSunCo zAuSQ8yfP8MeJuy4I_LW_t5nc=AecvR89)uM?**Bk%GSyHXd(Qdh5>YYCkjT6`Vp;13B*tvflLeu`w5~z{3JSo3ji9G@4cEs zf0s=tMp5)s5TbzmNU%m?#VSK*9x!cTPV0IR+xv48KHU36R24XU>3sXBW znU4}prHY<*f#f1t>iD-UQ~+AI7`3T@R5VKsM18`dE|b9DHW8%0ZIQyKx14{dG2Wb< zU}J9P*%;HlnhIqGQ`ep){%1&B> zpj{y14CgNd_z@JG%Y2|Koiyb2#A%UBt}JkwMiHz{^d{naT48oRD14ZWHl{`<8(SK( zEy7-7H5epaF6A(3xyb7Wl9FoVp<0deSRSSQK$4b{G6DzDrXKM70J}KVKLDtCPowjn4>%zY3CT8NQo+Rb z(ylu}t;PYg2Zht+6;hF9*`?psvOMP3ngMj^M-iCCqD~d|Q~-{mFdT0a8+=B35~!YT zd*$#ol6H1%oh;-w?+#?CMQWRqjcXdidEk^Jo+l+bo0G%it@SNpGhgdbE0+xV(tOn< zQ+mEpi5&T9NZlJurA-YHbNWb|BZJF#QS=m4jBP@o;?BDlh5&W_9?Eky_^G#1LG5a9 zlNCMgK+)r+<}#;|#kn5@J}@zdr9IlTscSFjB?sf5ccDn)WI(d#%XJ8PN~GJeY1Gw8 zBd2{Hm|j}y5W)6U=%=OfGjSJ0_j9k26ACJzPcac*Q%}Gf^#2)?av1MfFA@I?NEO5W zK0&?$%#m`P#H?=s?aY4lD$qR<|08I8d3OGOu7l{|N1;MuqrB7&qI$d{>tK<=UIytA zuLiH{VhoH-$SN45>5b@D$PK8U=>=s7Xh?1)DQC&7+A#z`yCP!4`Ks;?k{1efH9(C1 z7o&->u~!{_1XPkA;vJFcqdh#&mvvx2JY9u4$-NGY=xVjND=<*8ISEA)S^6*CkvrDNmJrg=#{9Dg_JcsH8n9(Vy~{*PZqfiy$+~-j-ji^c8sYR z?HUhqW$S2J&k??1&Tw^e4A^jlYM@nz*PMSQhyn+rfqRf@%&|m88YjP}XVkdCnr(VH z$Ta#hpJ5Ple7mEZQz}=Uuh5%5QgtHJ36h`=t0m#=q-vHaz3+7*sZb!W&GKMW)MI+; z%d$xb?y8&3Q$Y7%cN74mXAS<*d`xkqZH<2x;#hPGV4zpw0MsFZ?Jo0?QlV$qYGvS5L%~^bDt^&3Jk#i&@gRsO<1ISXw$k$= z8*){K=y_Wp7U~5qXt-U9L(Wtu+$`ZIK4Waz@KO2zf8{VwwcMWF*dRO>$4?k8pd zeyE#UodIp3`yMaBJwjvdnpFbLBSAJ91an3T3s#}Wcqe1-?M7=`BGz#u$G=M`%{>Ds zA4L(_DcVD;-4D+$J6P>SafuX3e25@Q6{#q%$h$R1PM}-9*NP1I$AU0><}O0=23VCU z>dt81HBiP5^J!@_x6VGE^AMdK%|k;4am~F~JmotglOXubr@>C$Sfz@Hb_0Ezm!BC! zqrQ;tC-4-_9VI}Y^rHw?HL6DQE@!!uc#apQb9CY{pr_rvIQI43m@hujkq{ry#*=fs8O#>GLJR- zD^9rJp>sRzE2T#HWW8H?B*K@kZ(fqi752Yh)a6> z!<*rf!>)}EyXIC79AtA^p#~nhkLJ{9u;{SM&457`vfRS|fTs4#2{N{w`LJuA)sZn0 zH8;rmH0s<|fOCAJu-LELlR#;H4ZKS0>?Rk>at*n0dov6McU3pzxtDXK%ENQ7Z^bC) zMg|R~Qp@sMRzdC_I~tjjBS%a&IQLrQUdwreCqqwf1)uOpx|xlzuR6enAh^I}F({vs z|IOwy3>iIzy`nu<3i3=26s^YWXu|YbbX2mB_w;PE$Cq*1K&7>9XdvU&el}M@9O`BK zbbvci&x)lx^Eigm2dO`x=TyYgD1K?XmMJPyIxw}6_l4r z!D|Tn!Ez#U&V_6l_*2NC0y38p?WOu)F#s$m?d4v| zz$lTF>p=N|*`);8MyDIS3RHQt(W5pBspjVBO2txY^DVGi4I*6{yv8mDX6@0+!aF7v zs8lzX6xEPNM5G2r*wI`kSx%FB9^qUfHBbY&R781WU4&_#8d>Z@G_LWYa>=5WG@E!W zy$_TfpG|YT3{r80QD0)>2}K2)-5}B%5ij3`k!aAWeIJ&3GU1YCGIjy*{}c*_c!QiSJ6dW%qh{#`x~;i(E|aq0i4<&2-v3s z|8o-RK~OV30xsWQU`E_1hjrwJ_rwjfXt= zd4imG=yCGyN-_XcKk-uV*_Y`pHs*T~&{R3d!x8>zpuSmj1`S|hG_xH95v-t?X8}E3 zG)2P3Dgs9zqE$h}?f7wR*U9!RdF3S*Ki^!Vn{J!C?Zt}=H<*Gk>(ouWvv8amdc~*G zoD?V$H3dk!ic@XzBavs?hdP+1-80j3H6>A`rI4vEx#0A+nK@}dV8zlaCPYR08y)CD ziTm61n4%R@2yWKF#@vtU#2IAKy@z&xdqpTaz0;#3p0;53n}s3)9JIm zzDN`*mhwc8`BJQD>D$W4qkUn@kZjH>IrzOD#R;_Qw1D*Cl!;koq&T%`&>ATF#QT;M zyw7_F3HC(wLCr#ZWSYKPIHY{cOkvlyUSWFx?IwEfN>WG1tr9|A{>)Oy>Em4upjSm- zB0&Y^mp%Bn2freqS*q`jK7eNR49+C--n8Op2BVPDoKf_~6l3w=mFlC}Z?z}`zfc`3 zkCq1Z30<28>f3^s)q~s_=Lo%Ruo!9^C;L@^nlhj8;MW99*XU%gK(oGrSCyo**jK|_ z0BIiprXK|p9W`@`ytFyIaccYIXz3fRJR&AG>PhdWj8%DAt-ft&ygn4ZvW5{>qrf4f z?UA0}uj!@+Nz0s6RDO6WW!S*U(&)gfV_z4!TN zAPy6d=!LHpm#Iayp|6VM6KTB^A4~%rPrz`hrl$aENPgRc2LLXEkm;1yZWXQc;GJkp zccAVX{oAU4Db0~F`Fgbz+OyQ@(n{X}xBPv1%sW3!k%G5@$ssnneVph5pQiXHN}jDH zCE0!#AP+0)?En=8D0qd)KUWc^8vRb#QpaOrN_X*#C5Xr5rc4#XL0xW5vHYg{DpJn0t@5HcUF#Bi z3^CK_${2neP!)v>-)E!}hcCVXEc2~3=$R~Y&nw6sf@!p_po}=l$ZonMK98Qp@$ z)Bb_QG1T{5e^REa(D?n%L_CJ2f5-f}6Jt>Ke@}Lpp{`~eSZ7Ff&fwa86?N5NF@=Nb zcIgY0aa!v6NT};hN%=>E>THXHrikri4wuOwV{DK$%oN`hr{4#SbFd#uCCaqJ!%+47l7(z|0+;=q{PeYo4`CtON*6*aS;YGPwpMi+(Y>jT0-vma-w zBSnM!62srtX%H_j6SJmxaE`Mdg`nHUJI((U@^s$<40VX09@PL|rfb%If%7#>IYheK z@1-CqOrJhB3y~F~EIMyzedxL0%d)?y5ZxSfe4htw886lel^rK-@zFZ#E2b!QV)WL< zbg;Ga{by+jLs-7H8yag4E%E_OaVI$(H*Q>qEUoq;_!;?p4ZZTO=txK`54RR~H}aRg zXD$JlKpc^WUmx<2rAx+qHlvVpSg>R;p=4*t7t4C^O4uie-6QN+v=!f$PhKg-IIZTd zA|Mv^mW5h>rHs?dLXs_w^o_>k$bb~OB-BtRkN9c@bIZ=9#%2yR-BRItC~Z>4Y4F41 zlknSt;P4z=qHs_+osP^MXF7`dVZV)SS*~nXFalaV>R>8?VreK{ap@HtO1GUau@5Ii zEodtLFW(B)XKR@YZ%1nrMHK}VJUSvoq1Uz}?3z2=qY)udx>g=qDJ>iKeXyCObznKJ3(a zADT^pUA8!2iY|!N_!5SV*}23>ku9eMu*frLb4*|X5HYa)vsDf6Xl2hv+&og|c-m&L zgi|&Op4XwM6YVyf%DCf_BE6J-aIehNt#y}Zve78TVI5TdG-kB$W;~t`E&$OX6a+Q< zxZittOWI>EDxTHZKVE(KJ&JX44_kGPBVS1d~ zft?EblXy_%C=uPz2Iyuwea zRLyqODNGGe*&#i9c<$pRyTOIy1&4Gta@(A7yue*bw$0gIy@BO|ts6@oMZy(V!$C_K zP^tPb_A4=JA6ki`J)^^W7HsK2$r#O^h$1T|a^q!R0aIv9>AzM^4?HNdr6|4;#p5f) z&>%Cc_HMj%ztHL=e(oBxKSg7--OlzGLz6>uhm);>!MOzq#V-n#eO+kgat$G5I)0G3 zsN^7Z&~Fb=UKeKBH>9WfUT`L0PYt(xH_CX3SNx;763gyyg`F;tpM|0gv$n?Cu@FQ- zrc?!wm&QES5W(rL!1sZA1jVB$z9_D%r&xcVRR|SyCpjLnq#$1+0LCm{M`e!#{}@p8 z^U~`mHQ8ZM@|jKS#?O1VfC;&H2NzG?;_*8tbFjFu%f1b!NN4eREBm(=#$5&&n6qfR zI!+RE%bw`FON#7swAeeqUTyQ+9(<<DZK#Kc*C6Y(1YbGXOI91 zv9d5oi)c+=LlJ%MpG~3>-kMzmUb^_#(8v>0@c@tJ%2{$H6SK)LEp=1C)m&S+XoP!U z?)I^kPnob|oi@gU8p`gL$%zMBIq^^Sj>v-R64c^`bV| znCdNE8HQJDJfcS5#_2^?$Jb0DIP;oyX3=`IwMls}{sbmMPnJ#oR#dp45=z%$f<8U# zR7#%{=z_?k2o~`zX~n+-q_QwV^cNKlqJxqDV1uX)}ui zs!X}xZtS)yfqa&O8_MDFQIJZ%8AclfQonT$-<*TCE4*=BJ3~hw{jIM7wGZb&!R7bo ziWAIWqsoqMJ0dR)0sMHSMIm9UKSP-<)VQU&8Qk=L%brrm^Wzl%{0v3XE4<|OH?KDh zD;*vLJ$N}~9B&@-x6Vk&Dcdf=nw6m8q13DrC|gJZrW0L2fLEyP{k+Oe-N4qlim0wG zEzHFlv7E19DR!JrS@QwO6bLOf!$vG*u5ZV zQFP%g{RdLN1#(b&3+G-pf2n8B^XNrv`$c*Y%6<<<1CDmStLvQZ%2T);^n U29)vxu0aj`YU88t$M5z2KbepqQvd(} diff --git a/src/library/arith/Nat_decls.cpp b/src/library/arith/Nat_decls.cpp index bce59a39f9..dc343031ff 100644 --- a/src/library/arith/Nat_decls.cpp +++ b/src/library/arith/Nat_decls.cpp @@ -34,6 +34,8 @@ MK_CONSTANT(Nat_mul_comm_fn, name({"Nat", "mul_comm"})); MK_CONSTANT(Nat_distributer_fn, name({"Nat", "distributer"})); MK_CONSTANT(Nat_distributel_fn, name({"Nat", "distributel"})); MK_CONSTANT(Nat_mul_assoc_fn, name({"Nat", "mul_assoc"})); +MK_CONSTANT(Nat_add_left_comm_fn, name({"Nat", "add_left_comm"})); +MK_CONSTANT(Nat_mul_left_comm_fn, name({"Nat", "mul_left_comm"})); MK_CONSTANT(Nat_add_injr_fn, name({"Nat", "add_injr"})); MK_CONSTANT(Nat_add_injl_fn, name({"Nat", "add_injl"})); MK_CONSTANT(Nat_add_eqz_fn, name({"Nat", "add_eqz"})); diff --git a/src/library/arith/Nat_decls.h b/src/library/arith/Nat_decls.h index d7ed8f6d90..1df8d744a2 100644 --- a/src/library/arith/Nat_decls.h +++ b/src/library/arith/Nat_decls.h @@ -92,6 +92,12 @@ inline expr mk_Nat_distributel_th(expr const & e1, expr const & e2, expr const & expr mk_Nat_mul_assoc_fn(); bool is_Nat_mul_assoc_fn(expr const & e); inline expr mk_Nat_mul_assoc_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_mul_assoc_fn(), e1, e2, e3}); } +expr mk_Nat_add_left_comm_fn(); +bool is_Nat_add_left_comm_fn(expr const & e); +inline expr mk_Nat_add_left_comm_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_add_left_comm_fn(), e1, e2, e3}); } +expr mk_Nat_mul_left_comm_fn(); +bool is_Nat_mul_left_comm_fn(expr const & e); +inline expr mk_Nat_mul_left_comm_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_mul_left_comm_fn(), e1, e2, e3}); } expr mk_Nat_add_injr_fn(); bool is_Nat_add_injr_fn(expr const & e); inline expr mk_Nat_add_injr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_Nat_add_injr_fn(), e1, e2, e3, e4}); } diff --git a/tests/lean/simp3.lean.expected.out b/tests/lean/simp3.lean.expected.out index bab4db32d8..2da8ef33db 100644 --- a/tests/lean/simp3.lean.expected.out +++ b/tests/lean/simp3.lean.expected.out @@ -6,16 +6,16 @@ 9 ⊥ 2 + 2 + (2 + 2) + 1 ≥ 3 -3 ≤ 2 * 2 + 2 * 2 + 2 * 2 + 2 * 2 + 1 +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 +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))) + (Nat::add_assoc (a * c) (a * d) (b * c + b * d))) Proved: congr2_congr1 Proved: congr2_congr2 Proved: congr1_congr2 @@ -28,7 +28,7 @@ trans (congr (congr2 eq let κ::1 := congr2 (λ x : ℕ, eq ((λ x : ℕ, x + 10) x)) (trans (congr2 (ite (a > 0) b) (Nat::add_zeror b)) (if_a_a (a > 0) b)) in trans (congr κ::1 (congr2 (λ x : ℕ, x + 10) (if_a_a (a > 0) b))) (eq_id (b + 10)) -a * a + a * b + b * a + b * b +a * a + (a * b + (b * a + b * b)) ⊤ → ⊥ refl (⊤ → ⊥) ⊤ → ⊤ refl (⊤ → ⊤) ⊥ → ⊥ refl (⊥ → ⊥) diff --git a/tests/lean/simp8.lean b/tests/lean/simp8.lean new file mode 100644 index 0000000000..6088279c7d --- /dev/null +++ b/tests/lean/simp8.lean @@ -0,0 +1,10 @@ +variables a b c d e f : Nat +rewrite_set simple +add_rewrite Nat::add_assoc Nat::add_comm Nat::add_left_comm Nat::distributer Nat::distributel : simple +(* +local t = parse_lean("f + (c + f + d) + (e * (a + c) + (d + a))") +local t2, pr = simplify(t, "simple") +print(t) +print("====>") +print(t2) +*) diff --git a/tests/lean/simp8.lean.expected.out b/tests/lean/simp8.lean.expected.out new file mode 100644 index 0000000000..f88a808740 --- /dev/null +++ b/tests/lean/simp8.lean.expected.out @@ -0,0 +1,11 @@ + Set: pp::colors + Set: pp::unicode + Assumed: a + Assumed: b + Assumed: c + Assumed: d + Assumed: e + Assumed: f +f + (c + f + d) + (e * (a + c) + (d + a)) +====> +a + (c + (d + (d + (f + (f + (e * a + e * c)))))) diff --git a/tests/lean/using.lean.expected.out b/tests/lean/using.lean.expected.out index eb09767d43..70c5ef22bb 100644 --- a/tests/lean/using.lean.expected.out +++ b/tests/lean/using.lean.expected.out @@ -2,7 +2,7 @@ Set: pp::unicode Using: Nat 0 + 1 -Nat::add_assoc : ∀ a b c : ℕ, a + (b + c) = a + b + c +Nat::add_assoc : ∀ a b c : ℕ, a + b + c = a + (b + c) using.lean:7:6: error: unknown identifier 'add' Using: Nat 0 + 1