From 0283887ee9309cd914f3e39f5b68b770eb92b773 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 4 Feb 2014 14:15:33 -0800 Subject: [PATCH] refactor(builtin/kernel): move the heq axioms into kernel.lean Signed-off-by: Leonardo de Moura --- src/builtin/heq.lean | 71 ---------------------------- src/builtin/kernel.lean | 76 +++++++++++++++++++++++++++--- src/builtin/obj/heq.olean | Bin 4669 -> 51 bytes src/builtin/obj/kernel.olean | Bin 44575 -> 49208 bytes src/kernel/kernel_decls.cpp | 14 +++++- src/kernel/kernel_decls.h | 42 +++++++++++++++-- src/library/heq_decls.cpp | 13 ----- src/library/heq_decls.h | 39 --------------- tests/lean/univ.lean | 14 +++--- tests/lean/univ.lean.expected.out | 2 +- 10 files changed, 129 insertions(+), 142 deletions(-) diff --git a/src/builtin/heq.lean b/src/builtin/heq.lean index 6321f7e77..130458d27 100644 --- a/src/builtin/heq.lean +++ b/src/builtin/heq.lean @@ -1,75 +1,4 @@ -- Axioms and theorems for casting and heterogenous equality import macros --- In the following definitions the type of A and B cannot be (Type U) --- because A = B would be @eq (Type U+1) A B, and --- the type of eq is (∀T : (Type U), T → T → bool). --- So, we define M a universe smaller than U. -universe M ≥ 1 -definition TypeM := (Type M) -variable cast {A B : (Type M)} : A = B → A → B - -axiom cast_heq {A B : (Type M)} (H : A = B) (a : A) : cast H a == a - -axiom hsymm {A B : (Type U)} {a : A} {b : B} : a == b → b == a - -axiom htrans {A B C : (Type U)} {a : A} {b : B} {c : C} : a == b → b == c → a == c - -axiom hcongr {A A' : (Type U)} {B : A → (Type U)} {B' : A' → (Type U)} {f : ∀ x, B x} {f' : ∀ x, B' x} {a : A} {a' : A'} : - f == f' → a == a' → f a == f' a' - -axiom hfunext {A A' : (Type M)} {B : A → (Type U)} {B' : A' → (Type U)} {f : ∀ x, B x} {f' : ∀ x, B' x} : - A = A' → (∀ x x', x == x' → f x == f' x') → f == f' - -theorem hsfunext {A : (Type M)} {B B' : A → (Type U)} {f : ∀ x, B x} {f' : ∀ x, B' x} : - (∀ x, f x == f' x) → f == f' -:= λ Hb, - hfunext (refl A) (λ (x x' : A) (Hx : x == x'), - let s1 : f x == f' x := Hb x, - s2 : f' x == f' x' := hcongr (hrefl f') Hx - in htrans s1 s2) - -theorem hallext {A A' : (Type M)} {B : A → Bool} {B' : A' → Bool} - (Ha : A = A') (Hb : ∀ x x', x == x' → B x = B' x') : (∀ x, B x) = (∀ x, B' x) -:= boolext - (assume (H : ∀ x : A, B x), - take x' : A', (Hb (cast (symm Ha) x') x' (cast_heq (symm Ha) x')) ◂ (H (cast (symm Ha) x'))) - (assume (H : ∀ x' : A', B' x'), - take x : A, (symm (Hb x (cast Ha x) (hsymm (cast_heq Ha x)))) ◂ (H (cast Ha x))) - -theorem cast_app {A A' : (Type M)} {B : A → (Type M)} {B' : A' → (Type M)} - (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 - in hcongr s1 s2 - --- The following theorems can be used as rewriting rules - -theorem cast_eq {A : (Type M)} (H : A = A) (a : A) : cast H a = a -:= to_eq (cast_heq H a) - -theorem cast_trans {A B C : (Type M)} (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 : (Type M)} {B B' : A → (Type M)} - (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)) - --- The following axiom is not very useful, since the resultant --- equality is actually (@eq TypeM (∀ x, B x) (∀ x, B' x)). --- This is the case even if A, A', B and B' live in smaller universes (e.g., Type) --- To support this kind of axiom, it seems we have two options: --- 1) Universe level parameters like Agda --- 2) Axiom schema/template, where we create instances of hpiext for different universes. --- BTW, this is essentially what Coq does since the levels are implicit in Coq. --- 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) diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean index e33425a79..0d155c5aa 100644 --- a/src/builtin/kernel.lean +++ b/src/builtin/kernel.lean @@ -1,3 +1,6 @@ +-- 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 tactic @@ -894,11 +897,70 @@ axiom pairext {A : (Type U)} {B : A → (Type U)} {a b : sig x, B x} (H1 : proj1 a = proj1 b) (H2 : proj2 a == proj2 b) : a = b --- Proof irrelevance, this is true in the set theoretic model we have for Lean. --- In this model, the interpretation of Bool is the set {{*}, {}}. --- Thus, if A : Bool is inhabited, then its interpretation must be {*}. --- So, the interpretation of H1 and H2 must be *. -axiom hproof_irrel {a b : Bool} (H1 : a) (H2 : b) : H1 == H2 +-- Heterogeneous equality axioms and theorems + +-- In the following definitions the type of A and B cannot be (Type U) +-- because A = B would be @eq (Type U+1) A B, and +-- the type of eq is (∀T : (Type U), T → T → bool). +-- So, we define M a universe smaller than U. +universe M ≥ 1 +definition TypeM := (Type M) + +-- We can "type-cast" an A expression into a B expression, if we can prove that A = B +variable cast {A B : (Type M)} : A = B → A → B +axiom cast_heq {A B : (Type M)} (H : A = B) (a : A) : cast H a == a + +-- Heterogeneous equality satisfies the usual properties: symmetry, transitivity, congruence and function extensionality +axiom hsymm {A B : (Type U)} {a : A} {b : B} : a == b → b == a +axiom htrans {A B C : (Type U)} {a : A} {b : B} {c : C} : a == b → b == c → a == c +axiom hcongr {A A' : (Type U)} {B : A → (Type U)} {B' : A' → (Type U)} {f : ∀ x, B x} {f' : ∀ x, B' x} {a : A} {a' : A'} : + f == f' → a == a' → f a == f' a' +axiom hfunext {A A' : (Type M)} {B : A → (Type U)} {B' : A' → (Type U)} {f : ∀ x, B x} {f' : ∀ x, B' x} : + A = A' → (∀ x x', x == x' → f x == f' x') → f == f' + +-- Heterogeneous version of the allext theorem +theorem hallext {A A' : (Type M)} {B : A → Bool} {B' : A' → Bool} + (Ha : A = A') (Hb : ∀ x x', x == x' → B x = B' x') : (∀ x, B x) = (∀ x, B' x) +:= boolext + (assume (H : ∀ x : A, B x), + take x' : A', (Hb (cast (symm Ha) x') x' (cast_heq (symm Ha) x')) ◂ (H (cast (symm Ha) x'))) + (assume (H : ∀ x' : A', B' x'), + take x : A, (symm (Hb x (cast Ha x) (hsymm (cast_heq Ha x)))) ◂ (H (cast Ha x))) + +-- Simpler version of hfunext axiom, we use it to build proofs +theorem hsfunext {A : (Type M)} {B B' : A → (Type U)} {f : ∀ x, B x} {f' : ∀ x, B' x} : + (∀ x, f x == f' x) → f == f' +:= λ Hb, + hfunext (refl A) (λ (x x' : A) (Hx : x == x'), + let s1 : f x == f' x := Hb x, + s2 : f' x == f' x' := hcongr (hrefl f') Hx + in htrans s1 s2) + +-- Some theorems that are useful for applying simplifications. +theorem cast_eq {A : (Type M)} (H : A = A) (a : A) : cast H a = a +:= to_eq (cast_heq H a) + +theorem cast_trans {A B C : (Type M)} (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 : (Type M)} {B B' : A → (Type M)} + (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)) + +-- Proof irrelevance is true in the set theoretic model we have for Lean. +axiom proof_irrel {a : Bool} (H1 H2 : a) : H1 = H2 + +-- A more general version of proof_irrel that can be be derived using proof_irrel, heq axioms and boolext/iff_intro +theorem hproof_irrel {a b : Bool} (H1 : a) (H2 : b) : H1 == H2 +:= let H1b : b := cast (by simp) H1, + H1_eq_H1b : H1 == H1b := hsymm (cast_heq (by simp) H1), + H1b_eq_H2 : H1b == H2 := to_heq (proof_irrel H1b H2) + in htrans H1_eq_H1b H1b_eq_H2 -theorem proof_irrel {a : Bool} (H1 H2 : a) : H1 = H2 -:= to_eq (hproof_irrel H1 H2) \ No newline at end of file diff --git a/src/builtin/obj/heq.olean b/src/builtin/obj/heq.olean index fda2c6434b5dba13f65059ce2dd34b40fbbb093d..a9360f428a55f1ba85af21fd4ac56dee2b4049e0 100644 GIT binary patch delta 14 Vcmdn1Vmv{c!!<9(Ei)&T0RSUZ1aANU literal 4669 zcmaKw-ELG>6vxlUFdbn?j3I+JwIo0X$_P>s5;ZEV*zp21k%EaKWLl=QIGq`0T4=A- z_yOL?txCK@9szv^pFnTCLVW`-G{pV?tvP4!o)%Bi)wS1JdwuVaEx0m#vvqBf zGc%5CnI|eyjCZt>EIHl=g4Kiig&!qHH;H4}&T)qrN!Tcv+181J@^rLST99m@5Z6hm zrQPq=o{FR=1S|m-HyfdvQw;>XI-_pQ#{nl(v3!g&vb5f9Z)|DvQA+ZLckzdrkQEnj z82Vw+!g|$U<*8#PZ^>EH4tB79fUHSg9CUnQ(|K^^qBs$k=u=EBA4yV^r?7 zW!Hnl?a}!%lkTUKnLJNzjWP?S7C4CyB|M{W=$vAWXQO~9;9H82LZ8S~vAQfe2GcR2 zuL;DUuM3?AeM9I`&^Lu%0%bNG8%vrCqD3D~VO41uneu1C8cU4yP?`+dOC8}^$;L+g zJ?@Y?^oG;A5zGUs6qIUDGCUc@mJ4k-C-92EoWL2Ml(G|@4nuIY?@IeQBD^^m;D!`JuX7Nt*6L5z`+bi_>uy@-tM+&yd5yGlZ)au9TF# zsykX!jb?#(CF?*M_`@*?UJ$Upd(Wfq3%!fL2OhmB^lPZ|LcejB)q;yl8Q{Ajc+a(v zt@5rKcY^Jkx*4g%IQ_F%LWD8l*j!j_W13JDm?VYbUM3vQ%za6g>}KTd9w`#}dw3Y4 zboVoVoMSf58`%FA5j)rTvXjjdh<+!PcLYud{OBFQu?KYw=_bq~681pAX2B0ai~7Bb z53*5qUOUuXYA(G*uD1Gp*9@Ha$PMRkOy}Jt^|A<-kA10%C(MbHhr@+mv0Ml z{gOCW2z1ZWb3%w^iOyk%lreMIPa>$*&yu-8moT5KxfVq=^qSB|2;iup*F`-Bby;W) zbVcYa=nbJi6$cQ;kK_DPJ*vW{21SR9Ly8(rdv*S*D$6_p2I`7zI<_N8IIF^-O?Z|4 z>=aIuY%G#JEO4ZQ1A+>aVVjc+pdR^HQhB#F&er#4vp8$8=pHlH7pZTFviB5+0A@_l zl&D2ds8zEs^jD}nTits#S?gWR->_o;CJ>y2qT;OmyG|_V{jHD5{AuElSt(S{H(LwE z$jo6i`XW+~vmk3eNGl-?Lo&&2Iw^UGQ~?g!%yrMH9&s`9(!~O&$ZtWJc_FrCj0tHO zTNl;PTOPeF^f7s4N*TH-YOUDxz7_ry{|_9ezk_Jt6#E-5ZT=BXLsAee1zK7jP*-F- zbuWi^Iy-~jrkTf&NXuUWWX8`u#J!8;$odUywp;uD7SIdgRA>!v0_VNrV2b-AiM628 za2f^Yytt3mJe-mbLjgFpTg!h1ssc|6GB|`FGXLa))(v&79}0MlPqajtHQDc42O0JL z?Kl)r6hyzu_Ckyhy(0GbQsgs4v8LhO(_im&!po=dir(SMxs;u?YVo4Uh90@)@q14q z+ulIUgNlHJ1ViZzsoPr-?~VX5yeNzdfceCxV0_JqeMW#`XIIjvTHE3KOxSZ{B781j z_s|zYFG2lMXchD;hsFCq?+V>^B(XCm*7FWTH*l~c6bwM@zKrpHu?zlJMJpVPZGwj+ zq+w~ww>`B_i?ul^$SG%vK(xQ7a732kIzpVjK*)1wNBi3#$UeQq9q@~6;IlQ9w|QF} wCYk-=W_*8OVC6!w5)`YTF;{e2*Y<}3xgZ>5qP%B6aRTbubKPt2=wC+v0e~hg&Hw-a diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean index b856c463e37dcfdaee3cdb3b48d370badb8b6752..2c41e93644c73a46bdbe947eee05667c0fa2d9b7 100644 GIT binary patch delta 4553 zcmai2-)~e^5I*71}l zp+tJTI%eE~>iC2yx;w$KJw7cw($NG7de#ZipHuv8w3ylT$9b12L$YRR0{9 z)L#ao3G&yDBqGi>Ol0I@6D|mQ2~3EL7&tO=Fc^!21sir&uoP&Qur*F}102rT$)Y<1 znZj8CWC5w@oB-7T6d7G~C#e%wdG%;y<}o^HjHC!7Cho=yWG25)i29*ks&gF)w+2Wh z1_I6#Ab#xVB^edf(a6=IV>aAmMC<2TuvHuf1e-kB*HehacADI;0cQ|5 z_bT9NA)?aNqCQ=S&7OmZ)5CBQ+dg5?d}kZyFt$BH82LawV=T~DyxVjFNoCIoF(qva zXMiI$0xZhel(-E7V$VgUz$WIqna@~K2c{)@+{k{-`+%FCOe|wKQ5eR4l32oyXD?Q; zlgFJimRy7`W|aLE8!yJG^ab>wJ|>0($)xec)xi$j(i$gFTJ^UYt3EzvI>=_q z!#0Ou6xzQz0M|@QEXaJId#AxKQzpkF{!YeGYTOdo(n{|4;7$_$Ah2+Y@JGP25_2|7 zd!>`1xgy-C^D$M~Cbhj_BDV%~wfyq@&72$+_a~}g(#(s_$+X=vni^8fO zUWF9QX$USDOj4hzr*av{)~PPlasN485Hs`Psg~tCyl(~O**ei=a549$_bIN^?&d3* zw{c0jMR;ne-Pdws(=LY}Pc7T=n<$J<^>@IZd47KgG&yGd9YEIGFF6EnRL^R?AopP*QGSIZ53C62@1JB6E~F5yN3r<}aDf7Ur|=(vrrwlu+BjgL z<*GY08?~?Rf*Mdxe(fDu`B*j+)lPOM^=LkP|4dt;E>Z(KlX^onqT$I*DpP?rQYz3q znrn1inW?5Um<$^qUYTAshZ^+Zx+%+co3qXlLUv#N3aqPA1D8E+(wArAp0+S}7y&(*z3-c&x?`l#MWTw+TWIVjs z{Ov+A^^gj3hBE0V*ME?eB*n+l=-81XL%oN>Q?r%$Ybx){Jnn?BGP?!kYY*}S9~5Xj z!iQ4W2FN!?ei@;4yEpb5WJz=seSmsCH~@z|dOE2uKFaKLlB?R@;jOb#=y%Os~nNIs{AHEq&*3 zcNe8-YT>GPR|K7m&~h-E6>z_11+cXAIJ9D6WFCFUA(Zk$=w(2WT>3>#JE)6ZmMU2G zDW-)f2bQK%)On%YS-6`wwZ>!c4~V4C)VyERVTAvpkSL0Ar~~!D--jt$3Saz}FmJAd zcpy4+?@;lwX%1B#j%cj89`5_EfbUDz=B-D{d6*^t(s*{{z;lOcgXVvoZQ}$0 delta 127 zcmdndz&!sB(+1VGOo-LyVPFN>3*};;Xhh+`}0|OHyV@U=B)8xiI;*-Poh}*FP z#aI>r2?iE0b1{g?1!gV*F`3nX1mkxQQvgITg9t7)5Ct@E^1rPzd<%hWMn>1X6t~Qr GR0aTe5g8u< diff --git a/src/kernel/kernel_decls.cpp b/src/kernel/kernel_decls.cpp index a2445eaca..2234e6d63 100644 --- a/src/kernel/kernel_decls.cpp +++ b/src/kernel/kernel_decls.cpp @@ -187,6 +187,18 @@ MK_CONSTANT(non_surjective_fn, name("non_surjective")); MK_CONSTANT(ind, name("ind")); MK_CONSTANT(infinity, name("infinity")); MK_CONSTANT(pairext_fn, name("pairext")); -MK_CONSTANT(hproof_irrel_fn, name("hproof_irrel")); +MK_CONSTANT(TypeM, name("TypeM")); +MK_CONSTANT(cast_fn, name("cast")); +MK_CONSTANT(cast_heq_fn, name("cast_heq")); +MK_CONSTANT(hsymm_fn, name("hsymm")); +MK_CONSTANT(htrans_fn, name("htrans")); +MK_CONSTANT(hcongr_fn, name("hcongr")); +MK_CONSTANT(hfunext_fn, name("hfunext")); +MK_CONSTANT(hallext_fn, name("hallext")); +MK_CONSTANT(hsfunext_fn, name("hsfunext")); +MK_CONSTANT(cast_eq_fn, name("cast_eq")); +MK_CONSTANT(cast_trans_fn, name("cast_trans")); +MK_CONSTANT(cast_pull_fn, name("cast_pull")); MK_CONSTANT(proof_irrel_fn, name("proof_irrel")); +MK_CONSTANT(hproof_irrel_fn, name("hproof_irrel")); } diff --git a/src/kernel/kernel_decls.h b/src/kernel/kernel_decls.h index 61a51ec91..b3029d55b 100644 --- a/src/kernel/kernel_decls.h +++ b/src/kernel/kernel_decls.h @@ -547,10 +547,46 @@ bool is_infinity(expr const & e); expr mk_pairext_fn(); bool is_pairext_fn(expr const & e); inline expr mk_pairext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_pairext_fn(), e1, e2, e3, e4, e5, e6}); } -expr mk_hproof_irrel_fn(); -bool is_hproof_irrel_fn(expr const & e); -inline expr mk_hproof_irrel_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_hproof_irrel_fn(), e1, e2, e3, e4}); } +expr mk_TypeM(); +bool is_TypeM(expr const & e); +expr mk_cast_fn(); +bool is_cast_fn(expr const & e); +inline bool is_cast(expr const & e) { return is_app(e) && is_cast_fn(arg(e, 0)) && num_args(e) == 5; } +inline expr mk_cast(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_cast_fn(), e1, e2, e3, e4}); } +expr mk_cast_heq_fn(); +bool is_cast_heq_fn(expr const & e); +inline expr mk_cast_heq_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_cast_heq_fn(), e1, e2, e3, e4}); } +expr mk_hsymm_fn(); +bool is_hsymm_fn(expr const & e); +inline expr mk_hsymm_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_hsymm_fn(), e1, e2, e3, e4, e5}); } +expr mk_htrans_fn(); +bool is_htrans_fn(expr const & e); +inline expr mk_htrans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7, expr const & e8) { return mk_app({mk_htrans_fn(), e1, e2, e3, e4, e5, e6, e7, e8}); } +expr mk_hcongr_fn(); +bool is_hcongr_fn(expr const & e); +inline expr mk_hcongr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7, expr const & e8, expr const & e9, expr const & e10) { return mk_app({mk_hcongr_fn(), e1, e2, e3, e4, e5, e6, e7, e8, e9, e10}); } +expr mk_hfunext_fn(); +bool is_hfunext_fn(expr const & e); +inline expr mk_hfunext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7, expr const & e8) { return mk_app({mk_hfunext_fn(), e1, e2, e3, e4, e5, e6, e7, e8}); } +expr mk_hallext_fn(); +bool is_hallext_fn(expr const & e); +inline expr mk_hallext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_hallext_fn(), e1, e2, e3, e4, e5, e6}); } +expr mk_hsfunext_fn(); +bool is_hsfunext_fn(expr const & e); +inline expr mk_hsfunext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_hsfunext_fn(), e1, e2, e3, e4, e5, e6}); } +expr mk_cast_eq_fn(); +bool is_cast_eq_fn(expr const & e); +inline expr mk_cast_eq_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_cast_eq_fn(), e1, e2, e3}); } +expr mk_cast_trans_fn(); +bool is_cast_trans_fn(expr const & e); +inline expr mk_cast_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_cast_trans_fn(), e1, e2, e3, e4, e5, e6}); } +expr mk_cast_pull_fn(); +bool is_cast_pull_fn(expr const & e); +inline expr mk_cast_pull_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7) { return mk_app({mk_cast_pull_fn(), e1, e2, e3, e4, e5, e6, e7}); } expr mk_proof_irrel_fn(); bool is_proof_irrel_fn(expr const & e); inline expr mk_proof_irrel_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_proof_irrel_fn(), e1, e2, e3}); } +expr mk_hproof_irrel_fn(); +bool is_hproof_irrel_fn(expr const & e); +inline expr mk_hproof_irrel_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_hproof_irrel_fn(), e1, e2, e3, e4}); } } diff --git a/src/library/heq_decls.cpp b/src/library/heq_decls.cpp index 70ccf29d6..13acd55d3 100644 --- a/src/library/heq_decls.cpp +++ b/src/library/heq_decls.cpp @@ -6,17 +6,4 @@ Released under Apache 2.0 license as described in the file LICENSE. #include "kernel/environment.h" #include "kernel/decl_macros.h" namespace lean { -MK_CONSTANT(TypeM, name("TypeM")); -MK_CONSTANT(cast_fn, name("cast")); -MK_CONSTANT(cast_heq_fn, name("cast_heq")); -MK_CONSTANT(hsymm_fn, name("hsymm")); -MK_CONSTANT(htrans_fn, name("htrans")); -MK_CONSTANT(hcongr_fn, name("hcongr")); -MK_CONSTANT(hfunext_fn, name("hfunext")); -MK_CONSTANT(hsfunext_fn, name("hsfunext")); -MK_CONSTANT(hallext_fn, name("hallext")); -MK_CONSTANT(cast_app_fn, name("cast_app")); -MK_CONSTANT(cast_eq_fn, name("cast_eq")); -MK_CONSTANT(cast_trans_fn, name("cast_trans")); -MK_CONSTANT(cast_pull_fn, name("cast_pull")); } diff --git a/src/library/heq_decls.h b/src/library/heq_decls.h index 4e89e43d1..2776d59c2 100644 --- a/src/library/heq_decls.h +++ b/src/library/heq_decls.h @@ -5,43 +5,4 @@ Released under Apache 2.0 license as described in the file LICENSE. // Automatically generated file, DO NOT EDIT #include "kernel/expr.h" namespace lean { -expr mk_TypeM(); -bool is_TypeM(expr const & e); -expr mk_cast_fn(); -bool is_cast_fn(expr const & e); -inline bool is_cast(expr const & e) { return is_app(e) && is_cast_fn(arg(e, 0)) && num_args(e) == 5; } -inline expr mk_cast(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_cast_fn(), e1, e2, e3, e4}); } -expr mk_cast_heq_fn(); -bool is_cast_heq_fn(expr const & e); -inline expr mk_cast_heq_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_cast_heq_fn(), e1, e2, e3, e4}); } -expr mk_hsymm_fn(); -bool is_hsymm_fn(expr const & e); -inline expr mk_hsymm_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_hsymm_fn(), e1, e2, e3, e4, e5}); } -expr mk_htrans_fn(); -bool is_htrans_fn(expr const & e); -inline expr mk_htrans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7, expr const & e8) { return mk_app({mk_htrans_fn(), e1, e2, e3, e4, e5, e6, e7, e8}); } -expr mk_hcongr_fn(); -bool is_hcongr_fn(expr const & e); -inline expr mk_hcongr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7, expr const & e8, expr const & e9, expr const & e10) { return mk_app({mk_hcongr_fn(), e1, e2, e3, e4, e5, e6, e7, e8, e9, e10}); } -expr mk_hfunext_fn(); -bool is_hfunext_fn(expr const & e); -inline expr mk_hfunext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7, expr const & e8) { return mk_app({mk_hfunext_fn(), e1, e2, e3, e4, e5, e6, e7, e8}); } -expr mk_hsfunext_fn(); -bool is_hsfunext_fn(expr const & e); -inline expr mk_hsfunext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_hsfunext_fn(), e1, e2, e3, e4, e5, e6}); } -expr mk_hallext_fn(); -bool is_hallext_fn(expr const & e); -inline expr mk_hallext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_hallext_fn(), e1, e2, e3, e4, e5, e6}); } -expr mk_cast_app_fn(); -bool is_cast_app_fn(expr const & e); -inline expr mk_cast_app_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7, expr const & e8) { return mk_app({mk_cast_app_fn(), e1, e2, e3, e4, e5, e6, e7, e8}); } -expr mk_cast_eq_fn(); -bool is_cast_eq_fn(expr const & e); -inline expr mk_cast_eq_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_cast_eq_fn(), e1, e2, e3}); } -expr mk_cast_trans_fn(); -bool is_cast_trans_fn(expr const & e); -inline expr mk_cast_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_cast_trans_fn(), e1, e2, e3, e4, e5, e6}); } -expr mk_cast_pull_fn(); -bool is_cast_pull_fn(expr const & e); -inline expr mk_cast_pull_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7) { return mk_app({mk_cast_pull_fn(), e1, e2, e3, e4, e5, e6, e7}); } } diff --git a/tests/lean/univ.lean b/tests/lean/univ.lean index 3d4074f2f..9906ce40f 100644 --- a/tests/lean/univ.lean +++ b/tests/lean/univ.lean @@ -1,20 +1,20 @@ -universe M >= 1 -universe U >= M + 1 -definition TypeM := (Type M) -universe Z ≥ M+3 +universe M1 >= 1 +universe U >= M1 + 1 +definition TypeM1 := (Type M1) +universe Z ≥ M1+3 (* local env = get_environment() -assert(env:get_universe_distance("Z", "M") == 3) +assert(env:get_universe_distance("Z", "M1") == 3) assert(not env:get_universe_distance("Z", "U")) *) (* local env = get_environment() -assert(env:get_universe_distance("Z", "M") == 3) +assert(env:get_universe_distance("Z", "M1") == 3) assert(not env:get_universe_distance("Z", "U")) *) -universe Z1 ≥ M + 1073741824. +universe Z1 ≥ M1 + 1073741824. universe Z2 ≥ Z1 + 1073741824. universe U1 diff --git a/tests/lean/univ.lean.expected.out b/tests/lean/univ.lean.expected.out index 5927c52d7..1ae285e47 100644 --- a/tests/lean/univ.lean.expected.out +++ b/tests/lean/univ.lean.expected.out @@ -1,6 +1,6 @@ Set: pp::colors Set: pp::unicode - Defined: TypeM + Defined: TypeM1 univ.lean:18:0: error: universe constraint produces an integer overflow: Z2 >= Z1 + 1073741824 univ.lean:31:0: error: universe constraint inconsistency: U1 >= U4 + 0 univ.lean:33:0: error: invalid universe constraint: Z >= U + 0, several modules in Lean assume that U is the maximal universe