From c423198a698836fd6870e9a5be0731e50e70e0d4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 1 Jan 2014 11:35:21 -0800 Subject: [PATCH] feat(builtin/kernel): add Not.*Elim theorems Signed-off-by: Leonardo de Moura --- src/builtin/kernel.lean | 18 ++++++++++++++++++ src/builtin/obj/kernel.olean | Bin 20042 -> 21583 bytes tests/lean/exists8.lean | 27 +++++++++++++++++++++++++++ tests/lean/exists8.lean.expected.out | 8 ++++++++ 4 files changed, 53 insertions(+) create mode 100644 tests/lean/exists8.lean create mode 100644 tests/lean/exists8.lean.expected.out diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean index 903ecea16..0fcb8158e 100644 --- a/src/builtin/kernel.lean +++ b/src/builtin/kernel.lean @@ -306,24 +306,36 @@ Theorem NotAnd (a b : Bool) : (¬ (a ∧ b)) == (¬ a ∨ ¬ b) (Case (λ y, (¬ (false ∧ y)) == (¬ false ∨ ¬ y)) Trivial Trivial b) a +Theorem NotAndElim {a b : Bool} (H : ¬ (a ∧ b)) : ¬ a ∨ ¬ b +:= EqMP (NotAnd a b) H. + Theorem NotOr (a b : Bool) : (¬ (a ∨ b)) == (¬ a ∧ ¬ b) := Case (λ x, (¬ (x ∨ b)) == (¬ x ∧ ¬ b)) (Case (λ y, (¬ (true ∨ y)) == (¬ true ∧ ¬ y)) Trivial Trivial b) (Case (λ y, (¬ (false ∨ y)) == (¬ false ∧ ¬ y)) Trivial Trivial b) a +Theorem NotOrElim {a b : Bool} (H : ¬ (a ∨ b)) : ¬ a ∧ ¬ b +:= EqMP (NotOr a b) H. + Theorem NotEq (a b : Bool) : (¬ (a == b)) == ((¬ a) == b) := Case (λ x, (¬ (x == b)) == ((¬ x) == b)) (Case (λ y, (¬ (true == y)) == ((¬ true) == y)) Trivial Trivial b) (Case (λ y, (¬ (false == y)) == ((¬ false) == y)) Trivial Trivial b) a +Theorem NotEqElim {a b : Bool} (H : ¬ (a == b)) : (¬ a) == b +:= EqMP (NotEq a b) H. + Theorem NotImp (a b : Bool) : (¬ (a ⇒ b)) == (a ∧ ¬ b) := Case (λ x, (¬ (x ⇒ b)) == (x ∧ ¬ b)) (Case (λ y, (¬ (true ⇒ y)) == (true ∧ ¬ y)) Trivial Trivial b) (Case (λ y, (¬ (false ⇒ y)) == (false ∧ ¬ y)) Trivial Trivial b) a +Theorem NotImpElim {a b : Bool} (H : ¬ (a ⇒ b)) : a ∧ ¬ b +:= EqMP (NotImp a b) H. + Theorem NotCongr {a b : Bool} (H : a == b) : (¬ a) == (¬ b) := Congr2 not H. @@ -339,11 +351,17 @@ Theorem NotForall (A : (Type U)) (P : A → Bool) : (¬ (∀ x : A, P x)) == ( NotCongr (ForallEqIntro (λ x : A, (Symm (DoubleNeg (P x))))) in Trans L2 L1. +Theorem NotForallElim {A : (Type U)} {P : A → Bool} (H : ¬ (∀ x : A, P x)) : ∃ x : A, ¬ P x +:= EqMP (NotForall A P) H. + Theorem NotExists (A : (Type U)) (P : A → Bool) : (¬ ∃ x : A, P x) == (∀ x : A, ¬ P x) := let L1 : (¬ ∃ x : A, P x) == (¬ ¬ ∀ x : A, ¬ P x) := Refl (¬ ∃ x : A, P x), L2 : (¬ ¬ ∀ x : A, ¬ P x) == (∀ x : A, ¬ P x) := DoubleNeg (∀ x : A, ¬ P x) in Trans L1 L2. +Theorem NotExistsElim {A : (Type U)} {P : A → Bool} (H : ¬ ∃ x : A, P x) : ∀ x : A, ¬ P x +:= EqMP (NotExists A P) H. + Theorem UnfoldExists1 {A : TypeU} {P : A → Bool} (a : A) (H : ∃ x : A, P x) : P a ∨ (∃ x : A, x ≠ a ∧ P x) := ExistsElim H (λ (w : A) (H1 : P w), diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean index cbad4b0e0054511ebd359dec457cec5667a8e8e5..82eff1ff67b6851fb23f8f644856648a7716b176 100644 GIT binary patch delta 3355 zcmZ`*X>3$g6n^iPseSKFg;J){+GUzfr)6t96a_lnJEeO|O$8J~z$FpW0ClpJ`@M6|J?Hz*xyu~c ztRLT|?>;@vTe0Zg>h^^lTC7;02~GZsk??MSxWrgdt7QRtXiL6}x~E#Rh5FW|QFmb2 zA&0m`hA-Q2r*iX1i&h5n7z{2iXLvpsRLvrkplefIMZwtc^myQ@zo79fTY$8>jwSe` zZ4kJ*+O&jMzr^ugSLVbKsGeJlfmu0-2aj1b+aMDI$sRd)_j{i+NgbSfxH*Vj=? zQEtNPNVtx9y}^*4EIO7^{ort74?rxVf-q*$zLKP23}+8Mp;Xj8+V{Q9`pV|(TP5ez9GV=uWx@l^qH#^R+5 z+S_p~skI~%H_4jvv0Y{z`$bn)1S@OKjAYN{=X4j4uA1RrfVB)SMskC>j?I5F#GF}= zp~1e9QslSC)}pHW3m00p!4cL))i_~3CwEPHimfurYYWW{ z6bN%Wtq*wg9_k59)Ze0S10DJ`YO2mI6fwwkN-Yn!$LzIL1YgAJl?#_GUlwXrYUmjs zg4a2z%GDL_)<8sT`^FJCljhHmD{cTh%g~6_0rNRFn+!2${)*u@yIb-zxSK&G+#5sU zDXM4d18IKwrC;IC>)5E~{X0zago6eel4xsnq3T^omX$%@Hzv`QYD?Ke*OQe?Ni)WG ziFldON@4Oh0;Vw>1(?n-K~)Zh3^w2$u`)o~OgbZJexXBFwq$QI;*S_Am@`Mzh9az~yY^)7csIPOAa95knJ|)+Dv@z2sn89HuQY z49bY^S>u65FdevBdFrNEr*XOtm?8sjt9d}xDmHkKtre76J4c8_dZ;!zUxjmUI1Znu zB6AXTJ=MsNn)L*R4RolsR0t<`C%G;V)tz2SX!3Tcnjk>9J^NMlVB?oh;IvyiS?bMz z-3-$JcQZ_9?LKbI9+-PnSioNP$Y2;RK7Wg5C1lsaUYXLAs-1lMu4B=A7?* zbLPzKI`9R_DtfLBt^revcuAH{GDTredEp;!_bp zT@6Ll8_X;H0IMS$_+c7;1o%D;HU;GwdZ($;{S-RzvnHs&B|v4(`O3OV8=K3vTC;vE zsI=0L5qFU}KLMO%_!;07!_R#h%d>D?vi$gb1#_9<*MQ&9Tg{Iyw`PEU@+tU=p zy4k#XMRI{l>JDHCIMuF85}k zW*<$pRxR0^(IMIpEmrmcx*aZ}#;|Yu838J95c^TA;tQxaY*I9|rcD5QIpCZL&{prp zSkBhax)$KZjlyjorsLs8r9aogYjf>mW(JP((lIJ&^S4eT>Li!)0PZt%X+`D~zsK6? z|8;^>UZml+R$3aV%G&t^#Uo|y_LXE71ZG^sSul?AZhizDPc}VW-wfG8BWLK{NTsr` z(@dl?tI`}5MK>z@FA8>)S!O03MZ2R9N|)Y<_RC+$Zm%epH*_6mU4|UUcXHCg==F|} zp;pO}aq8&Tj{A)-HSSJ`R>d9|lD{GQ5#GUVz#4|X1J*M9!;AtuSGjHkfw08EYSMo(0|o z^PHjN8oYUrAx0m(tdn`4&*a6LzKEI^D2HO{>*y)3wXKU^7=yeiT&h$R|{?=W5T zr8;|r0-aAPIZwl#B^wN{mwCC4xyfFxW(N8(%`KecFem7I=O!g@k(Jn%bzYM+m{>ow z=y`Ikns$QA{0aOGl5@P(e*n!G-UYk>ui_gis`#YvYB}SkMS%Pc^E>TKX19n3YD(ATpEB{YU>%$)(=F$7H+*y1d^t#;f^cQ_z;rM_&`Vvh#dGP}dM*QWx2qtI zO}Hzv+1TrX&BJV9cXJVCu38T79V6+MEd)5z^i=n&O5UOQ?!@9|yK%a{Ie9r!7slPH z4lHADn$D>emeQoeb*o#|u_j b$dQSG9YXc&@7=R^kC5Tr&$RXS^@#rf*X Int -> Bool + +Theorem T1 (R1 : not (exists x y, P x y)) : forall x y, not (P x y) := + ForallIntro (fun a, + ForallIntro (fun b, + ForallElim (NotExistsElim (ForallElim (NotExistsElim R1) a)) b)) + +Axiom Ax : forall x, exists y, P x y + +Theorem T2 : exists x y, P x y := + Refute (fun R : not (exists x y, P x y), + let L1 : forall x y, not (P x y) := ForallIntro (fun a, + ForallIntro (fun b, + ForallElim (NotExistsElim (ForallElim (NotExistsElim R) a)) b)), + L2 : exists y, P 0 y := ForallElim Ax 0 + in ExistsElim L2 (fun (w : Int) (H : P 0 w), + Absurd H (ForallElim (ForallElim L1 0) w))). + +Theorem T3 (A : (Type U)) (P : A -> A -> Bool) (a : A) (H1 : forall x, exists y, P x y) : exists x y, P x y := + Refute (fun R : not (exists x y, P x y), + let L1 : forall x y, not (P x y) := ForallIntro (fun a, + ForallIntro (fun b, + ForallElim (NotExistsElim (ForallElim (NotExistsElim R) a)) b)), + L2 : exists y, P a y := ForallElim H1 a + in ExistsElim L2 (fun (w : A) (H : P a w), + Absurd H (ForallElim (ForallElim L1 a) w))). diff --git a/tests/lean/exists8.lean.expected.out b/tests/lean/exists8.lean.expected.out new file mode 100644 index 000000000..badf3dbab --- /dev/null +++ b/tests/lean/exists8.lean.expected.out @@ -0,0 +1,8 @@ + Set: pp::colors + Set: pp::unicode + Imported 'int' + Assumed: P + Proved: T1 + Assumed: Ax + Proved: T2 + Proved: T3