From 5d698a60a796342c43c427004405f705c2b6ceb4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 6 Feb 2014 08:59:05 -0800 Subject: [PATCH] refactor(builtin/sum): use new 'have' expression to formalize sum-types Signed-off-by: Leonardo de Moura --- src/builtin/obj/sum.olean | Bin 10033 -> 10205 bytes src/builtin/sum.lean | 133 ++++++++++++++++++++++---------------- 2 files changed, 79 insertions(+), 54 deletions(-) diff --git a/src/builtin/obj/sum.olean b/src/builtin/obj/sum.olean index 5e306336e4ed2a9395f92d242c4237008d179056..0cc215017c2ce3bfb3c7af3c74dd8ad2ff16ce4c 100644 GIT binary patch literal 10205 zcma)CYmD4g6~Fh+zPi&v((* zIrrRi&pr3N?qjxIP0F?9N;NV5V=Jp`^+wA)m^5lh)%eyzxs{^LLyN5=Yf0LyueB=m zTDfYLl4awXhgM5#jbzCTxoI}Zl+$Z8Z(F% zNs8vsR{T;u0gs|%z~*V2>wqp0-3D|Y=iC{l=lTe|all18+!Lmr(m6@qFanO*jBP)# z%r@xkwoP)lC3T|yKu_~%e9otlC#G10NCTTp_+UaictR{VH`&>9FL<2l40}6iQtbpC zQ(JQQLKYZ9$}}*pC{OcTkG9%xJfJrKRa5Q&s=OZy=mgM%lrRZ&N#bx9l1tW%w#=5s z8>dxmKwklHTXL>dFRi2%ZdxrJ9FkdfyKwg->O$C6YSmDFA&tR?Z^^?Md>geA^M?K{ zFih@8&w54~Q?D?RV^tV#)>o;Z4@=E?7Rv&c_(=>@Bi#f{sW$^Pk~Xz^OKM81QTOw* z@b-_Qm*{$6M*%Jj#K+NoLJBy(hj)eIT^Mu=pqX#wQT44330fBsZ02hK>PL1_+oG5? zc?hL1%##D-M)Euh6aiwM7slq1)m7kPUx4QUz5`I;1hYUn_}h6mS8A@*A2BxPmdn*< zBJy*tyx2U{SW2hj1hnc@(2xGqI!OK4&aA#vX|^i0gFarAm-D9;=M&Ou^LwMq@7~>M z@)Wr4;CC1KJzLL(K|vZrz4>YMtB>abx(BElDvo~dE>1YV_yQ;n7Z^Q>Qd02 zp=u|C&|{#U2$JaBXF!Y`LZ+7)(=)X8_bA{L*yus!{XW_hpy8idbhnV5iBoB%yjYFv z(;QANm70(%Eji)v6Vi&>y{3CTqgv~@T5z7sOc)06S)%(%m3Yg9mXd14M;^7K6Mi}9 z9wBFbRL(T%*}{KIc4Z2&hF=C&+G0JONsn{As4U50iL7Rtl3;x!Ekay8pk|Af&by=zrKcZ;1yxiRhC)Cy zJ*j%aQ(|r@+*w$~u@Yi3+l0O>{I*U1-kx2gWX|<_>VJ>~qDuiyfa;d?UT_ulj>0+U z@k7-cW=z9`9(W&Zje;}^p+S3sS7mLzPatJ(;y9RPP`#GNGSP5tas4_eNG(YI(^k87~sFxGz9vGC;%>n_dvxkX_ z4A{u5ry=q*hcX;=Xb5ZeYld)74WdpkA^wK(x~I|JpcWUXuELWX>fNBV) zQF;sl>{jv*2TvqIHPfJ~C)nm()6wGk!{WeT$HU@OKv>*3`gQSKoC@T4o*}px-Q{M% z3a8qu=*^kAW4G7sWc-6>e^cXCdv60*rVZFfhL4U|SqYvD}Qfrcft;)ld z))BOg-3zEZs!bLNb}#J(Cwr~|8(cCEvW7|E(2MP}5D61nUh6CuNdARx31Gu%#Nr%c zKgTJ#Ivp^U6SBD+z|My-XXkvUHegx^k(l)A-v=h{-%*TG9D2fyaakJeH^xehFB9>` zh?U7lPPbaBgW?RjbQCiV-%^G%)r6(RLa1EHQ%@pv(6h!9wB|!ll&Izf2u16~<_*o0BU}=DZ zh$D!7EJTton4oSCrb(o&S>g99^lNel&Bj681aME5DSnU;qg#R2z(*+_=TohGM}a-| ze^owkcFuv-+NW4PZvz^toi16I5Ui6K+kTTHp^f=7Kv?WlFJdvOQXx)4rK7mxBF8?_ ztNSVR9FJt6&1;ngK{R`i5h@*Sy!NDk^Hw_aMM9v1hUr7e@`DCU@F?rRI4cN> z7|Wi$8Q9H{1hh|e4+9z5VsY8CXK49Zpp27KTFFSYI#17ev4`rsr#k!5^8x@gio=T& zC^0=}wuGa-d}X(JJc{#^J;tPOTzmpV7wZxqEG;s{t^;_GNrPhVcb208eFCV~s3#S5 z3vu}qnit{=5(s!fwIA&+5FkIw#YY7J#IFL3!V_jEQ2OL3uu*_-0Pq#Sc4S%a^99(s zO?PDxdTtNhz;*#VAEID8+IIk)KkB>ocd#=gU@yB{fWMz}H<+;?_y+^5h_6$2o{zxx zUj2G;Oz0LDLX9F^IxH@s_C*0cD)77z?d;h->2aaQukA~fgDdq`ef3DsO|51at>+-u z0m#dct2g+hrdN0nWeJ1+9XZ@A7&aVac^0+51EXwAi}?2Og)J^()cAUa3=B1-pbxd@ z1hH@Bn zFZCKJhrN2kzlntDj>&Y8@JC3Xm_GrdoleLTjl4OcZR|TRqWvu)tx!zORm`OEeqy5A z8n-g)%neq}Cw5lzMRvv}>jzeVhCRI?N+heGi4NgJ@J=4TTb1~nX;JCyyO|p1*Z`B3 zi}EJ{jAwMd%#4iQ!%k~J{v8}=x+DqF{sUbnI1UBf^vj=xPwWTy`3$eJ%gf=l$^MI7 z@<3EeO6{+o_5*aG-$$ZUjl(5A3)^7XsnoK%k1@VB#Y@UIEq`HTF`I_eg3Q`Tn)T|# zi5xS6MNY@VuMtLjE!c|yI1stv^o=^?68h)}M-LXpvKO!Lur{6gaypyKj;C{JXp0a{ z@p-J!T!r>tUH!2be+1@eH$h#H@NSaUgiE}d;0*T- z$D`^z$74fRjrp5^+RI&+!w765#xn!E5dbOd_|u+N0o6@zAHMJncPa<9+$}-5TZ3}! zqIo+_p(pP9ITTA zhdbU6z_Ev7{Syw1u^xbiWS4ppTfRFWz&}*Ji8fbxABY+{z|yRo(|ch|$?7x-XY3h%PsI@_lF5}!HTtCKMig{eLb#2m4Jgf3*=bA8w zL%#4928tm|sec?K=-UOgb90~B40NxPPC&e_et7&3`>DCZVQGyMji*dm? zh{6*GST_+A2~1P8+@~lMfT_xtFsB*LEDijS;l9rHTR@|pELGc7#b%_nn_CE@k2|9q z<<#@&k8%pl=c2?z`?JBMnrLAq2xb+x3##x?5{Y{b-JL0R9JFKT=}xf&>2`B~D;oyu zmjE=YXkug)z2gp0F=iFA%pr|CvWk00crkh!Y;C_VEgh1lwtB7S;d;MN8IBglHvRms zg7hM$|GL6(8se+E}5ctml^x5x~fc`>I_YxUi1^OeRuL1q> zU@C-u`3tO{ZvBGlPk7N0WjlzBjOdw?6^7>#9Xdt%aD|BuV$skFx)OkC0FIy37qX{8 zP_mXVoLu!)>!)MVbKXjz=MrYel`PgA4in0cQe7qBRWM2kASX59D~H+1@H;1c%xHg# zU}&(1EeQm4dG`($;m%<>{~0FK6LYU b!M3Js-RQ-Ck?BwWS<~3r+R|?POW%J0hWS3X literal 10033 zcma)CYmD4g6~Fh+zPi(a+KLFYiy6Azb}5$Ku!0raZl%j?7s^8l_{uWd{ck(CJG0Er z!Zsp;L1@FHK#iekh%qMm$p}8c4}!!fsU~~`KVVG2FMc6Pg8D&8Jip)h|NrOC?x0Sx zch0@%+;h+SK4u&9Nwq##n@?Q&@wJ7;MziId8F-o$Hnk;LFhQU>17#C98DVGWAA1Rj@b+%6>G39<;8+x#t56 znGO^mBPM;na;Hkt%rsgmQ;B30`aFVL3t|N|5&K*ONQ65SKxT}Z$FY1>n zb1?|j4>G4izFN4%45J&A<7tfQ;qhS2;I6iWjs$@ z+DzsoHu2%)PXQ`rro2cxU0yzGj5*qFOw5uI*f4c42Iys4XFIx-sc3e?SY&FI5rbt7 z;G%x1nTS<0Z3B&hLx66iZFT@WL~t13OT}q{aai?Qo|pJ*I1Nc;i-39LULT z29(%Z+X28LiL3sy!~W4-{IpfbbWLAn$> z0b*=h0bj@h=QuJBh#D1Xo}K8c{jMvfWfg8*Eo~0TEql38cO&X7>}vISE5G2zV8gfM;eLEOwG#7& z{w*;~jsmluQO49OZ7r}W^e;6QC}0|vn)57{C8~H0CaRG>4M<0K19Xx$^+ro-N~_sO z*Ja`D9t4))dO#1N*G;9|V6iWnr_h{6Q{n;#0CMs(vi($NmX@2d8DDav z3CBzrI!}upg<(H8@oa6WRjVIKgF|Vv%5t@=)aKvj8vmwl&61=<{mj21@^3Ep29u3S ztJkQP`f>uK3SJLL6@QexJNj^gnK9mCG4}^(Hf65+vAPapCn(y}#`Fn{o-$5!;t32! zh9}YUob)VE^p4`6L!Xn1nE|hpk>KJCIaZySkIPO42a;M{hHEW3xbS1yLScTXTR4MN z%d;A6ip0!=8vwpcP(xJ0C}%pI%-7O@(wYk5S9`;K_;$rXIjUqwhV)yKCKrgM`QxCZ z>g(w{I+&`WU?eLNLrYnvf%LVk#=J&Lkvys)78K-Juy`QP5?E{+EZ_?vm|B&?Av5hk z8E%VBk+}0=ra~4kr?y1r6*OuK+U$1pHQw$p@J@g)Q`X-A3}`6CA2Q=Chv{!|z1s+`GL5Rf$~1KPDYK6jO*PGR;F1O$pu996mX1Un&v`&>l)@axoNoRW zWuW;L1^W^}HN=+zX`p=tpxdSu@fN8#*`bDEK@ru3^s|bH8Q)Yn;VCh<)Z;v?;#jem z%oX^e(EB#|J9~D9oavG`DZgq)P;ms0fJ}Fqcg_syvlbhMdpS0+q21(BmfLFOidn9H1L>)3s((?&gkfOd33?*ispc-!wqLuelsi`--aDvxjH zl=}hglSa!6L!p!w+nx3 zdyl1}K|S$eS~RHDRpW^kkR4M#1eXEn#(FP6x&LS7_h?)B6`VhxA;cvaJ&ad9PrM8K zN6>7{jpnqv%Ah-o=1J=G0YIHjU$ICjC-&((mehJ%NtIbzuvBM_IPi)DK#lhUxd3Uc z#2{07lL?^HO#l@L(dPDmUP~Qi%~$dl0JCC2l-5IxZa32;(q|QS>2?IX=B`Pmg$|h8 zCmQ&Dy8)_n;OwZfs$kYJ6FkD1q1w__nAyOT28-%r~xj8qy7;`ZxLMm*4e91Cd>M5|*=c~~KPlH}5~6*3H7 zkHKiREnyWY#rHV#8q<831%g6Xz>D|Nt0N8=JiT@rhAA7a&;C0W?DWHFEmR!U(ly+1 zU1kQ?J-r$awn#Ke6kQWN7q~jBPE8?cuTJ@`8!y%TjxD;e$YYBP~gHmA*#nnxQQYLA=!2r(k{-U+{kKtwN%}CLF#~_NAXSAjH zi$1di`Q#r$^GycMswC=sIsiF0*)>T540m2dqx)Gjk68c^+K0gp59&3$GsyRI4w}zN z(_HbGVX6h!{Gcppu=dMlO_!UfawmL1;PC?6u)@S){Y!& zv>FS?J8n^R$GGH`AShq?;X(pQu2Fj5#-K>to4)1RHGomV{PVqF;(rf934$4Xr{UBu zP(-NV^au$US&tfc0;K1Pa^RB(3Km0s(vBa}db~U%V9G6W@Z(hXFMRzQO$kl(!d5^8 zJO3tHx#sJ8vhE4vuilXpywg^6z8D`Iw;P!G#2xF5*j)#j!nQNX!N#61=#25!AF6XFpHky1YLt{kk48dlnqdfIvr%D@Lr=) zH%=}LD3dg71XuRCCrA7^U*4%_Kmjc)gu(`Kxa1Mv!cjv6$pw5RU%*#lF@sR7L(>OR zqPSLo9m0S#TIk3n4CKm&0p$X!OQlJtcB7A}%&Rc4`WU4q=PvI-iUoom@ZJEpBliJO zsm2WLqa>BaPjWs|G7OL&?oraPqad(D0197e{3I=}%qe{rP&-y9Qd;9oGAePNt+d7T z1z!i>gq?tr3<_7EJBCIQ2Nz?xo1}%bKM%HmJ4qNZv38rzYILGzL1j+RlQ?a_`H&%u z=Gv>LibGbLr}g;`WH^V0&rtpkj4S8jhLFw$w3kFUea1^mDU&OHtPJPAg0MmIr?e*a zL^kNku|#+;OLr8rGij&DklN;RH8v`A;$ASkfeX-+xQ~V#(b$b7Orbww9-A=hfV1OH zz?vIueg&Ao07LCm%&mZK0Y)Da&!IoT=qVGVnbOA^SYbUHlE5`xVrEy^h4cv_%7OVJni80ZmQ_#zm0HH{vQB2F`LRhW@zC#^;687IDGg)O9K;xR0hDP(+rlDrNu!sOZ4ChGN| zVhvXLCZx~pGHl_}2Z6URXPteRHql%H`jDA)3jGn&#Mq6RO^n^cLcS(zPGIa&V4|$K zqZb2Z`3rZLq3=XrQ>7aqQbl(R=8L8Z5c$86d<(s{pMhqV<*lqy?|7)bSwzNP;*!g%TB5Bk|}n)d%B{x5wR^?GI;r4lcImEOUAV&G2&4BsWe&jEgq;7b6% z-uOFatf%b+~^Z>$ecgXzFY}72&7n+fjYz zf)Qm!G8&RbMymdh&FL^&lq`So~*}{>+|toj*{Yoxs1z F{RbaYD$4)> diff --git a/src/builtin/sum.lean b/src/builtin/sum.lean index 875aff5d17..d14b25025c 100644 --- a/src/builtin/sum.lean +++ b/src/builtin/sum.lean @@ -23,22 +23,26 @@ theorem pairext_proj {A B : (Type U)} {p : A # B} {a : A} {b : B} (H1 : proj1 theorem inl_pred {A : (Type U)} (a : A) (B : (Type U)) : sum_pred A B (pair (some a) none) := not_intro - (λ N : (some a = none) = (none = (optional::@none B)), - let eq : some a = none := (symm N) ◂ (refl (optional::@none B)) - in absurd eq (distinct a)) + (assume N : (some a = none) = (none = (optional::@none B)), + have eq : some a = none, + from (symm N) ◂ (refl (optional::@none B)), + show false, + from absurd eq (distinct a)) theorem inr_pred (A : (Type U)) {B : (Type U)} (b : B) : sum_pred A B (pair none (some b)) := not_intro - (λ N : (none = (optional::@none A)) = (some b = none), - let eq : some b = none := N ◂ (refl (optional::@none A)) - in absurd eq (distinct b)) + (assume N : (none = (optional::@none A)) = (some b = none), + have eq : some b = none, + from N ◂ (refl (optional::@none A)), + show false, + from absurd eq (distinct b)) theorem inhabl {A : (Type U)} (H : inhabited A) (B : (Type U)) : inhabited (sum A B) -:= inhabited_elim H (λ w : A, +:= inhabited_elim H (take w : A, subtype_inhabited (exists_intro (pair (some w) none) (inl_pred w B))) theorem inhabr (A : (Type U)) {B : (Type U)} (H : inhabited B) : inhabited (sum A B) -:= inhabited_elim H (λ w : B, +:= inhabited_elim H (take w : B, subtype_inhabited (exists_intro (pair none (some w)) (inr_pred A w))) definition inl {A : (Type U)} (a : A) (B : (Type U)) : sum A B @@ -49,71 +53,92 @@ definition inr (A : (Type U)) {B : (Type U)} (b : B) : sum A B theorem inl_inj {A B : (Type U)} {a1 a2 : A} : inl a1 B = inl a2 B → a1 = a2 := assume Heq : inl a1 B = inl a2 B, - let eq1 : inl a1 B = abst (pair (some a1) none) (inhabl (inhabited_intro a1) B) := refl (inl a1 B), - eq2 : inl a2 B = abst (pair (some a2) none) (inhabl (inhabited_intro a1) B) - := subst (refl (inl a2 B)) (proof_irrel (inhabl (inhabited_intro a2) B) (inhabl (inhabited_intro a1) B)), - rep_eq : (pair (some a1) none) = (pair (some a2) none) - := abst_inj (inhabl (inhabited_intro a1) B) (inl_pred a1 B) (inl_pred a2 B) (trans (trans (symm eq1) Heq) eq2) - in optional::injectivity + have eq1 : inl a1 B = abst (pair (some a1) none) (inhabl (inhabited_intro a1) B), + from refl (inl a1 B), + have eq2 : inl a2 B = abst (pair (some a2) none) (inhabl (inhabited_intro a1) B), + from subst (refl (inl a2 B)) (proof_irrel (inhabl (inhabited_intro a2) B) (inhabl (inhabited_intro a1) B)), + have rep_eq : (pair (some a1) none) = (pair (some a2) none), + from abst_inj (inhabl (inhabited_intro a1) B) (inl_pred a1 B) (inl_pred a2 B) (trans (trans (symm eq1) Heq) eq2), + show a1 = a2, + from optional::injectivity (calc some a1 = proj1 (pair (some a1) (optional::@none B)) : refl (some a1) ... = proj1 (pair (some a2) (optional::@none B)) : pair_inj1 rep_eq ... = some a2 : refl (some a2)) theorem inr_inj {A B : (Type U)} {b1 b2 : B} : inr A b1 = inr A b2 → b1 = b2 := assume Heq : inr A b1 = inr A b2, - let eq1 : inr A b1 = abst (pair none (some b1)) (inhabr A (inhabited_intro b1)) := refl (inr A b1), - eq2 : inr A b2 = abst (pair none (some b2)) (inhabr A (inhabited_intro b1)) - := subst (refl (inr A b2)) (proof_irrel (inhabr A (inhabited_intro b2)) (inhabr A (inhabited_intro b1))), - rep_eq : (pair none (some b1)) = (pair none (some b2)) - := abst_inj (inhabr A (inhabited_intro b1)) (inr_pred A b1) (inr_pred A b2) (trans (trans (symm eq1) Heq) eq2) - in optional::injectivity + have eq1 : inr A b1 = abst (pair none (some b1)) (inhabr A (inhabited_intro b1)), + from refl (inr A b1), + have eq2 : inr A b2 = abst (pair none (some b2)) (inhabr A (inhabited_intro b1)), + from subst (refl (inr A b2)) (proof_irrel (inhabr A (inhabited_intro b2)) (inhabr A (inhabited_intro b1))), + have rep_eq : (pair none (some b1)) = (pair none (some b2)), + from abst_inj (inhabr A (inhabited_intro b1)) (inr_pred A b1) (inr_pred A b2) (trans (trans (symm eq1) Heq) eq2), + show b1 = b2, + from optional::injectivity (calc some b1 = proj2 (pair (optional::@none A) (some b1)) : refl (some b1) ... = proj2 (pair (optional::@none A) (some b2)) : pair_inj2 rep_eq ... = some b2 : refl (some b2)) theorem distinct {A B : (Type U)} (a : A) (b : B) : inl a B ≠ inr A b := assume N : inl a B = inr A b, - let eq1 : inl a B = abst (pair (some a) none) (inhabl (inhabited_intro a) B) := refl (inl a B), - eq2 : inr A b = abst (pair none (some b)) (inhabl (inhabited_intro a) B) - := subst (refl (inr A b)) (proof_irrel (inhabr A (inhabited_intro b)) (inhabl (inhabited_intro a) B)), - rep_eq : (pair (some a) none) = (pair none (some b)) - := abst_inj (inhabl (inhabited_intro a) B) (inl_pred a B) (inr_pred A b) (trans (trans (symm eq1) N) eq2) - in absurd (pair_inj1 rep_eq) (optional::distinct a) + have eq1 : inl a B = abst (pair (some a) none) (inhabl (inhabited_intro a) B), + from refl (inl a B), + have eq2 : inr A b = abst (pair none (some b)) (inhabl (inhabited_intro a) B), + from subst (refl (inr A b)) (proof_irrel (inhabr A (inhabited_intro b)) (inhabl (inhabited_intro a) B)), + have rep_eq : (pair (some a) none) = (pair none (some b)), + from abst_inj (inhabl (inhabited_intro a) B) (inl_pred a B) (inr_pred A b) (trans (trans (symm eq1) N) eq2), + show false, + from absurd (pair_inj1 rep_eq) (optional::distinct a) theorem dichotomy {A B : (Type U)} (n : sum A B) : (∃ a, n = inl a B) ∨ (∃ b, n = inr A b) := let pred : (proj1 (rep n) = none) ≠ (proj2 (rep n) = none) := P_rep n in or_elim (em (proj1 (rep n) = none)) - (λ Heq, let neq_none : ¬ proj2 (rep n) = (optional::@none B) := (symm (not_iff_elim (ne_symm pred))) ◂ Heq, - ex_some : ∃ b, proj2 (rep n) = some b := resolve1 (optional::dichotomy (proj2 (rep n))) neq_none - in obtain (b : B) (Hb : proj2 (rep n) = some b), from ex_some, - or_intror (∃ a, n = inl a B) - (let rep_eq : rep n = pair none (some b) - := pairext_proj Heq Hb, - rep_inr : rep (inr A b) = pair none (some b) - := rep_abst (inhabr A (inhabited_intro b)) (pair none (some b)) (inr_pred A b), - n_eq_inr : n = inr A b - := rep_inj (trans rep_eq (symm rep_inr)) - in exists_intro b n_eq_inr)) - (λ Hne, let eq_none : proj2 (rep n) = (optional::@none B) := (not_iff_elim pred) ◂ Hne, - ex_some : ∃ a, proj1 (rep n) = some a := resolve1 (optional::dichotomy (proj1 (rep n))) Hne - in obtain (a : A) (Ha : proj1 (rep n) = some a), from ex_some, - or_introl (let rep_eq : rep n = pair (some a) none - := pairext_proj Ha eq_none, - rep_inl : rep (inl a B) = pair (some a) none - := rep_abst (inhabl (inhabited_intro a) B) (pair (some a) none) (inl_pred a B), - n_eq_inl : n = inl a B - := rep_inj (trans rep_eq (symm rep_inl)) - in exists_intro a n_eq_inl) - (∃ b, n = inr A b)) + (assume Heq : proj1 (rep n) = none, + have neq_none : ¬ proj2 (rep n) = (optional::@none B), + from (symm (not_iff_elim (ne_symm pred))) ◂ Heq, + have ex_some : ∃ b, proj2 (rep n) = some b, + from resolve1 (optional::dichotomy (proj2 (rep n))) neq_none, + obtain (b : B) (Hb : proj2 (rep n) = some b), + from ex_some, + show (∃ a, n = inl a B) ∨ (∃ b, n = inr A b), + from or_intror (∃ a, n = inl a B) + (have rep_eq : rep n = pair none (some b), + from pairext_proj Heq Hb, + have rep_inr : rep (inr A b) = pair none (some b), + from rep_abst (inhabr A (inhabited_intro b)) (pair none (some b)) (inr_pred A b), + have n_eq_inr : n = inr A b, + from rep_inj (trans rep_eq (symm rep_inr)), + show (∃ b, n = inr A b), + from exists_intro b n_eq_inr)) + (assume Hne : ¬ proj1 (rep n) = none, + have eq_none : proj2 (rep n) = (optional::@none B), + from (not_iff_elim pred) ◂ Hne, + have ex_some : ∃ a, proj1 (rep n) = some a, + from resolve1 (optional::dichotomy (proj1 (rep n))) Hne, + obtain (a : A) (Ha : proj1 (rep n) = some a), + from ex_some, + show (∃ a, n = inl a B) ∨ (∃ b, n = inr A b), + from or_introl + (have rep_eq : rep n = pair (some a) none, + from pairext_proj Ha eq_none, + have rep_inl : rep (inl a B) = pair (some a) none, + from rep_abst (inhabl (inhabited_intro a) B) (pair (some a) none) (inl_pred a B), + have n_eq_inl : n = inl a B, + from rep_inj (trans rep_eq (symm rep_inl)), + show ∃ a, n = inl a B, + from exists_intro a n_eq_inl) + (∃ b, n = inr A b)) theorem induction {A B : (Type U)} {P : sum A B → Bool} (H1 : ∀ a, P (inl a B)) (H2 : ∀ b, P (inr A b)) : ∀ n, P n := take n, or_elim (sum::dichotomy n) - (λ Hex : ∃ a, n = inl a B, - obtain (a : A) (Ha : n = inl a B), from Hex, - subst (H1 a) (symm Ha)) - (λ Hex : ∃ b, n = inr A b, - obtain (b : B) (Hb : n = inr A b), from Hex, - subst (H2 b) (symm Hb)) + (assume Hex : ∃ a, n = inl a B, + obtain (a : A) (Ha : n = inl a B), from Hex, + show P n, + from subst (H1 a) (symm Ha)) + (assume Hex : ∃ b, n = inr A b, + obtain (b : B) (Hb : n = inr A b), from Hex, + show P n, + from subst (H2 b) (symm Hb)) set_opaque inl true set_opaque inr true