From dfe46b9d259de966bccb0ef8a6b809cb2dcfa07a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 29 Dec 2013 14:01:30 -0800 Subject: [PATCH] refactor(kernel/builtin): move definition and axioms to basic.lean Signed-off-by: Leonardo de Moura --- src/builtin/basic.lean | 68 ++++++++++++++++++++++++++ src/builtin/basic.olean | Bin 21572 -> 24278 bytes src/frontends/lean/notation.cpp | 24 --------- src/kernel/builtin.cpp | 75 ----------------------------- src/tests/library/arith.cpp | 3 +- tests/lean/tst11.lean.expected.out | 2 +- 6 files changed, 70 insertions(+), 102 deletions(-) diff --git a/src/builtin/basic.lean b/src/builtin/basic.lean index 78eb30943f..d21bff7d3a 100644 --- a/src/builtin/basic.lean +++ b/src/builtin/basic.lean @@ -3,9 +3,77 @@ Import macros Definition TypeU := (Type U) Definition TypeM := (Type M) +Definition implies (a b : Bool) : Bool +:= if a b true. + +Infixr 25 => : implies. +Infixr 25 ⇒ : implies. + +Definition iff (a b : Bool) : Bool +:= a == b. + +Infixr 25 <=> : iff. +Infixr 25 ⇔ : iff. + +Definition not (a : Bool) : Bool +:= if a false true. + +Notation 40 ¬ _ : not. + +Definition or (a b : Bool) : Bool +:= ¬ a ⇒ b. + +Infixr 30 || : or. +Infixr 30 \/ : or. +Infixr 30 ∨ : or. + +Definition and (a b : Bool) : Bool +:= ¬ (a ⇒ ¬ b). + +Infixr 35 && : and. +Infixr 35 /\ : and. +Infixr 35 ∧ : and. + +(* Forall is a macro for the identifier forall, we use that + because the Lean parser has the builtin syntax sugar: + forall x : T, P x + for + (forall T (fun x : T, P x)) +*) +Definition Forall (A : TypeU) (P : A → Bool) : Bool +:= P == (λ x : A, true). + +Definition Exists (A : TypeU) (P : A → Bool) : Bool +:= ¬ (Forall A (λ x : A, ¬ (P x))). + +Definition eq {A : TypeU} (a b : A) : Bool +:= a == b. + +Infix 50 = : eq. + +Axiom MP {a b : Bool} (H1 : a ⇒ b) (H2 : a) : b. + +Axiom Discharge {a b : Bool} (H : a → b) : a ⇒ b. + +Axiom Case (P : Bool → Bool) (H1 : P true) (H2 : P false) (a : Bool) : P a. + +Axiom Refl {A : TypeU} (a : A) : a == a. + +Axiom Subst {A : TypeU} {a b : A} {P : A → Bool} (H1 : P a) (H2 : a == b) : P b. + Definition SubstP {A : TypeU} {a b : A} (P : A → Bool) (H1 : P a) (H2 : a == b) : P b := Subst H1 H2. +Axiom Eta {A : TypeU} {B : A → TypeU} (f : Π x : A, B x) : (λ x : A, f x) == f. + +Axiom ImpAntisym {a b : Bool} (H1 : a ⇒ b) (H2 : b ⇒ a) : a == b. + +Axiom Abst {A : TypeU} {B : A → TypeU} {f g : Π x : A, B x} (H : Π x : A, f x == g x) : f == g. + +Axiom HSymm {A B : TypeU} {a : A} {b : B} (H : a == b) : b == a. + +Axiom HTrans {A B C : TypeU} {a : A} {b : B} {c : C} (H1 : a == b) (H2 : b == c) : a == c. + Theorem Trivial : true := Refl true. diff --git a/src/builtin/basic.olean b/src/builtin/basic.olean index dde6574e90a55569443a566617b50fd22cc0edcc..c8313c601cd00501f5022d6e50d4d36cbe8c1844 100644 GIT binary patch literal 24278 zcmc&+50G7Db$|E0w{LeNh>icS83Jl$f`BOjEY38@CL|L^LTa-9X<<6^HhCdSH~W&^ zO|n$SMyLW3u#Hke&{kXIpQr_ewy21J3Mkc4nIf%LGOevxJN~Jl6{P2Pe&@UQeD}NW z?S{~Chg{A*-}%n}bMAM)`|WloI_=5L;}e~l{bXl$Hjht^&y05`Ygtwsy>MISO|`5g zU=8>3A8wU6rCb|R;ue(km~wpUwu$l1bS)bYZtYrDU(xMO@NP^QH*sxd`o94OE3;LM`%3j02lZ3(A(dx^ovy! z5u5nuyrpvx9Jutx5=HF4_T;Ad7;_9%HDg{*7>1Yy&Mu5)W$O~Pk3CkEdZpS06%vZ2 z=gmcN;L;n)B(Z6myHo86tFe(#EHw7_g3aoD=v?#lcN`F}Wi7rM@M#$nxt2Ahm}YB? z8AcYwGCQ;5(=%4(2PgA2;5I^;O98L+UQ`dW-j|s4NR={e-Dg!v#qBh{q@MI7Nafg= zv(Tb`G6vUEzf%BjAbcv|QS*;=q_yp-KROEyZ{xTWkNhl?e_2+pv*jvfnI=JJyI4Ov z-rb5ot)0Sm z;SH>T0rex-3k}~g2AmTuO_a1(32zVq4e@85ORHuiX|S3p`Ef;5CZRBiv}HtSpiYHQ zzk^;!ALu{;Lu*O6&l99CY3V*AlQZMf7fL_jiVM>!YI^QYf@*RFPCe?@@GKz{eKwZ# z8R=ChhvqGqcD`5$5o?;jlo#7H2w}?=A9J-WP zv*E(6=I|sbpyJaO3rjR;AD%QpONtD^_IGI?mq$iffzheuO5=rt}fuGSWo$gdeA9tfu<2%RO6Hr51JOU$y zh8wh7F%g#q5&e$NIi1zIfVDU(`9e`fX>nOZ7Q1V1;;OZAHK-^MAE)yz1%TkHRF*rq zxfqx53Zj&fwOj}lBjDAWkIvd{%|QMSVy~GRvua|zqFm{OMLH#;Lhr_GTbEn{c#*mR z`6NFj<$x*)CNJk0DbF2K6$@cRo%6wajYJz}+NxLi;s0beU`+YVPJFuwEs|C_HONno zen`lI8$aw|t`^Bl(AiD6+)Nh$+*jtuIF++ZHDGShl_x<)c8B-dzTis?MN5ptWq+j< zz8|nRSJzoN@xVXJpUfo(Mg8t0AhqPW-oZD3!+lJq8=VJ${(|1yv-w@LiAz-Eko@F1 zgB#2G#KP-z%=Hp^Etch~JZX?+ZA|T*5f*P)#>lB$6Q!{A^P9;=GvK2RzQx%@b1-;> z{L8+D%cI`LtAdR~B4K(1l41I{!Kl{LCw0n4}RC#^=iSRc7JCl6B$1 z(pw4Via-pM*6BX=NhCf{aB@1WnV{2!+R14hzYLkExbA;L7*~H7055`u&BGZ zNiZSgDSgNZQ3{JKpFRntEcZX<;M>(Bi9OH{+qw1UGfo0ZR54F4)qq`NLRmkC z+L)W4gHRd#a$meZC$1ILu;!95N&nSfnNa|rto@pPRcV&JgW%$#VoI4>g@zsvWjWhG> zan3iP`c!FJ|9QaXp?e&BuPVv8g08Q}WrMf#CR12(<;R$Y!X9Jbn%3#vf~+=cewEt8 zEUU>cK&F}XMF)SWWY$J#v581}$C@+)XHE3B9;RZlzGwEe^gfV90hFcF1r@o{|KoT!mm2`YXa9VS8c0}%ee?3Z=4{1pW2(g zEPW2I4-7;EBg+`XiEI6gTL$G$4V|lbE|)mE<6DELBjtA_#qOr2&|d$ z2?iNyE1*A%*S7k%ltHn4lvxtj>Qw;8z#=%LHywA#Ex3=c)wQ%}xT)UgAw#)C5I50U z%nI6PZ$f0lUTKP>3TpN5;qo6UgbIcZi_r*9`r5aJ02}n~%|br+?3k(eswM5r;$PBL zr9@k8KLE;_+JAAQ`G;yy9Rnx=jfd^P*|yNPsVUoKK{)I>j^sEPT!c$wIJ^xQ0g&8b z44F(OZhqBUSO}?3PyF*ZczW;j+^n`OVLIs`HmI4@KNdNSqX_>5@M6M01$;E&{{j38 z^<%!1rpAR@lyOm3i|kw*;6@%j%lgQ7iIb^mll>7S#@W$(ue`Sd4t-CYMm+&_mJ@yw z@acqq4*2zie*yRm!v70+CE;HJUR~k5P?j<-Sbcj{lw(7NOc()oFoBeS!5s<0AUK1^8WrhqSw9!$7@TU8mCVeM3~x zsq+0_?nuG~rIPG%B+mo76X{VeoX>M;7$ognNF;Xkpdg_!Z%! z7+hU3J(C9)WetaEc^_SnG%ZFLMa>72V*n44{N;dU=_LQlUIF+p!mk9(6Nba|)h-`V zu04H3iSf=$F{;F?Tw*98u|GV zxn?JFHc;T!yd0NHRK8R-&^WwQYw{UyWuokqoRmC^&Zlvc3xdGFIn_>N&4i$a7L5N}?c}SjA_U0_2<|lCB z-j7w^wdOsz$a+G3rwEm1IVsx@g$F~U)p^uVz_8(Bnqd$>&98EaukhDtfs)YoOl05t zlJ5c;b~eRb{uP|b^emc&<%NA(@m2**)W^KB{ED*VblCJgM*Q`F|C8_t;O`S&L1zK; zI4(aZI|zqS%%@%tbV2EQc{ zWAIB75sCh$L4*kh^xcltx~Y}jaD=c8bFE{H8O-GaVrys3=&hop@*`*~zS!MNy;#d0~r|CqiByzPj_W|fvq0H=~oMlkKm)w_fJ z__q?q)I3qt55P!_OFU!eC4(hI&;V!#&+{u0N35aFCKumvomj-TG&k)WAg~l=@;F2! zDYPc98RiC-m{-WfNH{%F(t#bxi3uDq$8yK|IZ3THEP29XD&dORY`1IdrOv8>-jzh{ zF$EL(n9U^tvxjvBkgKRQVdF~~6%|`z>&=M_z{k4Uz9=p5lsw(=*tPrvt&q8y1w&&XTXnFd_G0FLy^oGGXAeg`@9MP+pydf7t5>y=7=H z5U8>_po)A3A~!c=Bk6FpT&qeJ$+gmSrd>rmA6At^R)Vc1VZJvGPDQqmq6c>j`g73h zrq0?Fx5KFIDLK7oSIwnOz*E({R|#g|C%F8S*()F)YKByg3sR_*Aa*aq?XTuM{X9MJ z^B^5zW8V*J3pG9$hL0X1pb%!-kh4`dZ}@QYtHX6u>$gnXF?aujNL>Ou76qLk`~qN7 zkF*XqqDafu;X>S6SZFC^ASk&6EGZ-?Y*~xhFACCgkJu+MdqK#L3xbPp1DL!Jm&2X> zg^XF1moR-%^b9?FPABOcQxLE{`nCb2lgw0n{0Jy`poV>h+_S*s*cRTa;~`ZyI~#a? zKWQyhGx(`58wa|ztgQMdes?)q0Qm4?j(q|lsQEqxn2MWw^S4`sWER6=9H3eezN7%b z09dW)n`!F|I(s)(z4Eggm)1z6tz=_=ZRujnT%Z@OFm?c*!_97{`Yd;IY`sPxxVb#X z{Jfoo6nB*oS)h;fb~9NqTF};h{R5zVA;PXna49`xE~lmm1EFrUUHJK>x7BtI9huxT z@5Mfk%2BXu)kIt8ptmoiqM9dvTqy1PVhi1&wNK2O*0^smiH05x-N^~?H2cXZ>#`~5gSlf7q zC}61&dG%^ov9IJ+Ll&m-mmJIh^9>c`)eI0`^o=^`YUdkDhQ;KO z){qf9KCJNK5!~Tl4O?a{>?pPF)l?4#VK5H>hVQ~9+U2sUn2&(3VDdwW0Mk?$75XSq z;3?CrS(kI>4sg8H&9uWX)CsoTuW=t(fL^;%r}b3M+i0m%ID5MqbD6qwT5s_apa+0hsLE3`<_jnz>LM~l8cDqHMjKMk zN{~DwRhh};RW8t0_TH-?cW$-@v>zn4*0`212(ACE5GqlD{iMGNOi)HsHA_@rpqvUM zjz#I3ytlQ`Ff?LFNhFZ~XeTItQ44N&iF456lX~`sLOg%Nd>-OK>^Cta1J=o>5NOoK zn79G(n8DQv;6EWmPq&f}k~*^l_z(qYOZzZk%#7XAKLMyhk^o#1M}DZ(DHhc~0n#TP zRQ8f^&yVYoWR3XlA`w7FcOA6&Bmv6e4}Ap4c>w|7N3t1PCeSc1}V3q2Epz*=)5?smxrh@i&)(M zKUAB_3_*)!9!iPn@zCCJMfI%-r}{!5eJW{$xv%4lwhzd+!6O#RPdfNh0uTM6#-AIg za^$TTuAQqe5x9o8Kb5u67JtcSc)a7w0@1Bh>}1;Z_?!gJ4oecivYuzt-YDZB`gI|z*IYQ^&sHK_1EdnmZO0#q;`g>hgwhNp*FgnBEg_q*6=h@%0Mm5 zZY{!USs*M$Qii`pFzioz!^EL?=1I_ef&@y8KUNTk1?&|YWpRnJz_UoCpbKKAt0{XV zYvu%n(_ze`Hxk$9lSBl4N;4=@PU+%@G4*qSHI81kV24*)OcbvhMuw{Ri0W9nI7#Ca zM%g#OZLM(=STl5(C${=d{3a&yZyPu|52|jEILs4dZVcGkY7)@XJa}r&4Wm6=8TvX% zY*Ff-SJHj>$l{trzBWFq?vu8Y;jVL$CW=Uh70#os`wZ_SIh6Df3^UdB|0ILM6AZ&6 zfG6kZJ{4;1?xB|RwF7%7%lvnA6-}0!`|jiD!M8%Wy%oy!?mi`cMeXNBv%lJ@p}I=p z@Qvti=AOy@(AwT4te#Kumy0OdYtX*{OGeJG2CPoR$(D4EivwMBt+>BqGcn=_scxvG flG|+R0hu!VK(*U2WB4P=+Y)-!m_))^+fL}!T2nqt` z2waXN`bfaX>eyH*KZTkqjsw1@*AY`^L`L`fK&?IXbi=_`Y?>In?Xny9%uMf?o>v4k z?uztnyC?gD$s09HgXw+K6XK7~{9s{{?f^+yY?+*zQLaMuUzIQ|OkOd$VPa;^I6BHP z+m~rdwR~0Cnc}c&eM}L!*GqH}!3mWbmboQi$*-D7l4=3~May(_H8puT(5BTZ0B<4wm4ON9 zt*)%7yXi`cKnEi<(sC-xrjvvs$))vsg+24vc1RLERAbSfWkuJJ8pQ@07FLH^t{|5d z*~$RF3h)lnyc+OMRbQ$GH%H+jli})>t0IoB@$N!k%FL=$1S{zrf^kWIVf&2a`>xcs zvEarCLaa}rQ=bMzm9e;KWW;hLsYQzU;zlEwl|pPoT&RrA-hGlAk(9kL8R zg?ZR3JJVAbbZY_L!FycQhSh*p;Zj2%;yeuDsjd!a@*Z}&Ad~QH+Lp!zIyG|+2D8OX zqaRMrnKI2RY&fQj_Cp(M`l`NF)>*(C{7Xs?A;m{=`4}$u(ywd@T2|)+eV@`w*Ag8r znV#FRdt$H)eGFqNL8@4W*liwiVvL?-M2fQroJ^cX?K3JPu4#FepDA+EEMM23ogYl> z>CY|UO@^8_>O}5CpbU*)wA3gX2rKb(h0I-dUVzVUxbb0(Jwg`%d{Dt`0$qwjx+wvZ zjIKNz%*EHD-_CSjVuUU;d$PuGj#9+Nz%JchaN8kJjPtICJMKr&?J|F0*u3&9fGweZ zHNY1FewxYj+8_bwZ|S{cIBs4_o492`4#`iIGq@RM;RQMtI^PxjdD%Zm&xREfU^R;p z>k@Nd8U7U?wa^20g)}{12ZY)8YXN?Ju!-hiQ0wTQ0sTv~@pKnCE}G5l?%#CQTuxz}1eB=asu$~^TJ|N^vY&S-*H9aC^9vBFtSxO2YttY}C%<8d2-!BW zZb<4gbt0F^iP@dz#40~QvKbePiR=_B_$mR*4eU)@0ACsdl2uJ3__6LFwB(Mojunv9 zgDbL?hA(|IdSz|=DOwRRZ_D!~A zTnvyOE@knc7na%v&O#XrS3kgeRAmYkbom%AhnS~(X%49Ij8Q(W_jR`fSF^LIq)=~* zJL5)?kk=lLV3r8(4q=2nP^QH*KC2E_4NDWj7a$!v$5SW_k-#3!B5@;KSTHc;Act9BCux04O)A((4Y0QTgiQEx|od&*|kB*5eCtUpnb~# zx?T*foKpces#l&Dc8AOX1w-o^jbiL^h+?RSDUK>A%KyUUCprlu<{cKJ37oYCIoi`l z@bGvcCyWd8a)OA+PN)RS4@c1x7_oCZfXT_*yMVC}-&|^LzdLZrU`G!O`SfjvL<4Hd z-a=P^@a1ZkVHxk^AzlXH1Y|94Il?nN&*b1w>sX{p9>qMzAtY}zSof0Fx%I$}cKW#N zqi$IT($lqgXUo8QWuA_m5WWxa*-Z9Z0k0u^8{qTQkJY)F+U~U|o_o3)@0dni;Q9C8M0&BU}Dyq%Ca4>gLBy#z66X~x#zvRq*&hZ0n40pJ5;@r z2EHHgRfK;NupOg*0Pt4gKM435!oLOhx)$eoS<1NhAvmvRYLXzyvdmEjg;}yO@znag z+u9Eys(iqdwsW+weFzvUoDU1wVN-;M4yjuC=^S*eRTxPzK%2x*AYB8Dqq1n+DPxIw^6a&1U>k!*)?Vx;t0uyxl8Kz+ zFMF-yEeHfgrack|(7=6MS(8^%g6-U6jZ{awTxs2#UIBL0Y$OmCCvz(G#XXRD7XyG( zn9fHC-)l+$^}FgibidBsxZFdM`vM7fmP+#RK=KK|pCtJw0pA}hW+d?kS2`*eYs9+| z0;OBQ&LdJuy1uD_UeYy&SwPR#?WrCoM|6pf{e_Clvl})yi%~Pcb})yL0TY(H8a8`> z$u^ee23sqALHp^ds?hSA19Hc5pgF(jGT=L@$kqcCf1aB$_t`vstmuY%jfE=tr?);|m+FRe-N7Su`p2=GZH{~}=7L&>k=j{%=d_)CCSD*ubL zlW*jb&mc44+=<4p5)(a`W6&kL7f>^GxFRkL2q@Eiog!?9b3Y4kjJk1G6Klx!H!2yI z3n`eLAqu*Cd4g)aE>Y0xHd|soCzHuX6!;07qYeGR#LP^+>NgU$dJRkUL`1#FS_MgV zPN@)E8e_IvGm1|3`qL;r0tf7*r@jn$itty}4>|#!7rJQ5-D!?J2Ka3x;9PgaK)ZY} zTSUx}_F!lGOc~bgM|VNjXInABRqaIp=Wo0o7Hst+{wzV7WY#|}!H5@d0RsRNMjyln!*Q$$EF z`-UR0tx}q5cSo^*7Q~9^E*9?Y-AbuVvsgbrfjNt=E%*!$lx1*8t7%)vTQYqRFS@pY zXcDXRPgpo1^dmZxb@@AoWeGC|nsz^zRn4CYI*s=F{nK;vbBA9s7mFl#R~xRhVGFIq ze^Mn{`It5&YaU=IZ?wZ#Zix1du9fvyK>P`_;jaNdLip>Tv>os_r~^i|_`U+@tEBrT z1Nb*UJx2I%m0T0)5YTW<_X)Q{Zi;t$iee+R#q`7g4w1UwR8kDdkGw}z2Vmd>im~sV zm{N8o0ZQ!rMPpFYH@0&F+K!trW^$oa(R~`1?`bAzes!N#e#=fdoXDi93U*Kd5%x~c zGy?`d-5+o>ukb(80wtmEX&RkCIDc#Kmk^WoU}n^F=pWWz?d?mn$~A$Vmj6#tuOv&p zgW;br;@<`QKZLOZ>;5m{@6%bp{1lg;>AfZyon-Q@KS`IB$#pL_a%9CS=PtF&EonuV zoWX#a&ru`CQ8IP61YyWsX|Ql-WTAYRM%j0Be=ox$FKeF^3Xia3Se9nB{%s+VTHiW3 zzj@EZUVOw>7XFz>13M+VwS*3ztfd(F1}#P4RalC#bu+HVn+NOqeq5ueYaL^|=!P=j zP6EEP_YU+{T}{=eY9O&L{!f6d=zl~Q63mCc1I)-7xUh*cwgIUzB9%HfJ^u2JrMU(w zek@1DI9MHWLFk$oX4{>{02{GBFpr!QiLbZFX~}syW7=9{d{HxUMqQ<5QmV15*3j4u z5fS3LkeC~z64f&ms4SI9OpW=98Qk(?8ao+Kov{1bJXkw7*O$X4grY6n!0!N8GxUq9 zo((n-)XmoLf1`AD;lBs?KL~@hN)+`2FcRa2%+z_=U<2VA0L|b-aW!V`8y$fWT6ej{^ab%;XsmH3P4U1YbQbM)+KmN#(KIndWI#Mj)`<6WkCMOv@FvN>i}i$GQT@UDQT92BqVMijC$Z258e7`K*d15mm|~ z4vqMf5G;&IV(5lJE%Ab+k*_q80>~^Z&KzV0kSw@59pE%t6j}Ljn7bjhA_Dx4+R;xb zDCZ|)tiJ>Ry=AD+4OE(I?)0E?03pE>1Tf{8_HD@`xz=E3+O@>ue##5a}3<-%D>ET-NwpIa~4A`2DK6^fO4|9Ae3v(}C z&3Ss{+dGO841K@ndkYv^Pd3I0>d8zSO128;4J}GH16y{_+1K%Lg~(k3JNzSSOwJv9 zi$_+N;;EJ^pyg?GSM9B6b4fjkE39VGBd2E`5rs79B(C0IK}u``a@RWzmla|D)07qB z8oo>CCpP4_l5Ro|w6E-@^;5M}R12&&>o1E%85r(5_;ci%n^QnkWgu>ipUSgo7@ zL~k3luRje3^6Ere$;QRCrHdgB`!G>lwS6(*CEOf1nKj^vYU7^UQ?vMo)&c4P^Yc+Q zkf^>^Ht2FJGtAAF8wfBSaN}!YGvaul+g#2x$pi>>Zy|)gPyxM#pw-&hoy*4ka+gD|`|RB`y9sj`&iA zajS1;l>D_8P%Yy?>(n<3Ak)=TQ@3<#7Xag}GuYIe$Je+pZc``YX#j?=Hi>U(g0+nk zp?8Z{AA%L1Zg|y@wQ0#G_=$p4v)LQ*cBJ=E@C|23eM43k0R7^kDv9=-o-@P+jZE_x z=nVN_gWC1cTzmz1_z+sYGQcMj25XX|IM3`o+3=cU6kdN zgrqhDI^Zy=_bts~Hz+8JuRx35Q@A7tT$Y;4nc!J4|3fxGo#VAWO5`$y4M!CEOHBi$ z_4K3wy(dD>(2up77L}M;_hX3rPlkdMTHX%zG&EVP38=ahRXM8GNqF^L%xFtVH@eNz zg0RSs+I}sq{Uw$&ZvZgG*G|pkR{_(g|By3`NaRu_fv^KJffC_zKf1Dx*66EST&+@F zjUW(WW5&kWt1=lqQzh2%S0-FsqOv7_T`5gNHdc$R_xb^HB>~c`LH;5@I%vqgDrJQ^ z_@~&>i@@!A>5wK$so!7e#$xm$HOJQbm7pJeeHPnAH_p-jdWy_1nMxdkEi1OhR7V0z zYy!8PX#yPG6eH=Y6^U?d^m^Si3QrZcYztj`N&}`B+nuKNFSRFT0F0FiX>Okdcp0H< zZiyK>ec%tC;a1He2mI*v7&-e2vbj_(wpH`EQ4Ew#zUWgMei`Vc>T`&IG@kn)DaMl@ zH(6)4zlBOpN2&!Kg2GlZ>C;K$BRffjXLLU+n2Ce=(b1V1`wk;Bn)aCjAxq?Ma9G`Z zoUAmkKdK}{(h`KjimJ(?F<;frB8?>7c%uzzrbv*YAXOQDvml$w71|CR6R$ShYz^o< zxXkt%c=wcM!wEtqvi&J(F%^8%i)rvLSAiv*>13_eraA!D;nrd>X?Q^Jgf&E^8BtsN z>j$=wIEOubv!1i*`7j^s95y|4kB1nNG@IpB2sE0&n7Cod1d!Q5*-QY*i$=U-@tFDA z0xsl43cr>xI8(PQngFIkGXZiHo__))&$(5$Co{nWKK(8u0=cD&=3o06M>hTQNr3fx zmzeD0~*)0z*v!AOgOi^HOBS{j^$W3ON@D%F|B^Y5nollQCP(5T+g*s zbq24{<_wN+p8+~Fs!_gkU1l`kPW)^94X&dlMKCz51~0{+#b+boWyZ%Ruz6!VFl6(- z0EMT26x{5*zBk2G{}0usb9&I+Qs0g(b53}(5mo(Mba-5m$JM8uUPdvMG?YBo2}bh; za;f`T3#C5r8oXKb7#nEIvW@=zP|c!V@R*VaT>Uv*=Q@sI%|59tFIUQFo_(aYH~mBc zhx_6NST^)CwX0+tL|d7uV5mM42cvy@)$x6Zc>#2mUS!lOzJd0DjU1t<@U_F(hq*Wz zz7_$N7IORKS;_r5SNqykLO*s35A(JFejnj&fcb}n<<&In8lVok^0>Jjm-kZ>fcWEr zu@9yZvbC6s%6Jtn3cW52=qN zz))Q{N9O%GX=8f2J&&fOtcnC4~Ud>=du%W`Kguu{r1>T^-t_Bm#+dt zNbQ@ccD2S|T!q@dt->_%Gpl7NdtxSp6+^%4puKH57Sg3rxT7quqvb0X7luDTynM|P z7V<^7Zra9QLwTx;*NHk5n$XbTo5*=~rb*30Nl_l3=4IKbjI%5dk-}GAE0=NmAEi(k zL5$rMs7av2ZwSN!dO!kLi?~NcaEDo<0b-g^Q??o>4#<}@ay_TM3YMrX=M75mr1(6|6TpY?-NSiQekOPwOzLB^qv=r!S1WEuo@@7MDXRAb7c~nyZ&u?6Gsmd*&Z#Ln5DUiN z#oV3){O%>XPm5Z24pA%m4W7!%G&T(8e`HCN)%a8M*nI*$C|Z!B zjp(!OPK`YzpqnRk1nmj;sw}lq;1p=S%$-iKuBFZ@tcFS kO~H06?gPsen6tiJenZZ4?DzZ7$1{p`*S_&import_builtin( "lean_notation", [&]() { - add_infix(env, ios, "=", 50, mk_homo_eq_fn()); - mark_implicit_arguments(env, mk_homo_eq_fn(), 1); mark_implicit_arguments(env, mk_if_fn(), 1); - add_prefix(env, ios, "\u00ac", 40, mk_not_fn()); // "¬" - add_infixr(env, ios, "&&", 35, mk_and_fn()); // "&&" - add_infixr(env, ios, "/\\", 35, mk_and_fn()); // "/\" - add_infixr(env, ios, "\u2227", 35, mk_and_fn()); // "∧" - add_infixr(env, ios, "||", 30, mk_or_fn()); // "||" - add_infixr(env, ios, "\\/", 30, mk_or_fn()); // "\/" - add_infixr(env, ios, "\u2228", 30, mk_or_fn()); // "∨" - add_infixr(env, ios, "=>", 25, mk_implies_fn()); // "=>" - add_infixr(env, ios, "\u21D2", 25, mk_implies_fn()); // "⇒" - add_infixr(env, ios, "<=>", 25, mk_iff_fn()); // "<=>" - add_infixr(env, ios, "\u21D4", 25, mk_iff_fn()); // "⇔" - - // implicit arguments for builtin axioms - mark_implicit_arguments(env, mk_mp_fn(), 2); - mark_implicit_arguments(env, mk_discharge_fn(), 2); - mark_implicit_arguments(env, mk_refl_fn(), 1); - mark_implicit_arguments(env, mk_subst_fn(), 4); - mark_implicit_arguments(env, mk_eta_fn(), 2); - mark_implicit_arguments(env, mk_abst_fn(), 4); - mark_implicit_arguments(env, mk_imp_antisym_fn(), 2); - mark_implicit_arguments(env, mk_hsymm_fn(), 4); - mark_implicit_arguments(env, mk_htrans_fn(), 6); if (kernel_only) return; diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp index 95a6868e9a..62b6f4412c 100644 --- a/src/kernel/builtin.cpp +++ b/src/kernel/builtin.cpp @@ -190,85 +190,10 @@ void import_kernel(environment const & env) { [&]() { env->add_uvar(uvar_name(m_lvl), level() + LEAN_DEFAULT_LEVEL_SEPARATION); env->add_uvar(uvar_name(u_lvl), m_lvl + LEAN_DEFAULT_LEVEL_SEPARATION); - - expr p1 = Bool >> Bool; - expr p2 = Bool >> p1; - expr f = Const("f"); - expr g = Const("g"); - expr a = Const("a"); - expr b = Const("b"); - expr c = Const("c"); - expr x = Const("x"); - expr y = Const("y"); - expr A = Const("A"); - expr A_pred = A >> Bool; - expr B = Const("B"); - expr C = Const("C"); - expr q_type = Pi({A, TypeU}, A_pred >> Bool); - expr piABx = Pi({x, A}, B(x)); - expr A_arrow_u = A >> TypeU; - expr P = Const("P"); - expr H = Const("H"); - expr H1 = Const("H1"); - expr H2 = Const("H2"); - env->add_builtin(mk_bool_type()); env->add_builtin(mk_bool_value(true)); env->add_builtin(mk_bool_value(false)); env->add_builtin(mk_if_fn()); - - // implies(x, y) := if x y True - env->add_definition(implies_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, bIf(x, y, True))); - - // iff(x, y) := x = y - env->add_definition(iff_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, Eq(x, y))); - - // not(x) := if x False True - env->add_definition(not_fn_name, p1, Fun({x, Bool}, bIf(x, False, True))); - - // or(x, y) := Not(x) => y - env->add_definition(or_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, Implies(Not(x), y))); - - // and(x, y) := Not(x => Not(y)) - env->add_definition(and_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, Not(Implies(x, Not(y))))); - - // forall : Pi (A : Type u), (A -> Bool) -> Bool - env->add_definition(forall_fn_name, q_type, Fun({{A, TypeU}, {P, A_pred}}, Eq(P, Fun({x, A}, True)))); - // TODO(Leo): introduce epsilon - env->add_definition(exists_fn_name, q_type, Fun({{A, TypeU}, {P, A_pred}}, Not(Forall(A, Fun({x, A}, Not(P(x))))))); - - // homogeneous equality - env->add_definition(homo_eq_fn_name, Pi({{A, TypeU}, {x, A}, {y, A}}, Bool), Fun({{A, TypeU}, {x, A}, {y, A}}, Eq(x, y))); - - // MP : Pi (a b : Bool) (H1 : a => b) (H2 : a), b - env->add_axiom(mp_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, Implies(a, b)}, {H2, a}}, b)); - - // Discharge : Pi (a b : Bool) (H : a -> b), a => b - env->add_axiom(discharge_fn_name, Pi({{a, Bool}, {b, Bool}, {H, a >> b}}, Implies(a, b))); - - // Case : Pi (P : Bool -> Bool) (H1 : P True) (H2 : P False) (a : Bool), P a - env->add_axiom(case_fn_name, Pi({{P, Bool >> Bool}, {H1, P(True)}, {H2, P(False)}, {a, Bool}}, P(a))); - - // Refl : Pi (A : Type u) (a : A), a = a - env->add_axiom(refl_fn_name, Pi({{A, TypeU}, {a, A}}, Eq(a, a))); - - // Subst : Pi (A : Type u) (a b : A) (P : A -> bool) (H1 : P a) (H2 : a = b), P b - env->add_axiom(subst_fn_name, Pi({{A, TypeU}, {a, A}, {b, A}, {P, A_pred}, {H1, P(a)}, {H2, Eq(a, b)}}, P(b))); - - // Eta : Pi (A : Type u) (B : A -> Type u), f : (Pi x : A, B x), (Fun x : A => f x) = f - env->add_axiom(eta_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}}, Eq(Fun({x, A}, f(x)), f))); - - // ImpliesAntisym : Pi (a b : Bool) (H1 : a => b) (H2 : b => a), a = b - env->add_axiom(imp_antisym_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, Implies(a, b)}, {H2, Implies(b, a)}}, Eq(a, b))); - - // Abst : Pi (A : Type u) (B : A -> Type u), f g : (Pi x : A, B x), H : (Pi x : A, (f x) = (g x)), f = g - env->add_axiom(abst_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {H, Pi(x, A, Eq(f(x), g(x)))}}, Eq(f, g))); - - // HSymm : Pi (A B : Type u) (a : A) (b : B) (H1 : a = b), b = a - env->add_axiom(hsymm_fn_name, Pi({{A, TypeU}, {B, TypeU}, {a, A}, {b, B}, {H1, Eq(a, b)}}, Eq(b, a))); - - // HTrans : Pi (A B C: Type u) (a : A) (b : B) (c : C) (H1 : a = b) (H2 : b = c), a = c - env->add_axiom(htrans_fn_name, Pi({{A, TypeU}, {B, TypeU}, {C, TypeU}, {a, A}, {b, B}, {c, C}, {H1, Eq(a, b)}, {H2, Eq(b, c)}}, Eq(a, c))); }); } } diff --git a/src/tests/library/arith.cpp b/src/tests/library/arith.cpp index c85ec2dfd3..5701a4c14c 100644 --- a/src/tests/library/arith.cpp +++ b/src/tests/library/arith.cpp @@ -16,9 +16,8 @@ using namespace lean; static void tst0() { environment env; + init_frontend(env); normalizer norm(env); - import_kernel(env); - import_arith(env); env->add_var("n", Nat); expr n = Const("n"); lean_assert_eq(mk_nat_type(), Nat); diff --git a/tests/lean/tst11.lean.expected.out b/tests/lean/tst11.lean.expected.out index 48bf9162c6..175020fcdc 100644 --- a/tests/lean/tst11.lean.expected.out +++ b/tests/lean/tst11.lean.expected.out @@ -6,7 +6,7 @@ ⊤ Assumed: a a ⊕ a ⊕ a -@Subst : Π (A : (Type U)) (a b : A) (P : A → Bool), P a → a == b → P b +@Subst : Π (A : TypeU) (a b : A) (P : A → Bool), P a → a == b → P b Proved: EM2 EM2 : Π a : Bool, a ∨ ¬ a EM2 a : a ∨ ¬ a