From 87b238efcde0e871b1c0cb441295fb941d87864f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 9 Jan 2014 09:00:05 -0800 Subject: [PATCH] chore(builtin/kernel): cleanup Signed-off-by: Leonardo de Moura --- src/builtin/kernel.lean | 22 ++++++++++++---------- src/builtin/obj/kernel.olean | Bin 15580 -> 15524 bytes 2 files changed, 12 insertions(+), 10 deletions(-) diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean index 2e1564288..62a7ee6c7 100644 --- a/src/builtin/kernel.lean +++ b/src/builtin/kernel.lean @@ -113,12 +113,12 @@ theorem absurd_elim {a : Bool} (b : Bool) (H1 : a) (H2 : ¬ a) : b theorem not_imp_eliml {a b : Bool} (Hnab : ¬ (a → b)) : a := not_not_elim (have ¬ ¬ a : - λ Hna : ¬ a, absurd (have a → b : λ Ha : a, absurd_elim b Ha Hna) - Hnab) + λ Hna : ¬ a, absurd (λ Ha : a, absurd_elim b Ha Hna) + Hnab) theorem not_imp_elimr {a b : Bool} (H : ¬ (a → b)) : ¬ b -:= λ Hb : b, absurd (have a → b : λ Ha : a, Hb) - (have ¬ (a → b) : H) +:= λ Hb : b, absurd (λ Ha : a, Hb) + H theorem resolve1 {a b : Bool} (H1 : a ∨ b) (H2 : ¬ a) : b := H1 H2 @@ -197,7 +197,8 @@ theorem boolext {a b : Bool} (Hab : a → b) (Hba : b → a) : a == b (λ Hbt : b == true, false_elim (a == b) (subst (Hba (eqt_elim Hbt)) Haf)) (λ Hbf : b == false, trans Haf (symm Hbf))) -definition iff_intro {a b : Bool} (Hab : a → b) (Hba : b → a) := boolext Hab Hba +theorem iff_intro {a b : Bool} (Hab : a → b) (Hba : b → a) : a == b +:= boolext Hab Hba theorem eqt_intro {a : Bool} (H : a) : a == true := boolext (λ H1 : a, trivial) @@ -209,12 +210,13 @@ theorem or_comm (a b : Bool) : (a ∨ b) == (b ∨ a) theorem or_assoc (a b c : Bool) : ((a ∨ b) ∨ c) == (a ∨ (b ∨ c)) := boolext (λ H : (a ∨ b) ∨ c, - or_elim H (λ H1 : a ∨ b, or_elim H1 (λ Ha : a, or_introl Ha (b ∨ c)) (λ Hb : b, or_intror a (or_introl Hb c))) - (λ Hc : c, or_intror a (or_intror b Hc))) + or_elim H (λ H1 : a ∨ b, or_elim H1 (λ Ha : a, or_introl Ha (b ∨ c)) + (λ Hb : b, or_intror a (or_introl Hb c))) + (λ Hc : c, or_intror a (or_intror b Hc))) (λ H : a ∨ (b ∨ c), or_elim H (λ Ha : a, (or_introl (or_introl Ha b) c)) - (λ H1 : b ∨ c, or_elim H1 (λ Hb : b, or_introl (or_intror a Hb) c) - (λ Hc : c, or_intror (a ∨ b) Hc))) + (λ H1 : b ∨ c, or_elim H1 (λ Hb : b, or_introl (or_intror a Hb) c) + (λ Hc : c, or_intror (a ∨ b) Hc))) theorem or_id (a : Bool) : (a ∨ a) == a := boolext (λ H, or_elim H (λ H1, H1) (λ H2, H2)) @@ -316,7 +318,7 @@ theorem eq_exists_intro {A : (Type U)} {P Q : A → Bool} (H : ∀ x : A, P x == theorem not_forall (A : (Type U)) (P : A → Bool) : (¬ (∀ x : A, P x)) == (∃ x : A, ¬ P x) := calc (¬ ∀ x : A, P x) = (¬ ∀ x : A, ¬ ¬ P x) : not_congr (allext (λ x : A, symm (not_not_eq (P x)))) - ... = (∃ x : A, ¬ P x) : refl (∃ x : A, ¬ P x) + ... = (∃ x : A, ¬ P x) : refl (∃ x : A, ¬ P x) theorem not_forall_elim {A : (Type U)} {P : A → Bool} (H : ¬ (∀ x : A, P x)) : ∃ x : A, ¬ P x := (not_forall A P) ◂ H diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean index e2d592365fac6e91e660b6738a6cb83fae86ae05..af9437bc819fc3f5cea614d50b6b7b9d2a04e86e 100644 GIT binary patch delta 5427 zcmZu#3viUx75?wPo86UU^A35iNtR7EiIA*$kz_+i$^uQCDa67sKqbXIpm9cQL5j64 zlN38sWky>$9c@uY!>g@r1#EeB2v!hCwLVZ*LC+8~!prj1mYkx4BXesz>)XVmAs z2_CWdmPTq(8K>YVJ(V#>9itC2VxbdYnZSll0{R%90+ei?ruNL)>TTMXxv1eCkcIhO zKw%yR6z2B;W31vV;5>%!QzR><&d`diVm&^db!X{0EQ+ELKv8raP!wIzNIgh7<4d&Z zmht)OU(_-F;b|X$L*)JqC~_YHirhzl;=m=1)OvQ{V?d&!>`678HXpdS!F@=mT8DWz zh8_&OVi)fs^=Ge|@k>_pA1sUgD}ZAE6F{+l6;SMds*&2tVxIwSqxzgl1#F*9u@ipq z+bwvR`f{q0u7M_1`!DU!$y4j-?VO3~bGnw()$j!t#e*Awv)RB+z&Q;62Y3gd0y3fu zb@aJ4x+{+6mZa6;Ah8GDxf%?1}KiF1NN|n48U0oGXdGI(N(0O zw0{gx>WKZV*sw8W0q_-{!^cJT@m^4FPLmf}4Q9N?eAg%~P?&TbRE2t|>(mqos3ckx zSQ#A;vV@Wi7+{}r0J&@`S0nQlrse@A7W2M4M(+Hw@DZjLfVH zOq&a;t7`;WQiVYX;xvq?#wlXc~!Mz6+xsP z!)O)7&@=+-R2nJ_t0wxWFxM-xYbiMh%@x5wUMX0VTGeZqcQ0GE#$6 zqAKP*J@5uFJL6UH+7ZhAftFTv5bZMtsSSNe!a{^*E?qk^u5>Ojd3%s479hS}J?7)XnR9F#EN57iLB@jQLUw{dzFEdEQHp6&3U` zm6f8y%;j;L_lsh%ql~Iqoa3%e1SiW#wzNzq7%fBagAJKK1u>?VxfH7T%Q}si$G~yp zca-+iwBp?CUMGnhPLKFc%ZrN=;V*k+5S7-3) zWwnF{i`np5X$gj>H!p(tD7E}>veiC2My&~M)-7u3>2R6uilOlI=(kxB^RH#72Xhw& zQOO69nuaBV)%c3=qZU%Eq`u-VkUhfFU=$^oKLEi%EzAQzyrqowm>;BVC10!Ogz+h( z9D7G?eudPUc&r(4)lgz>3FViTXLD{n%<&=?Yfu=~L3fqj+9&Te9G)U5JM}x5OE>p2 zvyX9h*GG&i!#V!LKA)=Bk~vIhiP> zJWbQen#1>CX;djkFt^o>u=r_urYv8bpaW&SeR7iXt63sj!3q-es8%wxgEaAuF)zov z?PJF^>>2Zt=!OjDM$DcozGkIk93ghS&(B;OkVt7s^HZBRS~PC>vaQ2fwdZ3E%htIB zZ>$^vj!q=+J#pXRVsC^?6V02{HmN$i8tYDCUEEOd#Jb`oczO~NJ2>g<(H}DZm$!lo zFAGaj+I$(fqaOFvUXv5@X_5I8_#ty=Ai3~%2u$bVq zto(@T%cGTRS(ej>`^Hs{xoxE!Rt$bpNtJZplxM1ww5xn`NOlO{W&ED1PSCvSAxKCc zJxpndne=EyqB>3+DkdeRajGHUYM?hNB1y##p-~eusUT9R@8kAJR`gLv&Ceb93&=LX zTjLSu5Jh!eb0wQUqm7Xq^$6{bL_%`eat=m0h_l0Tkm3${JK2*wdZwbtZyt~dw8GB{ zzq!ky#2xk1p4&q09rl8OE6hmd9Q+DUa`0;hZqU%xF~)g?Thw)*IR6+s{{&61Y)pE} z5!`6G>7`ATP5L1*T-m4^DX(gNbd$rh*@0UCE5;ZyxV(>xp(okU0KHf>BWar>_#4~M zV=!@Y(Bn4ZUUhXsEV0QwVzQd{pdOKP4*8>d$R)mQS`In;ZnM_{29>fUV0u(<`oF zX#vD*aUJ5H{`ugI|0+ z%09kK@7Fh_J131Aw8F1!sA+x!GIHG=1C;RJ1eELjEsfl1rKbK-Ss-((a8tPRX`mrr zEv6S53j2zn)WAum-g8{)=1};w>}Cc&q>U=DarHQLJ(wOr)m4Wc-1?EzwseI?8iw^~ z_HsvbgVKZEF}n1B>-!SZo&;=V`BrRYJ&tm@VQrUGtJNW@b*w|zpo1NPC3iXPhz92` z1+2y}Sw3%q8jEc=!Z2behIs;hj*5$G!Et?p1=bq>>xFuq!i{apNB1^XFL;$RgufnH zWjF&UWq1cr%J8m6?l#1(7GuDcatHL_LPt1X18NZNxa;V%#)vmi3LK*HsTJ+B?F{hW zQ{31`5W640{E^GZJy+y4jq~fSz_Rro85JY_c4|nSqF1KI`qDImyN$yb0kd?|c|Zx{ u0-&GMgfh7;0kaKscbcU2bxfSzvYyh`-R^D^rc+nJ3(g_xjDWbI* zrWVDH6mmM%+S+j{R7)!YwzNP${eh>rvF1zMDx zJ?Tr*V6h=Lkjvs1V3LU8G6vz@xnLnC##(wYd1Cc%0mbz1Z1|FfDpAJ~0nPXTgMUDA zJq1#x2RDKyikob>8PLsjb`6!k5QP6=aEDC%tfjJ4pV~(KsS~|BK@i2)09_oxF3L}dgE_NUFKvFX`)mc&6Vp_djW zl{tItdmxMONk9>PA5e16g_6Mk3F-_se2QV8FF-k-Ty=sPJcW9kfdyycS-ZptiwB3TwQ^%xVj1`uKo)suC8gMe#2_l0oV8W zN>mHwdUDh!G}%{K^eJSeAfExQ;xax7$Vbm@1@W9OU)`YHzP9>X;EDVH0ZwJ>p94+< zWHsY1hK!>OP5S2WDs_NX4-coj24UC0>A6XJhj%u|gT`i60w9}JoDE);;uFlPQnx|i zJ~qo|c}B6Gt2byt_PCUz;0@STakMSFr}rR>CW9j$QUJw6Dxd_O1}K5214`f-fE{ch z6L1nk4HN{X$P+fM0RY{%mTjVvgJA;;o`lo;y7aouxha2Etb1Q?~d?~ zya}p8$`xmrO|v%a8*VFy%1yzX#ZfP4vO*tV4u?7%kV~wxH8LfgBLGth`S=~7LpjBv z{VeT=bUW_?KFs?u$6>~=+E3ZJL6t>gb0|E-}i$v-KgItH9-la!_bAcet1|4JD63|Q$T|tNQ z^7Q$+q{n(n_Sa3h0j|M0bOX82qq>01`k~fA9F1YHU0%!?P{-36e<;6ELkWR{aU+Dm z_Eyk8{CV}OAQc}I<&?*EDEyjAb#!(aW_MTDobLOVEdCB;%~~oA6uBZ{$g5&no|I#% zYFZYk^)`Sn$wP<+cM5YB^#>|cl&%GeRU!rQJ@<^awIv0 zMGsh9c!X;{s@2;-GNKX-6ESb+c@NDl$ZO~Zm5pMTnTrN|K5VZMJ5M!9aJ=a`ughsu z!SDclnvY_5To1Y-TbWc%1A!G}j{x6l_d{apA%CGqbyH1YK_VhyDf206FRZ$ICgy|E zvkr5t9KYr|J3h{sJ-9SmAq}eC5;k1cg3lIC2;B?yL1s5#9y7ba3VT|}r`l;=s8|xf_T# zx6!AO*-!U}8|zREBYud#1K_i~Dg@-$5|(Qy@iv!EhfBR(pv1GpUcf38O|?>S(a2tT zP@zT2o|dLHA9FctTm?Hl3a!#SY9&(n`JfsvLtY-1)`{81l%^QjB?oEC5HcMu8sQL2SfaqyIYA#6WvY`DS3EAX06aSg^E~FU8l7kPlQh3LR~@Gn#q)dpahk6dK}uG! z*oF@}9bH9n5t@(1UqW4~p+d-e%H@>;?47VLt%{(Sp*a ztP0{_)d9y>V~#CuY(CVnoC$sq$v#FjU&tIv{Us@mCRPxKNvS1~&{9a+iFNSxHjr3H zk}Q_yl_0S{EV(24Fw1{&8#?eTury^$&x4e_iL7n^U2=|!h8_WVkheU{O)CSAJjoBW zjq0l71~g>5JK)wKI#{8DuX__VEHB@q&qqZk{Q#6fUMet;d8vRG<82I5CC(m~k>5&^ z(i8MZ>GS&gB)`m)v=Xwijh>*i#LOgq)9?qCd6e49N|HRBa6F$JW2iAw=5`d@lyRDp zNvk4mx?EN;y)nj+&#B}%t)+f!yI5_*H89wSePBFk_gNI)F;f!#IHgtj^lktB^73FJ zTjrC@3yH90g0=+zlcB+P(#7(Uq}?$+D|mCOO|gUTy*)U+HO3em{LgF`&)D$i8ai5s z1kabEW2pq+$H6~M!zvn*p0yQ!i7=_XqB(vHh%S1zER@AfO-c>u;Ku5r-bgMvE33TE z+v;m=xQ?b(X1ksdZ@*w~zoM0u%}FoVGB2{X3zZkV+`}YO8*Tn3x)jNFy(%_-%{Der zN!55-Qk9x6(tm(-F`tQ>^rNauwVAe8O`O9=Nk0*!wR0P2K>p0HU`*#){Sk)Z82$-R zUb0&OLrmqSdavbaZgqCnJK)9ZKgVGVN3cuGBwAfvm?;E3x4#Rv(7x(u1H0FcHi?Tj zet@m-fUvmV37ErfaSF;1vaal1M>6! zNjbK2Irh-f+NxSv z6+|vVC7)OH2A~*X*F#q1OrZB`{VJiaF8Ymxcq<|3kd7Oye$ZAw1SoO*MI&bd7CCS# z?W%HneE7%@c?}k_0q1oP`ceI)Glkq*Xydry$Ngb6>$VmJiP@d7c%;l(^G^K zpt3;b_Rdvz=2Lflu9{1a)%$ykVAMb-Qvb5UYUkzr4Xkz+$PNMHVJe?+I8*$jSNl;Y zh4+cGNH^wAzC)cwkT-j{i0v909oQR2oBp%D0Ws}}n}HvGYPYbR7R=eW+>^18RExD; zRLjtSZpC!q$yq@UMg#ZY72>SLaJzgOU!!FDNdT?+Bad9H4nt^bf4YaeN zJRwj79HuJ`Wz)YN%K)d_c{ilB8sEeG#mUGyQ}i`c*2q?^SH++;(!$X}b&Pk{`q86$ zaS=PG@KQd6VOh#qKv@c(MgHFn{vdK%3i5<@dL*^z9E0|k_5X#|E$y5lLdU*BDA8^; KXK2otN&g4;A$y4c