From daf7075ce4f73e5ea6b71edda22799695f2a73f2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 6 Feb 2014 09:15:12 -0800 Subject: [PATCH] refactor(builtin/sum): use new 'have' expression to formalize optional-types Signed-off-by: Leonardo de Moura --- src/builtin/obj/optional.olean | Bin 6683 -> 6841 bytes src/builtin/optional.lean | 87 +++++++++++++++++++++------------ 2 files changed, 57 insertions(+), 30 deletions(-) diff --git a/src/builtin/obj/optional.olean b/src/builtin/obj/optional.olean index ab2fa979ca4e1510a66bf2f663ce9aa4d78d088d..befd296dcff48b8c1b01764758eed4ed87a1f82d 100644 GIT binary patch literal 6841 zcmaJ`TaO$^6|U-8GUKczL*hst))Jesy*m>kffFtX7YQQmvXQ`XvN2HovNjzoca_}Swa4`XOHMScP&MA&U%Efbo63OC986N-WH4h&Xsi*cOgIpy=e%#+q$Km+;rLA*OK1Ar5{W3@Q$d+j8_kWG>MA zScTRF)P!dU=plfgT&g@m;kmB{J_*>$zDTT^8KbnZp*|yu7gOl3DaI1kRR= ^)b< z=h?Q{Vw?_KNGUmvpW+dMivSty^=WXW^{%vyXpjsisS}&( z!=T<}B80b%4YpaK49nmn1SFJW5{b)kb|FjT3^^U-K896<8-PPuzL}g2AuNf&m8_Kf zG8&<`1JPKrxQFnG##|N4E~droLP(DRr-9)v8uIg;dj%UoX;NfttSTp(+*qWSN(Y+- z;Xr4dhdv9?EH#LAZ*q1bxr?821>`9900)D0 zzkN?FY$R--26&Wq0>_4w2MN+$})~5bfsyX@E`DiVkY!(;2^w_3wY7P{! zZ4`(Z(Yedvr`<+$uE@`iS=HR(2xLC({oM_R8Q`inP)I?q2--MsuFBGv1g&9f-tWsT zm*wZmeOymI4EBC-w(6-Fi-Z!Na_JiiV_d@^HSJVQ%|6zyVz~ByT+Dc(w#P}7Y`M6? z+Vdk2xE_4f4!$B5@n7Y51*jT-M0&ECTi(bI(QGSJ?`OfHG$D_1SfL4jj2uRs^WUn_FSkIPA;4SDKPhQhXKlW&F9QvkIlJ_7J} z=maEn_-o6gD$8-Ytk<$a+c^&t0yZwk!WSzH8E3-mtbSG{cO*bK7aLiF+FM>Co4R2hi22CkP{?@%wPOYDUsww#7A<2K&oQMjrrAqY98D2-QF%x2Div z>X9k#ldEky7TtmgZcy0Zo@St|?$XFXthtD#sjDFTHW&xfFa~esGz21k?+5l0Q&@rX zohs@HOx0&GKy~T{AT9F@gZGj6C+n4Q_73?cPF#d>N0T_w9?>?~ zxH)4O+Lfk1z~$}z=U7Y2YDTs;qPUW_!D=IM@Wed?CMeuTl1a?LdQ z*mQf~%K!r>=y1R%kA#~%VnT>avi$roEsK25i=$0IAX}z!+U~*_bdhL=xbnFs&njJ)iuYPq=vXFmm$*Ms5vnxSW|q6Cksl**u6fv z+id}T1Ql*0sBP5}7AOP-?gew&qd1`Q0SayXUT%V7a#d_mtmoKj% zAl)myD*hUC9>XREd1UL}X>_t!*|qCjK#^+FvMy;o|20l%gSkl1%RF24=;)i`L3tqR zO+;U)mDTnLOUwI!s{EMrFsL#IIfu;@={n}W#Q-AqG$6ze6Vg6DFHhl7oX66xyZ#&q zm&5rPCU5G6(FYdms(k{G^vR@yM{yuU*=e~hkfMsJeTur!@ETIIP}g@cL|<7B9*L_* zp?wPMzQgkypbA_YbN(df`?!Oh|()d?Qc;Dp%u^v`j zQn@qeOE$GPq_V}?L0v2VT(Jmv%YdOe1BrlgoaEa1**qAohUkq&+AI5@SY9$s2F(3n zz{3{+O=VyvS&ah;h_QZESj0|fC#l%oKz_{E|4#L81Z8~4% z<42zeG@3gj4EZZeg&r>dOGNj=n;ZlQ&i0%e(S}dMfzAc@ng=fvBY`yAFMSFfuwJ zGE~|ZaLm0?LqNe_MsZmgIHyQeKiCoLYFqWvzUiiRDl30#NC{aNXyD*_7L-qkRQYGw zD6lZN=80O0Dby(ISBkUVNtv4`#lSs71F99A^ZE(Gk zGPU6=n>EpfL$3>psbvUv-UW?!u;X8rl-k8g(C95-9OWDlW8Wg$B0&oC0znl6T|Nr-*`J&vSD=AVoNr{cd+kc5<0vr?@#6XPm$Ljqo;AgY)Mad zQg3}4<(kaz6EtnjHTv}q^3PW=wuhG$?vXvdGLV`phSjMK z3l7VoG6UiO+cXSYEbSiuzKm6tt=TIA*qhje&1{B2CG}51Ip9+NA5JvHf#!852>4ov z1_XTQ{514?LDtu>jdsp{1W0A|t^TiMMOytwMv0lj?je4Ttj+lfuFd@y%i5BD#o$8t z4~*SYeK_#DYlSlN!T1c=ZzTPGJRX}!z5plFVOjq#5&wRtgboj9-md+($)0!qE%2%@ RUbonVK-OgQWlf literal 6683 zcmZ`;-EUmQ6`#3l*bQ!#wlq?fCcYE+@BPwh*Cs;c6leLzUi@&~k!RsVzb{C;QV&g|M*DdTfy z&YbT#bLOTTWNERU4>IF^Hs2hUqsly$jf!kw9Cj+LJUHH7tu72R)6dpTQVy%UEYd-5 zILi8_m3-aYWKHs@KtuVLngm=M$v4V!p!}02{#qgg8vq+e8%a4bvgJIt*dvXkC@W)* zU{$vWNp?OTSL5Dxk#B7~g>`L07pj4Mq6_3F)JTR^;Yj*ft_nkM3-QJg>O$DqYQxOb z=9zK1nFSk30`u^*M=^dDL$fLR6F4TyZi#3?=mHwtr0`EG1;)={utHmodU;We;DXvr zti>#4Auami5^}j2i|u0=4?+S}r<6A4Y%95dzorc}MM42}@ateub?Drd;|C@)f!_@^ zSrR~d1FCiMiQ^4@LyJndCaQ~fSTOKNovl$ zZSln@TX!j?>^R=aEd=KPegT6$xjDpN^C=(qCPWV`3rp{%T)8ckvq}xE#z;J+$ypOmyun~+VN9M)}l|+{ti{qu*!Dm4^ z@Hx#*cL6l>4N~2au8!sG;-^vpIgX2fLrCrf67k153;gRNM#p{^JM|3R15oqmUO<+1 z^?V?xQo>DoEe*kDd$(AxC?K$Xq(I!*u0ank!#v-V(6 zTQU{|kT;RtUXlA{I!evFcrsh7Bvq;ldw4_KvOq?1YUFSOJcyyBCd_pnAi7~ItTURr z!lf@`lUni>K$=lsQZ7=DW3XmIzgbxMyb7&cHl zElfb4os|mO8)d_>R7gx53<{7`qd_j6U?Zy)xpab*J=fc}N7*W;>M-A1xj7H3DSp2pCW1Z+R=^Qs$| z@gS+8wPd}D7)x&M`1JackTh(RV12nr^J1;qBfBVq5$%V3Qk%3W;LJ+eaO#A@7$3wS zW%E>IaUXM+FkIdhPRuf0j*=5)F|(Ff(_XIEnNH6FCCycibhqX*qjU!A#I+W@9z3Pa zt=E_6nm2%Rg&uyvdze#8HF4xoW#c^xlDKj_oercWK?B5JD{*xL_nKx5j<`E*3|pIK ze=E#>8=#icQvm;nCPLDmzqTNCMek+j{jG|{wpZTu19S+hWrx0!B#e)jdI@uX_SQTk zNR%C}4DPChDK@!==MMmB!X=KZkUH@_QZa>i)o7}GksCr-O5kit&XJy~GI#sHFL~Wy zNTeI?Qm^0SZA7zMWJBeoiJSqa{a+&;Kv&|vPZ+6+-vfoh1J0H`tS0n!U$1>k!)zsG$k#?16>^KVR^gD;2UUaH-q>rnrM zCC&Fo2nMCD0e^SOCm}=si{&PlnHo%*bMrI=MNRUWy#7TH!+$U^BbAF!qaVt2Q@Uk$?0WSOv5{GHt5MpMYdNtN=)TPFay*exDIeue6YSUp#!xnXW2B5m@$AC`HCOnLK;cC||uNo}fAx$9u8gmxI1_pUF z>)OL;5iv8dD!!KYnO1XpP5q%>LSoo&V#h@czrdi;q6vJI@g`Lwo_zKoT8AR*e}=7E zz;^&@CpbsY`@r4Fm}9M@q<4YJm9fkNWFMN9=j^ao^rYo>%`ONo!q0nZ`a3PsCKPBgOrvBJ$R<>xuoc8 z&t-qU=SfnR<#jS>^h9t}LZw(j6MY537Mla7Vph5GBVagJpm`3gctq`UfS#vKAq9NM z?V%u(7X{thLFnugWW?RHdIca{Y~LieS3Pdpvk7X1_I$2T)Q;i>WDf-eC`Uz{4YA{F z6g%K5?QMA0ZeZ96X6*pKOd|T?HGqfJnnYl7rZs$=sxQK(w}m7=UR=2f9>2kg8gVO? zo&$b`LeMMND=I_{gs6R-4FbPFdwE42&cMBPt6Vs+tt?>Q@h@x)~(5hdO1;JmD8NpwJ z;4cK<1o+pcdpllZJeEV^@L)r%eY|#<>2fD8Dfe}tc7;J2yY87shd3EX8-+C(?wwJ$ zD)w&_%;E2{>`G)!*_A=QO2ch>wv zO18N}{ZY{8tq^@CGL7$m4-d>ggKBSqBUe5KRLA-aL8OQN&M-AISlG`Gei6>cVubr| zg3**d_Bj#$i(nGfj+|dMYm%u?vUtv!m9*dQjYcMsZ>;I|po;&~!9R1Up`*i|-$ws2 ZvFkZ}9lH91&vn+L$K+DcKY{-c`aeHGeH;J) diff --git a/src/builtin/optional.lean b/src/builtin/optional.lean index ba1a299274..15e9f8bc22 100644 --- a/src/builtin/optional.lean +++ b/src/builtin/optional.lean @@ -32,14 +32,18 @@ definition some {A : (Type U)} (a : A) : optional A definition is_some {A : (Type U)} (n : optional A) := ∃ x : A, some x = n theorem injectivity {A : (Type U)} {a a' : A} : some a = some a' → a = a' -:= assume Heq, - let eq_reps : (λ x, x = a) = (λ x, x = a') := abst_inj (inhab A) (some_pred a) (some_pred a') Heq - in (congr1 a eq_reps) ◂ (refl a) +:= assume Heq : some a = some a', + have eq_reps : (λ x, x = a) = (λ x, x = a'), + from abst_inj (inhab A) (some_pred a) (some_pred a') Heq, + show a = a', + from (congr1 a eq_reps) ◂ (refl a) theorem distinct {A : (Type U)} (a : A) : some a ≠ none := assume N : some a = none, - let eq_reps : (λ x, x = a) = (λ x, false) := abst_inj (inhab A) (some_pred a) (none_pred A) N - in (congr1 a eq_reps) ◂ (refl a) + have eq_reps : (λ x, x = a) = (λ x, false), + from abst_inj (inhab A) (some_pred a) (none_pred A) N, + show false, + from (congr1 a eq_reps) ◂ (refl a) definition value {A : (Type U)} (n : optional A) (H : is_some n) : A := ε (inhabited_ex_intro H) (λ x, some x = n) @@ -49,44 +53,67 @@ theorem is_some_some {A : (Type U)} (a : A) : is_some (some a) theorem not_is_some_none {A : (Type U)} : ¬ is_some (@none A) := assume N : is_some (@none A), - obtain (w : A) (Hw : some w = @none A), from N, - absurd Hw (distinct w) + obtain (w : A) (Hw : some w = @none A), + from N, + show false, + from absurd Hw (distinct w) theorem value_some {A : (Type U)} (a : A) (H : is_some (some a)) : value (some a) H = a -:= let eq1 : some (value (some a) H) = some a := eps_ax (inhabited_ex_intro H) a (refl (some a)) - in injectivity eq1 +:= have eq1 : some (value (some a) H) = some a, + from eps_ax (inhabited_ex_intro H) a (refl (some a)), + show value (some a) H = a, + from injectivity eq1 theorem false_pred {A : (Type U)} {p : A → Bool} (H : ∀ x, ¬ p x) : p = λ x, false := funext (λ x, eqf_intro (H x)) theorem singleton_pred {A : (Type U)} {p : A → Bool} {w : A} (H : p w ∧ ∀ y, y ≠ w → ¬ p y) : p = (λ x, x = w) -:= funext (λ x, - iff_intro - (λ Hpx : p x, refute (λ N : x ≠ w, absurd Hpx (and_elimr H x N))) - (λ Heq : x = w, subst (and_eliml H) (symm Heq))) +:= funext (take x, iff_intro + (assume Hpx : p x, + show x = w, + from refute (assume N : x ≠ w, + show false, + from absurd Hpx (and_elimr H x N))) + (assume Heq : x = w, + show p x, + from subst (and_eliml H) (symm Heq))) theorem dichotomy {A : (Type U)} (n : optional A) : n = none ∨ ∃ a, n = some a -:= let pred : optional_pred A (rep n) := P_rep n - in or_elim pred - (λ Hl, let rep_n_eq : rep n = λ x, false := false_pred Hl, - rep_none_eq : rep none = λ x, false := rep_abst (inhab A) (λ x, false) (none_pred A) - in or_introl (rep_inj (trans rep_n_eq (symm rep_none_eq))) - (∃ a, n = some a)) - (λ Hr : ∃ x, rep n x ∧ ∀ y, y ≠ x → ¬ rep n y, - obtain (w : A) (Hw : rep n w ∧ ∀ y, y ≠ w → ¬ rep n y), from Hr, - let rep_n_eq : rep n = λ x, x = w := singleton_pred Hw, - rep_some_eq : rep (some w) = λ x, x = w := rep_abst (inhab A) (λ x, x = w) (some_pred w), - n_eq_some : n = some w := rep_inj (trans rep_n_eq (symm rep_some_eq)) - in or_intror (n = none) +:= have pred : optional_pred A (rep n), + from P_rep n, + show n = none ∨ ∃ a, n = some a, + from or_elim pred + (assume Hl : ∀ x : A, ¬ rep n x, + have rep_n_eq : rep n = λ x, false, + from false_pred Hl, + have rep_none_eq : rep none = λ x, false, + from rep_abst (inhab A) (λ x, false) (none_pred A), + show n = none ∨ ∃ a, n = some a, + from or_introl (rep_inj (trans rep_n_eq (symm rep_none_eq))) + (∃ a, n = some a)) + (assume Hr : ∃ x, rep n x ∧ ∀ y, y ≠ x → ¬ rep n y, + obtain (w : A) (Hw : rep n w ∧ ∀ y, y ≠ w → ¬ rep n y), + from Hr, + have rep_n_eq : rep n = λ x, x = w, + from singleton_pred Hw, + have rep_some_eq : rep (some w) = λ x, x = w, + from rep_abst (inhab A) (λ x, x = w) (some_pred w), + have n_eq_some : n = some w, + from rep_inj (trans rep_n_eq (symm rep_some_eq)), + show n = none ∨ ∃ a, n = some a, + from or_intror (n = none) (exists_intro w n_eq_some)) theorem induction {A : (Type U)} {P : optional A → Bool} (H1 : P none) (H2 : ∀ x, P (some x)) : ∀ n, P n := take n, or_elim (dichotomy n) - (λ Heq : n = none, - subst H1 (symm Heq)) - (λ Hex : ∃ a, n = some a, - obtain (w : A) (Hw : n = some w), from Hex, - subst (H2 w) (symm Hw)) + (assume Heq : n = none, + show P n, + from subst H1 (symm Heq)) + (assume Hex : ∃ a, n = some a, + obtain (w : A) (Hw : n = some w), + from Hex, + show P n, + from subst (H2 w) (symm Hw)) set_opaque some true set_opaque none true