From f28c56b1883fdbc44ee6d2801bde340f4c084332 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 8 Feb 2014 19:36:17 -0800 Subject: [PATCH] feat(builtin/num): add auxiliary definitions and theorems for proving the primitive recursion theorem Signed-off-by: Leonardo de Moura --- src/builtin/kernel.lean | 6 +- src/builtin/num.lean | 234 +++++++++++++++++++++++++++++++++-- src/builtin/obj/kernel.olean | Bin 51435 -> 51581 bytes src/builtin/obj/num.olean | Bin 6452 -> 15973 bytes src/kernel/kernel_decls.cpp | 1 + src/kernel/kernel_decls.h | 3 + 6 files changed, 232 insertions(+), 12 deletions(-) diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean index 3434edbced..5983dcec61 100644 --- a/src/builtin/kernel.lean +++ b/src/builtin/kernel.lean @@ -800,9 +800,12 @@ theorem eps_singleton {A : (Type U)} (H : inhabited A) (a : A) : ε H (λ x, x = in eps_ax H a Ha -- A function space (∀ x : A, B x) is inhabited if forall a : A, we have inhabited (B a) -theorem inhabited_fun {A : (Type U)} {B : A → (Type U)} (Hn : ∀ a, inhabited (B a)) : inhabited (∀ x, B x) +theorem inhabited_dfun {A : (Type U)} {B : A → (Type U)} (Hn : ∀ a, inhabited (B a)) : inhabited (∀ x, B x) := inhabited_intro (λ x, ε (Hn x) (λ y, true)) +theorem inhabited_fun (A : (Type U)) {B : (Type U)} (H : inhabited B) : inhabited (A → B) +:= inhabited_intro (λ x, ε H (λ y, true)) + theorem exists_to_eps {A : (Type U)} {P : A → Bool} (H : ∃ x, P x) : P (ε (inhabited_ex_intro H) P) := obtain (w : A) (Hw : P w), from H, eps_ax (inhabited_ex_intro H) w Hw @@ -1033,4 +1036,3 @@ theorem hproof_irrel {a b : Bool} (H1 : a) (H2 : b) : H1 == H2 H1_eq_H1b : H1 == H1b := hsymm (cast_heq Hab H1), H1b_eq_H2 : H1b == H2 := to_heq (proof_irrel H1b H2) in htrans H1_eq_H1b H1b_eq_H2 - diff --git a/src/builtin/num.lean b/src/builtin/num.lean index 8f938cb312..7f689bdb1b 100644 --- a/src/builtin/num.lean +++ b/src/builtin/num.lean @@ -1,5 +1,9 @@ +-- Copyright (c) 2014 Microsoft Corporation. All rights reserved. +-- Released under Apache 2.0 license as described in the file LICENSE. +-- Author: Leonardo de Moura import macros import subtype +import tactic using subtype namespace num @@ -54,7 +58,7 @@ theorem succ_pred (n : num) : N (S (rep n)) show N (S (rep n)), from N_S N_n -theorem succ_inj (a b : num) : succ a = succ b → a = b +theorem succ_inj {a b : num} : succ a = succ b → a = b := assume Heq1 : succ a = succ b, have Heq2 : S (rep a) = S (rep b), from abst_inj inhab (succ_pred a) (succ_pred b) Heq1, @@ -97,6 +101,20 @@ theorem induction {P : num → Bool} (H1 : P zero) (H2 : ∀ n, P n → P (succ theorem induction_on {P : num → Bool} (a : num) (H1 : P zero) (H2 : ∀ n, P n → P (succ n)) : P a := induction H1 H2 a +theorem sn_ne_n (n : num) : succ n ≠ n +:= induction_on n + (succ_nz zero) + (λ (n : num) (iH : succ n ≠ n), + not_intro + (assume R : succ (succ n) = succ n, + absurd (succ_inj R) iH)) + +set_opaque num true +set_opaque Z true +set_opaque S true +set_opaque zero true +set_opaque succ true + definition lt (m n : num) := ∃ P, (∀ i, P (succ i) → P i) ∧ P m ∧ ¬ P n infix 50 < : lt @@ -138,9 +156,9 @@ theorem not_lt_zero (n : num) : ¬ (n < zero) show false, from absurd nLTzero iH)) -theorem z_lt_succ_z : zero < succ zero +theorem zero_lt_succ_zero : zero < succ zero := let P : num → Bool := λ x, x = zero - in have Pred : ∀ i, P (succ i) → P i, + in have Ppred : ∀ i, P (succ i) → P i, from take i, assume Ps : P (succ i), have si_eq_z : succ i = zero, from Ps, @@ -153,14 +171,210 @@ theorem z_lt_succ_z : zero < succ zero have nPs : ¬ P (succ zero), from succ_nz zero, show zero < succ zero, - from lt_intro Pred Pz nPs + from lt_intro Ppred Pz nPs -set_opaque num true -set_opaque Z true -set_opaque S true -set_opaque zero true -set_opaque succ true -set_opaque lt true +theorem succ_mono_lt {m n : num} : m < n → succ m < succ n +:= assume H : m < n, + lt_elim H + (λ (P : num → Bool) (Ppred : ∀ i, P (succ i) → P i) (Pm : P m) (nPn : ¬ P n), + let Q : num → Bool := λ x, x = succ m ∨ P x + in have Qpred : ∀ i, Q (succ i) → Q i, + from take i, assume Qsi : Q (succ i), + or_elim Qsi + (assume Hl : succ i = succ m, + have Him : i = m, from succ_inj Hl, + have Pi : P i, from subst Pm (symm Him), + or_intror (i = succ m) Pi) + (assume Hr : P (succ i), + have Pi : P i, from Ppred i Hr, + or_intror (i = succ m) Pi), + have Qsm : Q (succ m), + from or_introl (refl (succ m)) (P (succ m)), + have nQsn : ¬ Q (succ n), + from not_intro + (assume R : Q (succ n), + or_elim R + (assume Hl : succ n = succ m, + absurd Pm (subst nPn (succ_inj Hl))) + (assume Hr : P (succ n), absurd (Ppred n Hr) nPn)), + show succ m < succ n, + from lt_intro Qpred Qsm nQsn) + +theorem lt_to_lt_succ {m n : num} : m < n → m < succ n +:= assume H : m < n, + lt_elim H + (λ (P : num → Bool) (Ppred : ∀ i, P (succ i) → P i) (Pm : P m) (nPn : ¬ P n), + have nPsn : ¬ P (succ n), + from not_intro + (assume R : P (succ n), + absurd (Ppred n R) nPn), + show m < succ n, + from lt_intro Ppred Pm nPsn) + +theorem n_lt_succ_n (n : num) : n < succ n +:= induction_on n + zero_lt_succ_zero + (λ (n : num) (iH : n < succ n), + succ_mono_lt iH) + +theorem lt_to_neq {m n : num} : m < n → m ≠ n +:= assume H : m < n, + lt_elim H + (λ (P : num → Bool) (Ppred : ∀ i, P (succ i) → P i) (Pm : P m) (nPn : ¬ P n), + not_intro + (assume R : m = n, + absurd Pm (subst nPn (symm R)))) + +theorem eq_to_not_lt {m n : num} : m = n → ¬ (m < n) +:= assume Heq : m = n, + not_intro (assume R : m < n, absurd (subst R Heq) (lt_nrefl n)) + +theorem zero_lt_succ_n {n : num} : zero < succ n +:= induction_on n + zero_lt_succ_zero + (λ (n : num) (iH : zero < succ n), + lt_to_lt_succ iH) + +theorem lt_succ_to_disj {m n : num} : m < succ n → m = n ∨ m < n +:= assume H : m < succ n, + lt_elim H + (λ (P : num → Bool) (Ppred : ∀ i, P (succ i) → P i) (Pm : P m) (nPsn : ¬ P (succ n)), + or_elim (em (m = n)) + (assume Heq : m = n, or_introl Heq (m < n)) + (assume Hne : m ≠ n, + let Q : num → Bool := λ x, x ≠ n ∧ P x + in have Qpred : ∀ i, Q (succ i) → Q i, + from take i, assume Hsi : Q (succ i), + have H1 : succ i ≠ n, + from and_eliml Hsi, + have Psi : P (succ i), + from and_elimr Hsi, + have Pi : P i, + from Ppred i Psi, + have neq : i ≠ n, + from not_intro (assume N : i = n, + absurd (subst Psi N) nPsn), + and_intro neq Pi, + have Qm : Q m, + from and_intro Hne Pm, + have nQn : ¬ Q n, + from not_intro + (assume N : n ≠ n ∧ P n, + absurd (refl n) (and_eliml N)), + show m = n ∨ m < n, + from or_intror (m = n) (lt_intro Qpred Qm nQn))) + +theorem disj_to_lt_succ {m n : num} : m = n ∨ m < n → m < succ n +:= assume H : m = n ∨ m < n, + or_elim H + (λ Hl : m = n, + have H1 : n < succ n, + from n_lt_succ_n n, + show m < succ n, + from substp (λ x, x < succ n) H1 (symm Hl)) -- TODO, improve elaborator to catch this case + (λ Hr : m < n, lt_to_lt_succ Hr) + +theorem lt_succ_ne_to_lt {m n : num} : m < succ n → m ≠ n → m < n +:= assume (H1 : m < succ n) (H2 : m ≠ n), + resolve1 (lt_succ_to_disj H1) H2 + +definition simp_rec_rel {A : (Type U)} (fn : num → A) (x : A) (f : A → A) (n : num) +:= fn zero = x ∧ (∀ m, m < n → fn (succ m) = f (fn m)) + +definition simp_rec_fun {A : (Type U)} (x : A) (f : A → A) (n : num) : num → A +:= ε (inhabited_fun num (inhabited_intro x)) (λ fn : num → A, simp_rec_rel fn x f n) + +-- The basic idea is: +-- (simp_rec_fun x f n) returns a function that 'works' for all m < n +-- We have that n < succ n, then we can define (simp_rec x f n) as: +definition simp_rec {A : (Type U)} (x : A) (f : A → A) (n : num) : A +:= simp_rec_fun x f (succ n) n + +theorem simp_rec_lemma1 {A : (Type U)} (x : A) (f : A → A) (n : num) + : (∃ fn, simp_rec_rel fn x f n) + ↔ + (simp_rec_fun x f n zero = x ∧ + ∀ m, m < n → simp_rec_fun x f n (succ m) = f (simp_rec_fun x f n m)) +:= iff_intro + (assume Hl : (∃ fn, simp_rec_rel fn x f n), + obtain (fn : num → A) (Hfn : simp_rec_rel fn x f n), + from Hl, + have inhab : inhabited (num → A), + from (inhabited_fun num (inhabited_intro x)), + show simp_rec_rel (simp_rec_fun x f n) x f n, + from @eps_ax (num → A) inhab (λ fn, simp_rec_rel fn x f n) fn Hfn) + (assume Hr, + have H1 : simp_rec_rel (simp_rec_fun x f n) x f n, + from Hr, + show (∃ fn, simp_rec_rel fn x f n), + from exists_intro (simp_rec_fun x f n) H1) + +theorem simp_rec_lemma2 {A : (Type U)} (x : A) (f : A → A) (n : num) + : ∃ fn, simp_rec_rel fn x f n +:= induction_on n + (let fn : num → A := λ n, x in + have fz : fn zero = x, + from refl (fn zero), + have fs : ∀ m, m < zero → fn (succ m) = f (fn m), + from take m, assume Hmn : m < zero, + absurd_elim (fn (succ m) = f (fn m)) + Hmn + (not_lt_zero m), + show ∃ fn, simp_rec_rel fn x f zero, + from exists_intro fn (and_intro fz fs)) + (λ (n : num) (iH : ∃ fn, simp_rec_rel fn x f n), + obtain (fn : num → A) (Hfn : simp_rec_rel fn x f n), + from iH, + let fn1 : num → A := λ m, if succ n = m then f (fn n) else fn m in + have f1z : fn1 zero = x, + from calc fn1 zero = if succ n = zero then f (fn n) else fn zero : refl (fn1 zero) + ... = if false then f (fn n) else fn zero : { eqf_intro (succ_nz n) } + ... = fn zero : if_false _ _ + ... = x : and_eliml Hfn, + have f1s : ∀ m, m < succ n → fn1 (succ m) = f (fn1 m), + from take m, assume Hlt : m < succ n, + or_elim (lt_succ_to_disj Hlt) + (assume Hl : m = n, + have Hrw1 : (succ n = succ m) ↔ true, + from eqt_intro (symm (congr2 succ Hl)), + have Haux1 : (succ n = m) ↔ false, + from eqf_intro (subst (sn_ne_n m) Hl), + have Hrw2 : fn n = fn1 m, + from symm (calc fn1 m = if succ n = m then f (fn n) else fn m : refl (fn1 m) + ... = if false then f (fn n) else fn m : { Haux1 } + ... = fn m : if_false _ _ + ... = fn n : congr2 fn Hl), + calc fn1 (succ m) = if succ n = succ m then f (fn n) else fn (succ m) : refl (fn1 (succ m)) + ... = if true then f (fn n) else fn (succ m) : { Hrw1 } + ... = f (fn n) : if_true _ _ + ... = f (fn1 m) : { Hrw2 }) + (assume Hr : m < n, + have Haux1 : fn (succ m) = f (fn m), + from (and_elimr Hfn m Hr), + have Hrw1 : (succ n = succ m) ↔ false, + from eqf_intro (not_intro (assume N : succ n = succ m, + have nLt : ¬ m < n, + from eq_to_not_lt (symm (succ_inj N)), + absurd Hr nLt)), + have Haux2 : m < succ n, + from lt_to_lt_succ Hr, + have Haux3 : (succ n = m) ↔ false, + from eqf_intro (ne_symm (lt_to_neq Haux2)), + have Hrw2 : fn m = fn1 m, + from symm (calc fn1 m = if succ n = m then f (fn n) else fn m : refl (fn1 m) + ... = if false then f (fn n) else fn m : { Haux3 } + ... = fn m : if_false _ _), + calc fn1 (succ m) = if succ n = succ m then f (fn n) else fn (succ m) : refl (fn1 (succ m)) + ... = if false then f (fn n) else fn (succ m) : { Hrw1 } + ... = fn (succ m) : if_false _ _ + ... = f (fn m) : Haux1 + ... = f (fn1 m) : { Hrw2 }), + show ∃ fn, simp_rec_rel fn x f (succ n), + from exists_intro fn1 (and_intro f1z f1s)) + +set_opaque simp_rec_rel true +set_opaque simp_rec_fun true +set_opaque simp_rec true end definition num := num::num diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean index f5175babe0f8927d4aa4dd5222c626ff8f6cc8ae..588c2bca4aa3d490cb31ab65c4d901fd92185680 100644 GIT binary patch delta 6708 zcmZ`-33yaR5`J$oFEjJzp=6Vgguny{B;im(01*(w8HmW`u7D_nLkQsrK|xs+lid#m zbUBhjj;Ih219Bx?f<#Wa)xRe5m6WGq( zivz97;1T}iwuoTrPLjb4roJ-3(X~FdprXZXttHrtc0d35mQmH>jBf2QR{nNiWP8vN z3QMr8F&1zcNQFlQkNuIQT4>ZGHiqsk_UaYXx44g9MhlAL_1#one3za<=Zf!b)`RES z)_VeaWmCNXJpy}Ex02y{cUoG~re1e##zf7PHz8-nV>8FoL8}qvEUmA9Ouv)_;^47u zXaHb@%pOSXC`La`Su`N(bPHzt`a&2FbcWW_pdsgFzkwk4G{$-jbhY|H?w5>w=Mi?7 zB;Skir7)%QqC~xyG*AChtUB|R2=jH>8ywJ1LSI>?G zED%JTP?JI=VNQM_o^)b$-&ssT%6w;AMYzUI%g=ob9A!xJCME-m=0yi$lJ9dG@>0Ux z7Xigcr{oC6Dipr6VJm(PzuXTn(OUAK?=xESQg+|ZVA9wE#wb9y33wLXMgG7<<>b7o zQ40(^OF*958tqRROS^H#3zi1rhC`wX^C3W$@e!Qy=tA>0{;+2cYjue>L zfSN9Em~y>#ta*dAVa5cZl$9AvW0oiMh=Ho~txitP!-~X=#s1wRYgHwbzEN1)_ajv; zPl|nzVMI{;6D;|@qwC9?CPgD?Cgz7!NJMRg45PLyx^jiwI1odHE6ljj&{I_+c~lK% zES0TD(7V!}6#>@m5gYCC$ieuSZm!5?&Y1h6X>e&IqhY1V@tH`m>swfogBzi$v_F-U zrg<{$i3dwF8uw-mvk$bT80%;cqxvt$>p9f&SOg;l~1*=$TBkQy{sL zlsrJ?|0F==|6~VF0aUGFDxjK{4|qx}OanY8uz-?6k?vrUJZ0qrb4)EP!?4NYGA(r_BH8XUW`Z3`(+KXT@3xsL>zuu!=7DNA~k7C zkY^1C-*$-}SlKrHvAX&aE5{FWM%bk3v~^`{WIr)NCsrmjkbOw@&PkoyqMDT*3d2mR zGlq?6=jtx14vvz9t(Ol?eF7#S1mc-GytDc8&dDDKi8(2askHZyXczjVO5vb1Lp#sV zpBAnU9Tc&-==UVz*{N`evxndkPVTgtG`geA7pu|?%TmCLfo4(vvV_4;13nWxdunG9 z62n0dVP=TE(ZN8dEiPiQb}B@jYE~xDdu54tg@+xNnx=xwz?>Tv;YG?Y4JnH@i)*{m zMC!Uale@{&s{^UCFkcC$y`?X_0~p=vMB0xHJ~ z9a!YRzc4g6Q_gFx^lkLQYYjvEm7x89fAMzK;#Kt7-vHhIMq;`bo06iFO{t<&tq}|D z3I<;7`CaO{wxzkZHsrHu=Gr{o@rAVs(z@)X$}@E@6YY8Fea``^_WHa7=K`vo&VyY2 z0+FqWo?4Z8`$ zJhgY)_j+>brCP3eIe2D7-@GJ^I@i|qmJj0no~(?f$>kQKS>?$MFxR+(X{ztR0rLuN zEl**EPs`IhSM4J4tP5C|S?DI4(QX~8X8Jl*&5P@j^~+STE@|i`wHEA&$H=SgF(dP< za0j87$A5lLxTKEj&DUon-hhGcKu*^6*YBn2>*4S6^{HOJ&#n^By2kbV$f1^Jb8f7M z$L-#TYvR|O+JKv)XMR{)8gppk8z>FF<%9SBuNxA`*wCc&LReGO_@HyVJKDGvi){o-*``17D@AO@s7OTDmEq_otnk9@bY=)aLZebx`p?;&Dw7 zFjD;Lq#iG&N+t?`_M2vP2%CyF7wQ{Jwv3D00j^qhCnNhe;G6W+mLxr&O1E@o`q7pw zrim3vQ5&J{95?@Ld5q;$c=hcxvEqe9+-@PASn5b>*q=}JDiaF#V7gkZijlqA+u*8b z?FCfP+Q&#&;oJ{y9xB3pfQf&uz=I6+Wqwz`@zdLBIx0ne*6Ep%I+W(C|KvP-L@UFu z=~kpPSoWu~GLd(6qOx_)Ayzj>plan#*CfAw>?Q1uSGRGPL|qutG5lzr&K&DjKr!AXYR%d*6WP*4j? zM^@eRBWBtQsk^ZAV(`m$U`Y$U+~4Pcq2u2Z^wIWq`X>~*<6hS%@(rQnpg}00 zGc<9>U-gT0b;qDCS1?fz5%pa%1OPb$$eUIAf8t3OxC}mcXm#F z2z|#kcGH31JMafUwc#Hf_>%*FW~eWdh5s!Ot z7aF;%y+7LP>X`}?7G!a>ZC4kw+U`<@mww!p9uuNsU&;Pz>asgA(A4tUA9iqn+}O8g zRqfmudVF`=#=ke$He%gD`**j{1N7zYUhGoKxB85~Q!HQu2GXXYVPF?FYz5>Kh1L#i z!_Z$X+&dUrJ<<2{U!dT{Secb3X~bwWJu#Y^9EzlCZzbz{sQ#X2dMdTwGcCI#CP>8@ zcQH~GXLN#v;bOcqLy!ETF}eW0%6IHo2AVaZ74m9eHNKUCE0kpzLn_0v0$`|aU{bNQ2C22}h5g6%`|THvVG1<@_>u@9JP z6Il-I3n-n-=m#iOWMn(=KEPbD(4Ud&T;iaAKw1)WoR3b{Y*{$?3i98g|GeEL>U-zD zlc3M0K6^WOl9ZFwv>>{^H5ZH29yX&ly|y>Mu)20@IxZmVS#eI~bqv-7Yi7Dk^&r4$(5}0z?Ec%O)Z`WD7p4@HNbsz;?-)mtiz8@FqFVcG^#ihuYXF%4>gN|f9gIz zXZu%ksM8dfvbl_`Z_?MbWY3Dv<0-4m_!HYkY<2j!jGM1JQz*50+Pb>Nh6Q zn8WG%a4I?6i!0^y;Z&x#4kr}Ogqq6C6O8Nz_asBR!Odc5H#qrSsE!qW7uJiE+Ikw0 zA1ROXLk5Yf=VRigHcYMYOw=2r21rUsz6z)?W@&EL_fqMRfFFr5(4Khw&XJTzMAMo^ z*N-GbLd5X4qbadx?At{JW&*m3@eE}j4JiG5ntC+QyD_W;f+5$tW4_cKP(6s<$AR#b zMDwIFv3_RaDAo(m2S?-d8FcAr550(59?RpLVUapPpti>YT&@F;x8qx<=y+^g5j0c-M{u>;qqXUH`t5Ug?9%l< M`HyDhO&PEK50S15$p8QV delta 6620 zcmZu$33yaR5`I0I$;`ZY5dulba3nxDLIgSFMiUVULKI#)x(f#V<@yC+IBoi$BqvHTrZaUl1k;CcRg_XCn3Z&9VY8(3V%3>%i)t@Q zh}EVjV^M18941siwYpm^F_z6I%O39Hv3Q|Z)sw18qP+T8mhJ*0C;&qW;&eugYxKkk z`BT8r?i;=k%El1QGY-Tg|5->{z_RKEi2WMS@t*+^!(Gy180&cWPe*xi7Bk%am>8}2 z=l=+(MS6^@;L%AVY)`1q;?8|Of>qBZ=nMyRn}DaWiP--!(eba;wQ7N(Ij4ZU;abh6 zLyK?id^{|bH4VhbfRBbQhI;^YiTuUk4(1Z6TgP<&p*n^x35Nc_^}2KjlXaARu2Hb0 z_xPbbQui@Oc5M1ZEmB>k8{_EeGH+m}>8}|8r?>%slx+Om}PL!hIJWhkI-M8g2R z5|pI^LC_J+_H_616rS5Nu`W$t9?NL<@*JkzzP-s3tK)QWd0KKOM9}pE=D`CaMpt$= zHCvG$-$^TipAXWC<}Xj987n-UyYtBGfw@x4HRcY2s-7SvA2}5d((V;kL%9*7CIaI@ zFE_4&RMnKIEHEoT@}&gw0Cfz;0O}Zwb)Yz@yVN*v^|S)O3b8QWFxY67;D?#(+9>c5 zhGu_(695NABC4{GEu%I6#2s@mO?$CL2q)Xb#UfkKj$U=VheX#-6;MS@iQci6$US|c8M*itY}Ns)M?a9b>qiE!T1Ek$3HWdM!u3n zD_%0QWSir_!;ZvnmE}x_L<-xM$YDftvHhYiUTS;SxSIM-&UHM;M@`DdSn5%SDF!FR z%oL+Ed}T06qAryn_gz?2w6bF;YAKz8=*o&XZP#4X`gw3yjb$Ri&`yA7PUWYE5fdas z=E!vB$W>D<1tEW=EOf)yDaPC}(fZ7k$~I^JnM8c9h?Y2kl={Lw=A_xUnoj#(_9ses z;G~%k@(joXs(Lw?I~i~awkt=rdU$(7gqhXsjl^;i2))JGJTxjK8(N);Rt9OrD-G_6 z4m%vPgUi4yjEeB=h~a7x#vJpX;l?+b-g_mBn^jzCO3SIRrcXK^3T^mT2R_EoETciC z89bw~^d_boN|PI|tGSH19y9XA|4jO<6y_V31(|j)OG|~&^F17u(lggVInuYL&{JjI zYn6pB*BKBdQ~T1?INO`2n87YwF3V8ssH8N3+O3N1gkq2#>S91Tq)nR9p6wTjjx2kY zLeH&gk`XmqcR^M(H%7v#PwRfFT-D0l5)R!H%F3-F#bj`I-T2@#{6IOwF}vNtoyP8dG!=LiL-U(WSlhY1mqemBz14_kM0?ZrR!t z>r+;6lg&7|HcNXZhekX*z;ac`Uair(H1#RMC)T-QZNX z^=@GMXD9WDnTeU^v2f-?^y_+L9yh$#-h9bxL8|pyEWP+@{cg{(wp|Bv0Cn=82lPtv z=K|{66R%4~etHa3cZhy?wS)UvhID;>65aAzjwSDCF_AU8b)64=U1P<7+I9(`w!HvQ z+m^b?N0VI-5dj4K3I-x?VZhda=!n?6=6*$tq7( zdDObR8`H7n*-STw5!{Zn;m(;M**p{VUByzRh)4E^$+2IF9$^?LldT^GToqYX z+z3cw&?^ILsmYcb)qd)?WuPjfm0ND&#ZPVthTerS9e$iMJNzdY`Ywpw_n@E`J_-1Y zaNlQSFZ==E?wSkhh9V0in)a(+_+-Ar9FM}k$7t-<_Ube(-J0n-t-n58DvwiV=+~{Y z)Ojj=b3pemF<-~vzYhFLnBvL>2VMlUTFEgzZ^);a;I3mUxb(FeYTP#gNrf!{mu z2SB~k%MSd}fj==+OJvb20@05G7pcMaUg{E!VCttfJL=J{?e$X5gerxW0d{Dg_8FvH5tKu$d%{61i>Fv|J`LpfmlkbZ4bIw_ zYDcn%01A7DJ zi-l}Px*>V`0QO2x7%g@G$HcW?LjuO$(9U(jKlN+0d*s1nI~tA4FQ zaKkUco-FG0)`Sq3nBJ4Z)nHANwR4~-Rqnadfp;Cw^D0=gBG}Ptm!DEY7u!s zA|lNgH-t5vyJS7pm&WbS$&}Xad63z5T821qD4mk;VVRJ&j$BJ!v!anP?>SM3$r9l9lS5q7`P3|L1I*jkW4 zET<$|N4ye6(XlRs74^p#Z%cFww>a$Bw7!XGNi&Jb@#)X$o-y>(p?0c2H9Opk6FTm2 zOQyw#gP}>7pwl#&k=?bXFtocCj)2{@rZKb+6s~^jHz_H+kXhFPuBqXC{mu+GwFX;C zS;}6BWKN#Tb+EDxH!EGI)<;qT$b=^wldjX?BQ0W)FKZ0VJQ9qBh~djeS|pzG>Hj{^ zffrdGz~{lsoD&H!dL(a&;T#qw)pCLF_)pBrbu8;cdyp`i_aC7?(h! zj@DBX>2F7SswZjp(d=$BSV2GNdS*Is7N9<$PYdK?9QBYP4`}D49ye3>V|Q?{L&w_3 zV-bCP>>$vAV=3w+(*(M5tWlfIkV{1&vi5(Gc%B5V&bF&7^PP6JLM(A9)q6r-cEKZK GjQ;}xa`kxt diff --git a/src/builtin/obj/num.olean b/src/builtin/obj/num.olean index 8d769ae92ba9595c57ebb6a3a817a938d6f84b3b..b266bd7fac099e46667c9a1ac7bf7722bfe34ea2 100644 GIT binary patch literal 15973 zcmb7LdyJjORiByfI(O|&ob?s1F|Bwx^*ScCu${!z3EIYCy=&Lm_(2ofNw~S*y=!mS zy}RCfw{e^bnb4w;mC`C0(m(~mq!4?P(4g=rs#=iHQXV#?m68DeQL7uedH63}q&DLG zerLX!x!>M(f+dg7%$zxMUUSZw`K~9&>$S${*m&LeKXz+Q( zusL(A_1IM1v`(0kYs^fTvBrtov9VTtq&n6ZF&i=$28=;x#F*a9)lZEzTg_^Hd~Cv) zE?47r7OgG2QT9qVWv&MFk7C&)_2Jgor#)Ya=zu1Zjmbu}IWye>0|;d_4kSj$8e^@; zWF+69>;}i0m^R(LXfrgjzu*Aqa;Fp!AsUk{?o~g@A!9dScP=OcB1cY`5soRlnsGP2v~9AuzI;Dp;@L{|s>w$3lM#nmdU0Q=-(O#Xq)*Cal)f^HlUr zVPORj{mn(24Mm1Bw`+1z6iA=v&f>)TvB>PkA=?0mlRME34j$(Eh(NR+wl`y-LXdMk zK^a4$2{rjf;Fz7|d?)eW(;OPW0VA{zZS;pBu}9Eimm5^Z4g#sny$J3hr`s`V3Em3u z{`P%{UZw@rVS%%W=sy9_cA@<+LE@$^OU}8hL<($5Wq`WdC$ZYMhv92HZgf~qBcHWZ??pGiCY16AP?gE62sOoW9}zA z56Y7{p2>EAd|DNiKHL~iJse>7+&1#5ztJ9J&W$2qdBL{ehRSZ zqk8@VU*hQig>896Uim0h_z^5MUq$l@nsPVVBMAwLuScsl`bZ~6 zS@xd) zRJRlHLM*xolPl2ps9OvNm?D|8vhb*CZa@MY>eeK>9iscueEw$XB90pOcx#PtWK#vO}lxV1)S|GQyMoKiq3&Cn`K%B+&PPj$|hq)GKMU(nHrNHz*d^ z%g-(aUQn?yzQ`Re2mM(?=DRy=%yVMS(n+4@S~L|YIwk*wyhJr5L8SvBvxtS{ZIRxz z1AVp7^_}o}R*6q5aE%z?K+P|@uG1pMt+Pe}6}K(Q4k9fyYKJt7cS>@K)r|#5G&5cSytqjkt@=LDj)``$oHR5Gpc~3Flt@Y7 z4e_YzLlTf*4{;@iB$8StB(0$zQRE8*>F<3s*l&;^!OsHJEcrQs>^6@6CcxV^(llDX zadl+9FHagz05evW%?7Sk2&BHMp&gQ(A?R{LM*9>RDW~wy6B^3se6!NGcVV=wF?$%W znJ?!grMeu%h`mcnMY+%C;f`BrDX;y4w-X2jRzsoCHQASYSVD~soOJ;q+o>+9D!CU+M# zgVaa<_D5UH0rvq#q0H2*mK>|&KxJsMRbzq^bnEWqaoUz)@#kZ)IxdF_&p3h4V8kxB z3%EWTVmo^bed?y-Q{sM%1UI#Z+c{kfUFC~Qc|6#tUouvyGky`o6nqX~KPCG;f$T8B z-v{_eFXkwSD)brjz0L%(hl{#dq*fB$@Pw!!LFWR%av;!RV9|NH&DN!+;Ora;>oG|- zg_*48L|hK-2&ih+iUeg(qj{W^*8zMC&1aNBY~f4=&9;(Z)1Siz@#zrqm{X62U(OsM>!)AbXg&IDGagf;fU! zuQN{z=yBiAQmN9WuuQMPmzS!a7F6|% zh~8`h_$#C+*X?g$R&?tc0_v`8>4q)3(j{O(Dlbqdb%kwz>-4cGIpZ}GnP=F91pc(~ z{-UP;OOTbAr7`%gdx7*K8iq^oZ-=E>p8w{A_dIgVDBV(Fu=eF{w|_#436OxX>^gA8 zP-AfzOr;y`5gVCZkiK2FDZ}{lXpD{kqN!%yt1^<_c#up)L%i$<#gLQLaW~SL zXZsD1q-Wc^Ik1BR(pXraz0yla%wuw1v)fC64M)V{v@NvjQ`{vlY>^4tXP!(A$a4Ey z?oqFGyT-m>rUZ$G=o<5y+aRN>vw^&y#PO zSgwHkwTzS8rWcJ_?xqg8PaMAqBzs@CYmQ0zS3R9xCucFIS^*>_ zsUS%yk|Tu@MBS8(*?yq*r7Bi;!8M8(O8;FW;WG*pRAb);8D4gjqPm;NA)CvL-6nMk zV+HUu{fm?hkw@J;W<>iv;O~wWu?ws?{|*ab1|slW6pQ6(5Z>D-CL5FD%N>(>deAlC z1&gV6F3=MHhE4U%e_KI4^Un2x6P)?Tgv-!vi&^=*7lT%Q=7H6I+7A@HLbNqGonGZ> zTYnM7dc8BzRJeL{_Lc)pI*z?hE=7~mOAQG^S{TzkufnhzU@kx#t}8J*aG@x7W5iO$ zNf_jf-pRFOP->^*gG?W8$E!ff?vsZ4a%%wz=ljRJ16;vC4=qj2LtsmV(v>i6*NIa$ zADhsytxkkVMJvk}3=xtAfT#{!nyY9u9mFHn;uIvdt1vGH8fQPZKqX&E*c7$3Q*m2BdJA{`0T_T5+!ivtNKnqq zfoA?v84rzLGXR|1e5LPhgEn3Ajeyi>KVA&nS`vn&j_SE65Y?gf`~@<1iAdBx1d}9# zHrR-kv>E#v`iZZsQU9D;4EFa6@~u?!A1`d>)A3SKKn90tm@f`m*vq(NWg zNHHK`vfbp-*~}tY8o;85a>GBAXcHmA*AF}^bY_~QLlHsK(TCN_jJXS-Jt9p~Na$(6 zSkNglK&sP5uFv!;9Q8*Q=Ggu(=yWV0+(}H8;dkcmbCx3Yp<8#_G>Nc8L`30 zSQ8(LCb&`_LOf+WEJO|&@aE8WT|k6KdJC*UpAKz_mEU39TrZGb#5A=Gh8(*e$dx5N zsj=CDg8dr2)2&8xCOCpS6WCIak0{>T<)mm-PVT-5r#3OZXbm-o!I%`TAjX)>Bpdlb407KDeXZD% zm?R1hwGx(I?MQ&aUm<~Y#6rVeTd0fLb0o*Fs`S)X(cYxSnpeZ=)m$C_rRr!`nc9P8 ziH)V%S|V+27u2H)Z~A7Kf9wDk#hRL$&}v7ILIxy~)jE?(`#voJXYlv}U9-Zm@QXCA zA#l8ZjiVf5=`(2H1deZ6cC&y!aQvKtJ`=tdj=7IBTmuvd9C|S@FX?HaEkf~R_v+=J z$_zKqh(i~BH~*Y71&YD}8v4A1)l=yBHzksVYuc}2unhl6k{mBeT*t5n)~11{ImUe% zFsIdr^FVyF45wPmulRDQX1%yfD8{Ne#AE=EN0D>~a(OG}G!WmWAOec~adX1kHbRff zb!WQXoE-mjU8dUIF>;&z7_$j2o(iFY=8|j&X`4L8H^(NXtX7X{3ImLRbz1V4e%4IvdmCq4i(DCwPy1ess^ zk{p+&HqbJapbGy$%0Lpo@Yv^asqYZ%jzW*lK+GVtN?1-Mr22%7B*S8FIv}5d?QZm+ zq;vxS%LE4n%5EpP7o+;X19`I@a`g+p$*F<`{!yQ%MsTzAmX#lNaz5L^_fZQ`d<72T z(f+2AOWQBQN!buAJYJuesBK+FURjgf9>kP)hq2L7!(zg$#~dPkc306}J<1ezY-0so zve&_iGL>x(rZbDZ7}$dqv|l`;bQ^EZYa^*|-3uCOi2VT75C;VEhB$~(`OF5{@-JnW z9VB)2<&791H+o93M2`?4^<+RHs_ANzwVf8J*uB{vh_oqQ8H*Dc<1|07=+?%juxUa79tw3z@T5nuKfD> z6Y|ql{>HOS5mzuRy7CMjkHmEb(*@e?I-Ukbc2qM5z$ymPRBG0D$%y?V##OMe-N~?> zGFt}DA{x~&ilwKhh%u!Q-8cVdmm7=43N*i364 zYVQp}m1ohUIsH*Gyn4a zb--;OJTxvnO#O|?T=sA;TAGR*bA|;XtvQd4)Y=aN@psVeC03jlN&UvnT8F zIPu3Yzua5E!tr1e1jZIUQ7#oRK*I{YnhH`{+$D|tI%;%lo44>#(_0p#Vrxy;8vIb< zFDaPFp2bQ&Jd6qG!);0@xY76Qi(Pvi#4Y=jv`Cr>_wG!2F6d z<|5ohFEss;CNCh$m|p1U*HDRj5cvFfq7m#%(#uv@?;tB008xvMmpN zh57|c@>q>5RrSB>!w5L{GLb#KY>*vJsb1-#cLQI&^_SwgqI`URHCV;li8`*@Kpht* zEuQLj8g3-0NAGWXz#(q?0hdoM@+bQzXuJ6QtS4k4Qs#+S0RF##eD+~!JQ5&rW4%OV z|0=0q`cZLStj!7+T0WfHy>Pvmx|A04-hYsxxW!8`;X{sjAxv`8l7zxMo<6K39;rd*wUNP zZvoaqPo4lo`0!(0T+CL>U$-lqOv5sQ5@z3(sq8Z6!2}PGALOPK3`TOhiu1vZiEl2F z{wkt^()ZY0V^MGs>XGm9%()p&%;j&=_&)$8Wi%?PAA|obO@~tnnQx5jy;ax=Glsu% z&?g3d`|+bI% zIOai*DgvuWd9V;9{b;6TWnV9r>FXU-ks#}r>I?$fyMfg?EXUlUYSW0!yN?pn0S3uM zkYQj#I9fgwk`rhuiAJScDEWX4mTvLyT%}v&(QIGK=$#??X@)wqzA9V?Iy}K{Ei4#A zDD#MZT;+FN-v@e`>bt}(k6{3;YtCR4^x;&(Sw!KcJFrk+W8$fjpC%*tZddFKGGuQ{ zlZcnSEj5fh$`n2hV_UaTAKQP36=cLg4x>5@5miP?E7ZOM`f3p8Sw1>TOR?3RV9ipD zn|=^T{$vPbP{*iu?*eo!^x$e5F>#RSUCHwP;I@9ZZ~{y}$nTbBnTWY2GNwQLgm>sp z{|Jb`Bgh!2^l349pVe#N3xZYJ16&-j(mpi$+c<=9We7G=t21KiAbdZSd=J#Cacm_( zp5D?u3Wm9)MC7ie!;j5SVES5MY_wVo*&xOCu+$~l=Qr;V)oFF`|5gpO4m3*&~1sL)vyl@P#2&yT41Y+ zY5wM44M1Ll6s8rpR-N4g8b?8nF}@UCqf`Tb2|tGK?X+kTK9$T75GZ$})sOOWB~RWC z^;ZFQMy5+o^h(P+n#KX_tq}vs+3EjIc$%1KJ}b?VI~wtMF)&xVWZs?umIl^er$QKP zNP1<^I8~|ju5PIHE|yXO;bK1`BjIC+5X1JZv5Bs{{yfW BOH%*< delta 985 zcmZ{iT}V@57{}lDjCH1q!Op%xLDP9=7}1I(q!zKlNw`6l1i^~6%BU&2j3kKiB6Shg z(;x}#o2)Ko)Kv*xd2YKhFRGg&y6C2EyXyTvud*u#`=8(Ye7(=}ob&VQyX0b5{HX{;F<6V81*`eSvI-uQcQE?SStL%$YghhWOFlOmvD5lmt7jBgg=tFp$#if727fEm*^Yky=C2M3y zwhywCr*K%`qgthd<8E*-qMJ>~Ujmt4=yA!H`>F~frQ7ur`3-fGFoD0{eDQe4pN=Fm^{DpFU>{6kSpAb5jCZj#gqs7xg zqN>{S5L!|TG;(7Ad4Rq~Q$AkUTB8L)cI?pRZ*W_fNPeL!u~cG3GtAD~6mWh{Kx=FU Xt8L;1Q2$CY`