From 70828af6db8596e0ce7d9c25fcdd306e5a0d03ef Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 17 Jan 2014 14:52:09 -0800 Subject: [PATCH] refactor(builtin/heq): cleanup universes Signed-off-by: Leonardo de Moura --- src/builtin/cast.lean | 18 ++++++------------ src/builtin/heq.lean | 33 +++++++++++++++++++-------------- src/builtin/obj/cast.olean | Bin 2848 -> 2848 bytes src/builtin/obj/heq.olean | Bin 1981 -> 1990 bytes 4 files changed, 25 insertions(+), 26 deletions(-) diff --git a/src/builtin/cast.lean b/src/builtin/cast.lean index b429bfca8..d09e26189 100644 --- a/src/builtin/cast.lean +++ b/src/builtin/cast.lean @@ -1,10 +1,10 @@ import heq -variable cast {A B : TypeH} : A = B → A → B +variable cast {A B : TypeM} : A = B → A → B -axiom cast_heq {A B : TypeH} (H : A = B) (a : A) : cast H a == a +axiom cast_heq {A B : TypeM} (H : A = B) (a : A) : cast H a == a -theorem cast_app {A A' : TypeH} {B : A → TypeH} {B' : A' → TypeH} (f : ∀ x, B x) (a : A) (Ha : A = A') (Hb : (∀ x, B x) = (∀ x, B' x)) : +theorem cast_app {A A' : TypeM} {B : A → TypeM} {B' : A' → TypeM} (f : ∀ x, B x) (a : A) (Ha : A = A') (Hb : (∀ x, B x) = (∀ x, B' x)) : cast Hb f (cast Ha a) == f a := let s1 : cast Hb f == f := cast_heq Hb f, s2 : cast Ha a == a := cast_heq Ha a @@ -12,24 +12,18 @@ theorem cast_app {A A' : TypeH} {B : A → TypeH} {B' : A' → TypeH} (f : ∀ x -- The following theorems can be used as rewriting rules -theorem cast_eq {A : TypeH} (H : A = A) (a : A) : cast H a = a +theorem cast_eq {A : TypeM} (H : A = A) (a : A) : cast H a = a := to_eq (cast_heq H a) -theorem cast_trans {A B C : TypeH} (Hab : A = B) (Hbc : B = C) (a : A) : cast Hbc (cast Hab a) = cast (trans Hab Hbc) a +theorem cast_trans {A B C : TypeM} (Hab : A = B) (Hbc : B = C) (a : A) : cast Hbc (cast Hab a) = cast (trans Hab Hbc) a := let s1 : cast Hbc (cast Hab a) == cast Hab a := cast_heq Hbc (cast Hab a), s2 : cast Hab a == a := cast_heq Hab a, s3 : cast (trans Hab Hbc) a == a := cast_heq (trans Hab Hbc) a, s4 : cast Hbc (cast Hab a) == cast (trans Hab Hbc) a := htrans (htrans s1 s2) (hsymm s3) in to_eq s4 -theorem cast_pull {A : TypeH} {B B' : A → TypeH} (f : ∀ x, B x) (a : A) (Hb : (∀ x, B x) = (∀ x, B' x)) (Hba : (B a) = (B' a)) : +theorem cast_pull {A : TypeM} {B B' : A → TypeM} (f : ∀ x, B x) (a : A) (Hb : (∀ x, B x) = (∀ x, B' x)) (Hba : (B a) = (B' a)) : cast Hb f a = cast Hba (f a) := let s1 : cast Hb f a == f a := hcongr (cast_heq Hb f) (hrefl a), s2 : cast Hba (f a) == f a := cast_heq Hba (f a) in to_eq (htrans s1 (hsymm s2)) - - - - - - diff --git a/src/builtin/heq.lean b/src/builtin/heq.lean index 87c973708..64fed7f58 100644 --- a/src/builtin/heq.lean +++ b/src/builtin/heq.lean @@ -4,33 +4,38 @@ import macros variable heq {A B : TypeU} : A → B → Bool infixl 50 == : heq -universe H ≥ 1 -universe U ≥ H + 1 -definition TypeH := (Type H) +axiom heq_eq {A : TypeU} (a b : A) : a == b ↔ a = b -axiom heq_eq {A : TypeH} (a b : A) : a == b ↔ a = b - -definition to_eq {A : TypeH} {a b : A} (H : a == b) : a = b +definition to_eq {A : TypeU} {a b : A} (H : a == b) : a = b := (heq_eq a b) ◂ H -definition to_heq {A : TypeH} {a b : A} (H : a = b) : a == b +definition to_heq {A : TypeU} {a b : A} (H : a = b) : a == b := (symm (heq_eq a b)) ◂ H -theorem hrefl {A : TypeH} (a : A) : a == a +theorem hrefl {A : TypeU} (a : A) : a == a := to_heq (refl a) -axiom hsymm {A B : TypeH} {a : A} {b : B} : a == b → b == a +axiom hsymm {A B : TypeU} {a : A} {b : B} : a == b → b == a -axiom htrans {A B C : TypeH} {a : A} {b : B} {c : C} : a == b → b == c → a == c +axiom htrans {A B C : TypeU} {a : A} {b : B} {c : C} : a == b → b == c → a == c -axiom hcongr {A A' : TypeH} {B : A → TypeH} {B' : A' → TypeH} {f : ∀ x, B x} {f' : ∀ x, B' x} {a : A} {a' : A'} : +axiom hcongr {A A' : TypeU} {B : A → TypeU} {B' : A' → TypeU} {f : ∀ x, B x} {f' : ∀ x, B' x} {a : A} {a' : A'} : f == f' → a == a' → f a == f' a' -axiom hfunext {A A' : TypeH} {B : A → TypeH} {B' : A' → TypeH} {f : ∀ x, B x} {f' : ∀ x, B' x} : +universe M ≥ 1 +universe U ≥ M + 1 +definition TypeM := (Type M) + +-- In the following definitions the type of A and A' cannot be TypeU +-- because A = A' would be @eq (Type U+1) A A', and +-- the type of eq is (∀T : (Type U), T → T → bool). +-- So, we define M a universe smaller than U. + +axiom hfunext {A A' : TypeM} {B : A → TypeU} {B' : A' → TypeU} {f : ∀ x, B x} {f' : ∀ x, B' x} : A = A' → (∀ x x', x == x' → f x == f' x') → f == f' -axiom hpiext {A A' : TypeH} {B : A → TypeH} {B' : A' → TypeH} : +axiom hpiext {A A' : TypeM} {B : A → TypeM} {B' : A' → TypeM} : A = A' → (∀ x x', x == x' → B x == B' x') → (∀ x, B x) == (∀ x, B' x) -axiom hallext {A A' : TypeH} {B : A → Bool} {B' : A' → Bool} : +axiom hallext {A A' : TypeM} {B : A → Bool} {B' : A' → Bool} : A = A' → (∀ x x', x == x' → B x == B' x') → (∀ x, B x) == (∀ x, B' x) diff --git a/src/builtin/obj/cast.olean b/src/builtin/obj/cast.olean index 0b2e2662475a37c7770d36e95b065a01d03510b9..c67f10dee2de8c79934c9b104a3dbc80fbd33d94 100644 GIT binary patch delta 17 YcmZ1=wm@ux7o+b)Zz)FKjcL2M05hBgv;Y7A delta 17 YcmZ1=wm@ux7o*2SZz)EPjcL2M05eeqssI20 diff --git a/src/builtin/obj/heq.olean b/src/builtin/obj/heq.olean index 6ece1454a2c21e47d9c31b434d38acc421af835c..3dfde29b2f304938a755f3dea2b76967b84f9ab1 100644 GIT binary patch literal 1990 zcmaJ?O-~d-5bbVsm@ME2_=OrTuz2!f3>UKy)@USrBpOM)nE_^CWp-vA2C{fE{&MTR znw}mYu@A-Ts;=r+uWN@gPm>}W<*8|w9gQbtRhzT4D$?9EyZxj#mq}&ZY5L1VZp%3L z?P`)97}*RpGjfTs0xbZRb#7RexiQ=02^}!b+WoRl>QPx>Yu#XAoPf75vXUw9_|aTL zpRX);9nxV}of~DDF>Bb);#Q{ju*J^AednYESI6s_#1gRfIL(Z!%UgFLD{k+K+-H`V z>*LQn%Fh64*}H)EVGQ8|pqTI>pe0-coLd7YXrZ*>V}K^GTw`pn^-`6nVcT;DB%-8CH)joNk0QzAXmaA?3bm9^Q-X~xKVu>h`|>?EyYK& z0mb@Mp0rA{oP&cS0(3;;pah>y-wr2~4GXHUFX>&QG^p$!nr@i~UeNJ-p`PQUeD5$9rswZ`1-Epr*Va{1oOgR4;xI(`;6Xyr^8^GO zd5>p;tN2*!i0DLk88?(Hj?5xDfYEcF(yDkOP-;jWmBmTbCAIY$N&0*Cby1KWjcrFR zlawjFi!1m;9x`T`p4jo30|Dv+YQ*%Zn=2?BAwQ;l2e`|Eq|VV-*+VvR7}&&V6+ruD zBE3p#mj^;Q^;|AplKRmTL5J$1v`7{OyIS_)n}<1u(T9a5UdvqpT0)Q)8b`mv zP!!NJ&C~{|dW4k92C39bshIY~&krg^su$avjC^;fE**7y0~0KkK)1?p3jd9c!YliZ z*4vH*bvq(gD$wl+_fQ*}pV*%1ScHf#Jz%5kPG(l;c%44dXun)Lk{W)$NuK|wSKKnw qwkSwjzXE9QxZV;{eg}>m51O0oL*x%~{`$xGE*tXuSR8-C|L%X~Pnu8w literal 1981 zcmb7FT~8B16rCA#LDm9MOZ*^e#G&PwU>7Re-MU>!c{2WU?>Tp; zvo=xVK3vY+uQ}(=Oeym;DY9Xnn&z{^(YUN?bCFg>nww^|pVa0msf;^MznjSI8s`qL z$LW!g#Xu_~ml!M10^qaG4azb%=HqBg2aL0JzpRsbSQc1Xx3goMfY&hcT^7Tuw3?*G z?HS8<*0|%cZUv5J0Te8qrkNp`J+r74aJxm?WJ=0kJ!?2);jB~z9K&PmbLWOxX3Q2= zi`bWZI#^<5;+}KTgkQ_+rQMc*wWLy)em5j9`)S0py&{o@Z>0yjiuMaY+V&>kU6^IU zdw?-v7tj)}1Fmd=6Nam_;bRU>V7cC-7;tP7LM-+Q?nrFG1`Yn8QS%oOYlv@<(*vdw zJ_J@fz?6hk*wPfxLuc50d#aY8^q~ z+y&nos3Gx=-}4#VqFlGFtE8B;wa@l_hte>Ojwc}CgdqW*33lKhwh>V}{<7{WC8Y2j z^^u}^p3+P4M4;4=Iw^~@s!eM51&VYmzAsf_P#XIjxlBr?Ozdvr4|&L2$uwi%SM~*{ z3#b{UFCA>6afJGq_6^_x8}W_#2qb)IWLc&>iA)=}gLVZdX8c4AZ)E0s@M?&)r%ZpH> z5#PE`eH0}(OK;mYeWWq_efcC!!YfPi{2vk*X2&Ne0R=N{pUs>k#IFNKhc(SS`w;no ToS*&-zQ}_7-WR7I@Gtup`@olQ