From 2e3b92ef36ce3c1ac777b6e5cc55c4e2a91c2ba8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 8 Jan 2014 16:52:43 -0800 Subject: [PATCH] refactor(builtin/kernel): cleanup Signed-off-by: Leonardo de Moura --- src/builtin/kernel.lean | 53 +++++++++++++---------------------- src/builtin/obj/kernel.olean | Bin 14908 -> 14923 bytes 2 files changed, 19 insertions(+), 34 deletions(-) diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean index 3fe4e71cc..b50953d0e 100644 --- a/src/builtin/kernel.lean +++ b/src/builtin/kernel.lean @@ -10,38 +10,39 @@ builtin if {A : (Type U)} : Bool → A → A → A definition TypeU := (Type U) -definition not (a : Bool) : Bool -:= a → false +definition not (a : Bool) := a → false notation 40 ¬ _ : not -definition or (a b : Bool) : Bool -:= ¬ a → b +definition or (a b : Bool) := ¬ a → b infixr 30 || : or infixr 30 \/ : or infixr 30 ∨ : or -definition and (a b : Bool) : Bool -:= ¬ (a → ¬ b) +definition and (a b : Bool) := ¬ (a → ¬ b) -definition implies (a b : Bool) : Bool -:= a → b +definition implies (a b : Bool) := a → b infixr 35 && : and infixr 35 /\ : and infixr 35 ∧ : and -definition Exists (A : TypeU) (P : A → Bool) : Bool -:= ¬ (∀ x : A, ¬ (P x)) +-- The Lean parser has special treatment for the constant exists. +-- It allows us to write +-- exists x y : A, P x y and ∃ x y : A, P x y +-- as syntax sugar for +-- exists A (fun x : A, exists A (fun y : A, P x y)) +-- That is, it treats the exists as an extra binder such as fun and forall. +-- It also provides an alias (Exists) that should be used when we +-- want to treat exists as a constant. +definition Exists (A : TypeU) (P : A → Bool) := ¬ (∀ x : A, ¬ (P x)) -definition eq {A : TypeU} (a b : A) : Bool -:= a == b +definition eq {A : TypeU} (a b : A) := a == b infix 50 = : eq -definition neq {A : TypeU} (a b : A) : Bool -:= ¬ (a == b) +definition neq {A : TypeU} (a b : A) := ¬ (a == b) infix 50 ≠ : neq @@ -81,8 +82,6 @@ theorem eqmp {a b : Bool} (H1 : a == b) (H2 : a) : b infixl 100 <| : eqmp infixl 100 ◂ : eqmp --- assume is a 'macro' that expands into a discharge - theorem imp::trans {a b c : Bool} (H1 : a → b) (H2 : b → c) : a → c := λ Ha, H2 (H1 Ha) @@ -120,8 +119,7 @@ theorem not::imp::elimr {a b : Bool} (H : ¬ (a → b)) : ¬ b theorem resolve1 {a b : Bool} (H1 : a ∨ b) (H2 : ¬ a) : b := H1 H2 --- Remark: conjunction is defined as ¬ (a → ¬ b) in Lean - +-- Recall that and is defined as ¬ (a → ¬ b) theorem and::intro {a b : Bool} (H1 : a) (H2 : b) : a ∧ b := λ H : a → ¬ b, absurd H2 (H H1) @@ -131,8 +129,7 @@ theorem and::eliml {a b : Bool} (H : a ∧ b) : a theorem and::elimr {a b : Bool} (H : a ∧ b) : b := not::not::elim (not::imp::elimr H) --- Remark: disjunction is defined as ¬ a → b in Lean - +-- Recall that or is defined as ¬ a → b theorem or::introl {a : Bool} (H : a) (b : Bool) : a ∨ b := λ H1 : ¬ a, absurd::elim b H H1 @@ -175,21 +172,13 @@ theorem eqt::intro {a : Bool} (H : a) : a == true theorem congr1 {A : TypeU} {B : A → TypeU} {f g : ∀ x : A, B x} (a : A) (H : f == g) : f a == g a := substp (fun h : (∀ x : A, B x), f a == h a) (refl (f a)) H --- Remark: we must use heterogeneous equality in the following theorem because the types of (f a) and (f b) --- are not "definitionally equal" They are (B a) and (B b) --- They are provably equal, we just have to apply Congr1 - theorem congr2 {A : TypeU} {B : A → TypeU} {a b : A} (f : ∀ x : A, B x) (H : a == b) : f a == f b := substp (fun x : A, f a == f x) (refl (f a)) H --- Remark: like the previous theorem we use heterogeneous equality We cannot use Trans theorem --- because the types are not definitionally equal - theorem congr {A : TypeU} {B : A → TypeU} {f g : ∀ x : A, B x} {a b : A} (H1 : f == g) (H2 : a == b) : f a == g b := subst (congr2 f H2) (congr1 b H1) --- Remark: the existential is defined as (¬ (forall x : A, ¬ P x)) - +-- Recall that exists is defined as ¬ ∀ x : A, ¬ P x theorem exists::elim {A : TypeU} {P : A → Bool} {B : Bool} (H1 : Exists A P) (H2 : ∀ (a : A) (H : P a), B) : B := refute (λ R : ¬ B, absurd (λ a : A, mt (λ H : P a, H2 a H) R) @@ -199,11 +188,6 @@ theorem exists::intro {A : TypeU} {P : A → Bool} (a : A) (H : P a) : Exists A := λ H1 : (∀ x : A, ¬ P x), absurd H (H1 a) --- At this point, we have proved the theorems we need using the --- definitions of forall, exists, and, or, =>, not We mark (some of) --- them as opaque Opaque definitions improve performance, and --- effectiveness of Lean's elaborator - theorem or::comm (a b : Bool) : (a ∨ b) == (b ∨ a) := iff::intro (λ H, or::elim H (λ H1, or::intror b H1) (λ H2, or::introl H2 a)) (λ H, or::elim H (λ H1, or::intror a H1) (λ H2, or::introl H2 b)) @@ -352,3 +336,4 @@ set::opaque exists true set::opaque not true set::opaque or true set::opaque and true +set::opaque implies true \ No newline at end of file diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean index 6a147dec0f1e32e0eeea946bebe92cd9301d518c..c5e9431e3a97584246173e46bbe55283e527d167 100644 GIT binary patch delta 3043 zcmYM032>BE634&(CYel<`G(0cN3IETuENl2ue( zDM36b3MI7Gs))w&!UKzxx@=$(R1PgxghdvVl~q?(R>TtT3)t7)$d{_T`Q`t*|F7RU z`P-6xOV$os^_GEwK5gi!>5w^ewh1zDJd8pXehb&yi!}99kV>r&`}Aow0aFMP+PE)7 zXxO-=#@5+CNS~S?ztD@pj}A){lwg;|uiC|yYN*6VEdx-6j+AbQ8BJ`*IzUEp}=p&TU`w1N~7eeFL(tGjwvQdx-i^1U7hJHv!wk3+H>5{l1-_HsiNTD5 zG%;I)$&6-Lh08MHfcSF8bo+y*{X^)<^t;xPpc&L$+<`yil+2dEdeX$_5fe8Mdbp@Z zaU|1~-%Em)pr(VGi;M9vewf*o_AqH$0w1q&>)J53+NV@KLy8!0H1SzNgN>gfJR0JS zS%5q2L3kSfW1oaE!4Y!JW#ux{i@Ll6l&tEAo_wyKT&g#KXcE0bzbWf;W zXyhIHFJY4LBwm?a-Y^1`+rxLnNGBF$k=()U8uj!2TST1+3Bk?TUGNc}&5l=pPO>cP zX+>~V886RAB+GG?>VhoK#d$e#IECwTS^{5DguFjr6UyYjA(RdI7SHDt!)z?hjldb4 zk~<^uJ#|XT4}_BPBcY`HL>S}w{Y==!_zND-C8Kk>0r(F6u8?ZmT~`Nr?&1f`><3&a z`+)^_xhmD*U%HCmJUZN~6E?Et5`fo2QZh)DluSY{0qlxk4V3@}9&}R)XWY$@hIO80 zi7bi}qijMk${`e^TtYE&DS}}(a^t5SG0MdPuNRzH?@ieAD3*5t@^Pv667b?H-Ucr} z@gn;u!X~>KM@wE53Ne;9w>3bzl);Cfok!tQJBcw&0iBE`gbBt{!YJJ&CZ!7&SIo3fo-bMJNT9wm@&3aowf;M zt5n-R_IcIj`MZhz8=x060|*27SYRXEfE~eb&Qx;I_{7`zimETY6~TnDlw>Q0|QP9bkp`PQJQC-iPDEx5GWS zBRt|+Lm@KtdriFWrMpWK0Qck0(pB&fPA&`Q+{RvVPo-4Em1RkI1h<#1hR3n9JO=A= zd3h3^d}3=k*f*JOFXDTV0vsHdf+s58_Pkf?LGL#s<;s|_1`MdZ>cC0Xl-lQ^@s+kS?k z#s4eZR-3H;m;`N-`n8P8!_&?RAAfB&F&~Oz8eLh1>K^p)TP`O2mP?U8hJKRm;&2zqHe`=^)Wc75JaUuG1SWOQCZy zT%1ndS(X!}bT8C(J{#+SF}Sc{fm+Y~4a?P?y*%Ec{+Aw#uMBu7U#z@@GA_TzVwI1v zM59U^NW2Mdu3&0ogNNT*N#nOx(!#i*F{F%NSFL*J8;c--smW^h6@zm$y{CV$uV?=C O8ni9`Lwir(eC_|x9$Y5ENWnnC7T7B9tpMuT|;t6b2P7)YO7dzB?jCzN7m z5IVSI8=<{p=GFA6_2TmM5rIBJgR{)CkUh#-osFg~3Nvwp&9CgGwm#!J_QMZtrRnq8 z^;S+>zPVgk5BTa9gLZBtWylcJk2ibNq zr#IqJJdl-4f0Q&Wfdi2OU3(gn=2?;FNs)~x0@R^mO5 z*7|p>eCsS+uMl*#;yTi_-DFBm?b=$@o#zBLktQ|0XW?c-SweV{~yIO9PKy#2eeVlu6MNY4AfHVVLxg~kf$cJ@U3DCrN1SjNH z#9syS>6O=;ELRFupb9<8*08MS<3%G5u97jH(@`?a&x7! zAj?y5YF+~z!zc1u0>{Zi8qF_+vhZICfJwNw@FMl4&^TyX zqLOq;H-u2qRT0XHstIL95yJC0T@8LQXd+Z#r0AMXe$$d-D0xVVdP1ovMkp1<38kV2 zLf&FX5b`U4M*Oj8h}x<_Ua!4^Z+JRQsCDBR-bz(-pLZ}s@nP?1wH>>?(UxW!l*xw^ zdbzw2gtCt#73mIEM-gUAgFB{})}>Ft+4g+wF3y2goLxK$hT&_)69VltDrq|iCGDAn zvMpn=%r_d^u*WybJcneNZ9Kl=Yll5}!dI#~gs)^n^<-=CLJKcqq(gx<%INLgAF=udoEJ>kuP52y zg{p1Z5}X1zV|geB*Wo3hYPb#W3!QJyV;|m^+wsRxsPbJBq%Fjx6>ejNPfxz*MBa+c z;XB|i+z?*jzK>jF>Gxas!0UIHB>)gN4xSH-aBO)vZ!V4Ud20Wcx)ARuZ-U2hUHQGR z7|*PT!DBeLq6waTc1;DC%gJ35zl3|Li|}COXYMyF@l6X?;?^O4SccEkdf;_Tt4f-y ztijbBJiBVUd!r@tQYHB&oK)?Hw>fwNV)Za{i{H;K!b6x7b*Tq1I9dh=urqqY z8AoX_jZf-3Lb;24fy1nFpYNg$1}FF)`N)kQ6_=qNPextX&QC=ipHha^`QZp&T-Rm( zOx}|JIIgX0syRS{)~0?_R!IX&vcflC>n7&=P(rh-RNwxur`F%;PB|^;se~M;r{T%^7@SanZe7>0Gj@9eRjeccktu zPg19vQVtKM=b&EkK&%%W*b~1(?d7)k9Q9PsZfH^eO?SpT_+rCVfdUGYbZ$bKm-{lW zQ!m7LqEQ83o%ldCa0(mW7