From 4d533c6a256d551b6f1fd416273257347f5ba15c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 30 Jan 2014 22:13:34 -0800
Subject: [PATCH] feat(builtin/kernel): add nonempty_range theorem

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/builtin/kernel.lean      |  10 ++++++++++
 src/builtin/obj/kernel.olean | Bin 37933 -> 38337 bytes
 src/kernel/kernel_decls.cpp  |   1 +
 src/kernel/kernel_decls.h    |   3 +++
 4 files changed, 14 insertions(+)

diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean
index 12fac3cfc..11af8252c 100644
--- a/src/builtin/kernel.lean
+++ b/src/builtin/kernel.lean
@@ -650,6 +650,16 @@ theorem exists_imp_distribute {A : TypeU} (φ ψ : A → Bool) : (∃ x, φ x 
                      ...   = ¬ (∀ x, φ x) ∨ (∃ x, ψ x)   : { symm (not_forall A φ) }
                      ...   = (∀ x, φ x) → (∃ x, ψ x)     : symm (imp_or _ _)
 
+-- If a function space is non-empty, then for every 'a' in the domain, the range (B a) is not empty
+theorem nonempty_range {A : TypeU} {B : A → TypeU} (H : nonempty (∀ x, B x)) (a : A) : nonempty (B a)
+:= refute (λ N : ¬ nonempty (B a),
+     let s1 : ¬ ∃ x : B a, true       := N,
+         s2 : ∀ x : B a, false        := not_exists_elim s1,
+         s3 : ∃ y : (∀ x, B x), true := H
+     in obtain (w : (∀ x, B x)) (Hw : true), from s3,
+           let s4 : B a := w a
+           in s2 s4)
+
 theorem if_true {A : TypeU} (a b : A) : (if true then a else b) = a
 := calc (if true then a else b) = ε (nonempty_intro a) (λ r, (true → r = a) ∧ (¬ true → r = b)) : refl (if true then a else b)
                            ...  = ε (nonempty_intro a) (λ r, r = a)                               : by simp
diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean
index 001db09eaf01a750dffd7249b94cc7a1b28bddb8..4f90998b4c836178ec72570f21a945f7731297e1 100644
GIT binary patch
delta 3421
zcmaJ@eNa?Y6u<91cK1D{940<wNwyLZ6*ZMcN=C<~8u1UIW<^3_MMl&qfgwv6gGG@=
z!QsQ>(3j>UQj|G0X4aIZY4&AhmQ7z18`Vr{n&FWB)ztl+`}TvSkr~eZ?)jbjyXT&B
z-rGIcufKahf7M;*ud1$Ey}o8cy|1>sYRzil)E5f;r8)Jx8I(HpMPedgE=-wIFUP0w
zM0`GnTpLfpo5t{Iz*2_KNMufDxEo$ihBW%)@Xm1PON5_g#_-zIADJaI<v^Iok^g$O
zL$AX^&xSQ%TrzUD(400g7rwYjp!8F~`dl0+_A>+u@0uetrEKrj{C$#kTyW_1h%@KG
za<q4{MEYJQ*1dog6WK~5TzntMn+ve!4RJs&hrSV?<^qSlh><X4vN=M-ZfBk}S|6Z@
zXDBAfkBa>DHE<bEN~3GqhP6UpSLxeO`zSrPX)Z0ROG<eWyejTXfGUFnbgnK@D<qHK
zO^52{Bos~p$JO#kU@oO=bp`hq^No8!v9}Ow{VK=0!(N|6W^op%%W&d~W_e6dF`UKJ
zQ=gISW7WuhoBF&y(W#{9V!g*-h7HR&G%78WR(uKL!7;``hA@1p+7!jaWL3&~$uit5
z!X}j8EShTQ71dR1YT;2r!l9;%BTKmI;Z5cWL>a8SCcFXNHcMbwIC&zZbuW0cC?<;)
zJQ}ZnivzzL$jCDEb?a+<b|&Q7v@m};PIf|7>;{ZmDUDf_0d4J5Y3#lf^8^buHL8E$
z;zQHXPu-hVq`VHFnuH^OY7*YSB>3C7T~UQbz#fi@B+tsDA|1La96z5TIrNnC%^tK@
zaVMk{-_z{m7W6_|>0zBWYN&Q$Luce{Zf_4~8JV0;4&tHO#j>L)IaEF+h0xWJrad6n
zDggq*Rn5w%>B1V_H5JVx^`=}4PfSibsj0!8xegS9gaeHdJS|;es0OW@PBf%0>;jJt
zie&KI-ccjc%_H&_q7bS^WH*jBYslT`NjhXRimru{`7kYMOqt@BP~EH(<ubR1*Gqw1
zp`kcT9gQU^$KX>#@eZJaZ+e{mZ7kQ8Q@Q`I@uyK)qY@+<CR{vhMn6?GWof7BiKg5M
zA4|7+hT}>R5*>G#E;WtUj*?^Zk<4Hw*pKAD8I;C;slgYBVrX!4qVp8IX;i)~vB1vh
zeR$MU{{dh=XZj(ammzdTfFTmnhZvrb&>UchC&nD4vMsmF4^EPp-*;w^C#M4(lG6GR
zE82MN1az^ziETT(>FAb{`7!%c64%@3%;Q5bqvjBKn{P?LdGhNAmc7@gr8y^aI1>)8
z(y#=am0lr{))&Q4usPKSo~tMV5(#g3Hcc?rSUAC0@&CiHrU=9`(Pu2%ntq2;it<W5
zKGV(#@;5?6w7{TxW{^H<ao;->*)#-iI9t79BqLmswl%pMy`gYxELklx{jo~n>ERr#
zgqTg^coZu`qH<)R_gP3ZlDP085$$}4vGCn00wcpkfNEM3=}b#nW=tOZ@M(R#C+bEN
zA4v6c+2X_UTo=_UL&jTf`7Q6OLRW=(<vJ}uKpac}#w-7=8)C!5Om>8s#^+-IRDPpI
zBa-hhoeiYtgyXGoIAl6Z(#W=|^pTA<9wwD;ZB251C80S?d9A6*tieCFyj((?dZ;z$
z_Snin#jYHrGSD#*X?r%EZA~3BBlNC1NmpCTCVzn#^@8G`01BRucyXS!m^N;!y}4jy
z<*h<Q<*UZh-)-sC(CMa`?FqDGdyf1a)VzJGc8<)pyXGwpeSsav4)wnI22h>$Z3KQ7
zf!|9g4{m6isufUw+niCyS0mP=iXx9MPVj~=%#&eN)5`WKV^)PO{54Vgo?L!EsF(AP
z5KwRsP-XKI;Gjbq<7YtiPW<JywL4zW()LM*j;}APH#`^WZLp7~cI-_C@9YV;n7d*1
zQLv+6*7K@RGC=jnBaw(2W(=c+Zs}x~)YsXd_0kWW9&I1})0sYPf9#P6#%Ne4V;Q=y
zYku0xpzv$XdMqZRQ?$3MVAgx8b~4~P8J(20o~<Iu(_QR&J5ps%83ESDP>~0yr~BBQ
zze%56*$aTGvKIm49nu)T1FAu|1el*?NNWtxj-9i$U+MVHRa%g4qkD4y0IPa*1yCvd
b38<9t7POVF0_NkY)<t@j7HF4gfC~NteW>Fh

delta 2996
zcmaJ@YfzMB6#g!|%lip`C|E^^wFDt9H3{UZj5=jaJEKD-%{XX*F%y3fQ-5S$*bQM(
zkOU7pTI;AF$z)O^g_W4v&Fn&%HZ{}Leqq|p#`@Dtz0Y~S-EaA5V&*$M-?=>Jyyu+n
zg|kPEV}r&k(>Ku2(+`*I)8tRKR|@kvz!Zkh1Ev*9Vf+jjkdG*(l8sB#OY@=F0KwYX
z)UmPZp^7{x`V-nxyc^fqcX~owDUqmfXpu`Sa5+`56BTXB^H(yf6K|UiHD~w~6*X@P
zgy$omoL!U3Dv(<3B18ab%>4`@II9Xuvbd_6$9#V2F3J#OGAc5S`ZY}r>!49YnwN4m
zPkDUKOehlWVlG}y=4=2&BF!fsF$aPv{WC#oR7)W>uKaW1Y#xBk1ACCRZLSUlk;Yd8
zZ4A&;Cxs}>1CjoT6!uUm@}be5g0RN~lone3Bz~KFDSyk#$^l?C`xgM!?2iDtXWx(y
zZBl#b)RwI9B(2v_tqG{^`HWQvQzy9Fe)F7>8WDtOWVe0^Rgn#NpR_e=+11sb^|GLw
zG|kzKM)u;hS<AGOOmb~f6&GCZp)<`HVQvRjL)@FRFnC`Kq0AVbIVgn|a8<E}Ghyt!
zAX*G4RwRYE9}tn67n4%Eu{r_OLak_mDaNd>Jy{J4PtlJc9{Qv$Y2qz;G49G;Rdix0
z4TS@b^u<ZQB&xt9LU50%<y!!(#c&L<5|F>?Moe4q?9?|7OG<os4%2OsnyJU2Q_C|1
z=;bcGOcYtA2kA!S#<V`Lnoqz87A=LBQtqD7QmFS)aZB(P?3x&4zenMc?01+VEz|Uu
zXkW`n+UP7;&&x-Q(u%EF;ZX^VdMNqx332jaysMI41ym)y=D-m^bsd}lRAH|JRx`sJ
zfKi5TN@V=b@T7#|B*RmHZxy0gojvN&Qf-QSjQV^)teqHTh|fig@`^mmPzrqjJX#08
zV|rQ&%bQttvYH-jt;uo4sRHdddcXBneT>FiXQZPMn#aj}k+Ry#7hQ1rb%80R;CAT)
z6D?}Pq9CbGvQSrB)_oi~4ioI+N@Dj#!lFhHbz72|uD0b?DE}m_<l`IMt_k#4L87%m
zphI%bb?wt<jX6PM(1OX1OtMgOG|Q)w(EjM1VRsao<m3~-@JRaOeBxSSQQ1i@DojV?
zcBe?K7D@F>af`Sjkrtiku0_eSJ%ei7v(sI5XeQNd&5(mT*lw45g-*9m3yZ(J#sjrY
zyw2j||7j+&c{n8mHedYYc8^;u>pv{|0GlUT!eZR%CA!EtoKx!q6aB@wbP?C2u(0>y
zI?T@GR1Z<6xB>AecNbqwa(9ozgk(lNeX%XW4`^9ZXw}?KWv73(l`nI55!C7+Q3UDW
z=YKtz&$1FT;ze@Gu~OqV*l~((f2`nb#Hl;t9S6Sa!1pAy3MjQ>T~5hFQmYhRAvJjF
z+>uKsI%@S&n%dc_pQTvmy!i$3zkR3SsqUN)098U<Wj6fKfgedI6Q=Jd(o3jvN7<yb
zOW+$&4U%b>r{9%0JRjCtLUqNNWOZdsSr|X;IV$MdAN&-N>TdkZfjn(h(dW=!_DW&$
ze@*IcyfplG*AYECEY$`{VMP+Vz_)@GrbRn5>Eg}~KYV<961%_?vRY_;cU8((yHV%6
zbJHSBWh?&Z-l9inZBIZCQ%_HB@iT6AIG0Fa9dKJX@2@?#XK#lY_o=namHZ%;?W#&S
zWVZ{+4=|st7~Zu!u-EAyFB2TB>UitMsEAJazLGjEn||xe%uVx3XnqZa8tFHHp+Zwi
zbBt#6&h~sMA>BcKYU~Z^qcqaHIQSi$RPVnBR1N<DP!V1RRD?eQhHwz;9L?UnQ2&<J
H?XLP4NXw}6

diff --git a/src/kernel/kernel_decls.cpp b/src/kernel/kernel_decls.cpp
index c9adf1d3c..66cf7a16e 100644
--- a/src/kernel/kernel_decls.cpp
+++ b/src/kernel/kernel_decls.cpp
@@ -147,6 +147,7 @@ MK_CONSTANT(exists_and_distributer_fn, name("exists_and_distributer"));
 MK_CONSTANT(exists_and_distributel_fn, name("exists_and_distributel"));
 MK_CONSTANT(exists_or_distribute_fn, name("exists_or_distribute"));
 MK_CONSTANT(exists_imp_distribute_fn, name("exists_imp_distribute"));
+MK_CONSTANT(nonempty_range_fn, name("nonempty_range"));
 MK_CONSTANT(if_true_fn, name("if_true"));
 MK_CONSTANT(if_false_fn, name("if_false"));
 MK_CONSTANT(if_a_a_fn, name("if_a_a"));
diff --git a/src/kernel/kernel_decls.h b/src/kernel/kernel_decls.h
index d9993117c..2ee04c003 100644
--- a/src/kernel/kernel_decls.h
+++ b/src/kernel/kernel_decls.h
@@ -433,6 +433,9 @@ inline expr mk_exists_or_distribute_th(expr const & e1, expr const & e2, expr co
 expr mk_exists_imp_distribute_fn();
 bool is_exists_imp_distribute_fn(expr const & e);
 inline expr mk_exists_imp_distribute_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_exists_imp_distribute_fn(), e1, e2, e3}); }
+expr mk_nonempty_range_fn();
+bool is_nonempty_range_fn(expr const & e);
+inline expr mk_nonempty_range_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_nonempty_range_fn(), e1, e2, e3, e4}); }
 expr mk_if_true_fn();
 bool is_if_true_fn(expr const & e);
 inline expr mk_if_true_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_if_true_fn(), e1, e2, e3}); }